Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

122 problems · 1/3Number SourcesGraph view

declared open · formalizederdos:11

∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ l

number theoryadditive basisA001220 · A3775873 sources

declared open · formalizederdos:12

A \subset \mathbb{N}

be infinite with no distinct

a, b, c \in A

such that

a \mid (b + c)

with

b, c > a

. Can

|A \cap [1, N]|/\sqrt{N}

have positive lower limit? Must every such

A

fall below

N^{1-c}

infinitely often?

number theoryN/A4 sources

declared open · formalizederdos:25

True ↔ ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ (i : ℕ), 0 < seq_n i) → StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d

number theoryN/A3 sources

declared open · formalizederdos:36

Erdos36.M 5 = 3

number theoryadditive combinatoricsA393584 · possible3 sources

declared open · formalizederdos:51

True ↔ ∃ A n, A.Infinite ∧ (∀ (a : ↑A), IsLeast (Nat.totient ⁻¹' {↑a}) (n a)) ∧ Filter.Tendsto (fun a => ↑(n a) / ↑↑a) Filter.atTop Filter.atTop

number theoryA002202 · A0141973 sources

declared open · formalized · $250erdos:52

True ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ C, 0 < C ∧ ∀ (A : Finset ℤ), max ↑(A + A).card ↑(A * A).card ≥ C * ↑A.card ^ (2 - ε)

number theoryadditive combinatoricsA2639963 sources

declared open · formalizederdos:75

True ↔ ∃ V G, G.chromaticCardinal = Cardinal.aleph 1 ∧ Cardinal.mk V = Cardinal.aleph 1 ∧ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph), H.verts.ncard = n → ∃ I, ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)

graph theorychromatic numberN/A3 sources

declared openerdos:81

Erdős problem 81

graph theorypossible2 sources

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared open · formalizederdos:124

∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹

number theorybase representationsN/A4 sources

declared open · formalized · $500erdos:138

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 sources

declared open · $250erdos:165

Erdős problem 165

graph theoryramsey theoryA0007912 sources

declared openerdos:176

Let

N(k, \ell)

be the least

N

such that every

f : [N] \to \{-1, 1\}

has a

k

-term arithmetic progression

P

with

|\sum_{n \in P} f(n)| \ge \ell

. In particular, is

N(k, 2) \le C^k

additive combinatoricsarithmetic progressionsdiscrepancypossible3 sources

declared open · formalizederdos:218

{n | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

number theoryprimesA333230 · A333231 · A0641133 sources

declared open · formalizederdos:233

(fun N => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ 2

number theoryprimesA0747413 sources

declared open · formalizederdos:251

True ↔ Irrational (∑' (n : ℕ), ↑(Nat.nth Nat.Prime n) / 2 ^ n)

number theoryirrationalityA0989903 sources

declared open · formalizederdos:263

sorry ↔ Erdos263.IsIrrationalitySequence fun n => 2 ^ 2 ^ n

irrationalityN/A3 sources

declared open · formalizederdos:264

¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x

irrationalityN/A4 sources

declared open · formalizederdos:288

sorry ↔ {I | ∀ (j : Fin 2), (I j).1 ≤ (I j).2 ∧ ∃ n, ∑ j, ∑ nⱼ ∈ (Set.Icc (I j).1 (I j).2).toFinset, (↑↑nⱼ)⁻¹ = ↑↑n}.Finite

number theoryunit fractionsN/A3 sources

declared open · formalizederdos:306

a/b \in \mathbb{Q}_{>0}

and

b

is squarefree, can

a/b

always be written as a finite sum of reciprocals of distinct products of two distinct primes?

number theoryunit fractionsN/A4 sources

declared open · formalizederdos:326

Does there exist

A=\{a_1<a_2<\cdots\}\subset \mathbb{N}

which is a minimal basis of order

2

(every large integer is the sum of

2

elements from

A

, and no proper subset of

A

has this property) such that

\lim_{k\to \infty}a_k/k^2=c

for some

c\neq 0

? A claimed construction gives a minimal basis with

A(x)=C\sqrt{x}+O(1)

, answering the question affirmatively; Erdős and Graham had conjectured a negative answer.

number theoryadditive basisN/A4 sources

declared openerdos:327

Erdős problem 327

number theoryunit fractionsA3849272 sources

declared open · formalizederdos:342

sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → {n | ∃ m, a m = a n + 2}.Infinite

number theoryA0028583 sources

declared openerdos:345

Erdős problem 345

number theorycomplete sequencesA0016612 sources

declared open · formalizederdos:346

Let

A=\{1\leq a_1< a_2<\cdots\}

be a set of integers such that

A\backslash B

is complete for any finite subset

B

and not complete for any infinite subset

B

. If

a_{n+1}/a_n \geq 1+\epsilon

for all

n

, must

\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2

? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

number theorycomplete sequencesN/A4 sources

declared open · formalizederdos:349

∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α

number theorycomplete sequencesN/A3 sources

declared open · formalizederdos:352

True ↔ ∃ c > 0, ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → ↑(MeasureTheory.volume A) ≥ ↑c → ∃ t, (∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1

geometryN/A3 sources

declared openerdos:367

Erdős problem 367

number theoryA0575213 sources

declared openerdos:368

Erdős problem 368

number theoryA0743993 sources

declared openerdos:374

Erdős problem 374

number theoryA388851 · A387184 · A389117 · A3891482 sources

declared openerdos:388

Erdős problem 388

number theoryN/A2 sources

declared open · formalizederdos:390

Let

f(n)

be the least

m

for which

n!

can be written as

a_1\cdots a_k

with

n < a_1 < \cdots < a_k = m

- the smallest possible largest factor in a factorization of

n!

into distinct integers all exceeding

n

. Erdős, Guy and Selfridge proved

f(n) - 2n \asymp n/\log n

. Erdős asked whether there is a constant

c

with

f(n) - 2n \sim c\,\frac{n}{\log n},

and what it is. This preprint answers yes and names the constant:

\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.

number theoryfactorialsA1934294 sources

declared openerdos:393

Erdős problem 393

number theoryfactorialsA3883022 sources

declared open · formalizederdos:396

True ↔ ∀ (k : ℕ), ∃ n, n.descFactorial (k + 1) ∣ n.centralBinom

number theorybinomial coefficientsA3750773 sources

declared open · formalizederdos:400

True ↔ ∀ k ≥ 2, ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x => c * ↑x * Real.log ↑x

number theoryfactorialspossible3 sources

declared openerdos:411

Erdős problem 411

number theoryiterated functionsA383044 · possible2 sources

declared openerdos:415

Erdős problem 415

number theorypossible2 sources

declared openerdos:423

Erdős problem 423

number theoryA0052432 sources

declared openerdos:425

Erdős problem 425

number theorysidon setspossible2 sources

declared openerdos:432

Erdős problem 432

number theoryN/A2 sources

declared openerdos:451

Let

n_k

be the least integer greater than

2k

for which

\prod_{i=1}^k (n_k - i)

has no prime factor in

(k, 2k)

. How rapidly must

n_k

grow?

number theoryA3866203 sources

declared open · formalizederdos:456

True ↔ Filter.Tendsto (fun N => ↑(Nat.count {n | Erdos456.m n < Erdos456.p n} N) / ↑N) Filter.atTop (nhds 1)

number theoryA034694 · A061026 · possible3 sources

declared openerdos:460

Erdős problem 460

number theoryN/A2 sources

declared open · formalizederdos:477

Does there exist an integer polynomial

f

of degree at least two and a set

A \subseteq \mathbb{Z}

such that every integer has a unique representation

n = a + f(k)

? A manuscript claims the thirteenth powers admit a tiling complement.

number theoryN/A4 sources

declared open · formalizederdos:501

For every

x \in \mathbb{R}

let

A_x \subset \mathbb{R}

be a bounded set of Lebesgue outer measure

< 1

. Must there be an infinite independent set, that is an infinite

X \subseteq \mathbb{R}

with

x \notin A_y

for all distinct

x, y \in X

? Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal. The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

combinatoricsset theoryN/A4 sources

declared open · formalizederdos:503

∀ (n : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} sorry

geometrydistancesA1757693 sources

declared open · formalizederdos:507

Asymptotics.IsEquivalent Filter.atTop Erdos507.α sorry

geometryN/A3 sources

declared open · formalizederdos:513

sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

analysisN/A3 sources

declared openerdos:514

For a transcendental entire function, how fast can

|f(z)|

be forced to grow along a path to infinity, and how short can such a path be in terms of the maximum modulus

M(r, f)

analysisN/A4 sources

declared open · formalizederdos:521

False ↔ Erdos521.Claim

analysispolynomialsprobabilityN/A4 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science