Vela Mathematics Program: problems

Narrowed tosource:erdos-ai-contributions-wiki ×Clear all

Problem ledger

353 problems · 5/8Number SourcesGraph view

declared solved (Lean)erdos:696

declared proved (Lean) · formalizederdos:698

True ↔ ∃ h, Filter.Tendsto h Filter.atTop Filter.atTop ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → h n ≤ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientspossible5 sources

declared disproved (Lean) · formalized · $1000erdos:707

Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a 1000 dollars prize attached, that every finite Sidon set extends to a perfect difference set modulo

p^2+p+1

for some prime

p

. Alexeev and Mixon establish that

\{1,2,4,8\}

is a counterexample - and discovered along the way that Marshall Hall, Jr. had published a different counterexample three decades before Erdős first posed the problem, unnoticed by the community for half a century.

additive combinatoricssidon setsN/A6 sources

declared proved (Lean)erdos:716

Erdős problem 716

graph theoryhypergraphspossible3 sources

declared proved (Lean) · formalizederdos:728

Whether there are infinitely many integers

a, b, n

with

a, b \ge \varepsilon n

such that

a!\cdot b!

divides

n!\cdot(a+b-n)!

while

a+b

exceeds

n

by more than

C\cdot\log n

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:729

True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite

number theoryfactorialsN/A6 sources

declared open · formalizederdos:730

True ↔ Erdos730.S.Infinite

number theorybinomial coefficientsbase representationsA1295154 sources

declared openerdos:731

Let

A(n)

be the least positive integer not dividing

\binom{2n}{n}

. Erdos asked for the behaviour of

A(n)

for reasonable

n

. Under an explicit dyadic-regularity formalization of reasonable, the distribution is determined on dyadic intervals against the scale

F_X = \sqrt{2}(\log 2)^{1/4} L^{1/4} \exp\sqrt{(\log 2)L}

with

L = \log(2X)

number theorybinomial coefficientsA0061974 sources

declared solved (Lean) · formalizederdos:741

True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

additive combinatoricsN/A6 sources

declared open · formalizederdos:749

True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1

additive combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:750

True ↔ ∀ (f : ℕ → NNReal), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ V G, G.chromaticNumber = ⊤ ∧ ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - f m ≤ ↑I.ncard

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:751

False ↔ ∀ (k : ℕ), ∃ V G, G.chromaticNumber = 4 ∧ ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:753

False ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ), 0 < n → ∀ (G : SimpleGraph (Fin n)), ↑n ^ (1 / 2 + c) < ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ)

graph theorychromatic numberN/A5 sources

declared proved (Lean) · formalizederdos:756

True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)

geometrydistancespossible5 sources

declared proved (Lean) · formalizederdos:760

True ↔ ∃ c > 0, ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ), G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:762

False ↔ ∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V), G.CliqueFree 5 → 4 ≤ G.cochromaticNumber → G.chromaticNumber ≤ G.cochromaticNumber + 2

graph theorychromatic numberN/A5 sources

declared solved (Lean)erdos:765

Erdős problem 765

graph theoryturan numberA0068553 sources

declared openerdos:768

Let

A(x)

count

n \le x

such that every prime

p \mid n

has a divisor

d > 1

n

with

d \equiv 1 \pmod p

. Erdos asked whether

A(x)/x = \exp(-(c+o(1))\sqrt{\log x}\log\log x)

. It does, with

c = 1/(2\sqrt{\log 2})

number theoryA001034 · A3522873 sources

declared disproved (Lean) · formalizederdos:775

False ↔ ∃ C, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, n - C ≤ H.cliqueSizes.ncard

graph theoryhypergraphspossible5 sources

declared openerdos:776

Erdős problem 776

combinatoricspossible2 sources

declared solvederdos:783

Erdős problem 783

number theoryN/A3 sources

declared proved (Lean) · formalizederdos:785

True ↔ ∀ (A B : Set ℕ), A.Infinite → B.Infinite → Erdos785.IsExactAdditiveComplement A B → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop

additive combinatoricsN/A5 sources

declared openerdos:788

Erdős problem 788

additive combinatoricspossible3 sources

declared disproved (Lean) · formalizederdos:794

False ↔ ∀ (n : ℕ) (H : Finset (Finset (Fin (3 * n)))), H.IsThreeUniform → n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7

graph theoryhypergraphsturan numberN/A5 sources

declared proved (Lean) · formalizederdos:798

True ↔ (fun n => ↑(Erdos798.t n)) =o[Filter.atTop] fun n => ↑n

geometryA1164465 sources

declared proved (Lean) · formalizederdos:818

True ↔ ∀ (K : ℝ), 0 < K → ∃ C, 0 < C ∧ ∃ c, 0 < c ∧ ∀ (A : Finset ℤ), 2 ≤ A.card → ↑(A + A).card ≤ K * ↑A.card → c * ↑A.card ^ 2 / Real.log ↑A.card ^ C ≤ ↑(A * A).card

additive combinatoricsN/A5 sources

declared openerdos:819

Erdős problem 819

additive combinatoricspossible2 sources

declared verifiable · formalizederdos:835

∀ {k : ℕ}, 3 ≤ k → k ≤ 8 → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

graph theoryhypergraphsN/A3 sources

declared openerdos:836

Erdős problem 836

graph theoryhypergraphschromatic numberN/A2 sources

declared proved (Lean) · formalizederdos:844

True ↔ ∀ (N : ℕ), IsGreatest {k | ∃ A ⊆ Finset.Icc 1 N, (∀ a ∈ A, ∀ b ∈ A, ¬Squarefree (a * b)) ∧ A.card = k} (Erdos844.evenOrOddNonSquarefree N).card

number theoryintersecting familyN/A5 sources

declared disproved (Lean) · formalizederdos:845

False ↔ ∀ (C : ℝ), 0 < C → have f := fun x => match x with | (k, l) => 2 ^ k * 3 ^ l; {x | ∃ B, ∃ (h : B.Nonempty) (_ : ↑(B.sup f) ≤ C * ↑(B.inf' h f)), ∑ x ∈ B, f x = x}.HasDensity 0

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:846

False ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A

geometryN/A6 sources

declared decidable · formalizederdos:848

Is the maximum size of a set

A\subseteq \{1,\ldots,N\}

such that

ab+1

is never squarefree (for all

a,b\in A

) achieved by taking those

n\equiv 7\pmod{25}

? Resolved for all sufficiently large

N

: any near-maximal

A

is contained in

\{n\equiv 7\pmod{25}\}

\{n\equiv 18\pmod{25}\}

, leaving only a finite check.

number theoryN/A4 sources

declared proved · formalizederdos:851

∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d

number theoryN/A4 sources

declared openerdos:852

Erdős problem 852

number theoryprimesA001223 · A053597 · A0785152 sources

declared openerdos:856

Let

k\geq 3

and

f_k(N)

be the maximum of

\sum_{n\in A}\frac{1}{n}

over all

A\subseteq\{1,\ldots,N\}

containing no

k

subsets with the same pairwise least common multiple. Estimate

f_k(N)

. The claimed answer:

f_k(N)=(\log N)^{\gamma_k+o(1)}

, where

\gamma_k

is a weighted generalization of the Tang-Zhang sunflower capacity.

number theorypossible3 sources

declared solvederdos:858

Erdős problem 858

number theoryprimitive setsN/A4 sources

declared solved (Lean) · formalizederdos:862

False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)

number theorysidon setsA3823955 sources

declared provederdos:863

Erdős problem 863

number theorysidon setsadditive combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:865

∃ C > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

number theoryadditive combinatoricspossible5 sources

declared openerdos:866

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1, \dots, 2N\}

; in particular, determine the positive variant

h_4(n)

number theoryadditive combinatoricspossible5 sources

declared disproved (Lean) · formalizederdos:867

False ↔ ∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ ↑N / 2 + C

additive combinatoricspossible5 sources

declared solved · formalizederdos:868

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → Filter.Tendsto (fun n => Erdos868.ncard_add_repr A 2 n) Filter.atTop Filter.atTop → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

number theoryadditive basisN/A3 sources

declared openerdos:870

Let

k\geq 3

and

A

be an additive basis of order

k

. Does there exist a constant

c=c(k)>0

such that if

r(n)\geq c\log n

for all large

n

(where

r(n)

counts representations of

n

as a sum of at most

k

elements of

A

) then

A

must contain a minimal basis of order

k

? The claimed answer is no, for every

k\geq 3

number theoryadditive basisN/A3 sources

declared disproved (Lean) · formalizederdos:871

False ↔ ∀ (A : Set ℕ), ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧ ∀ (t : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) → ∃ B C, (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧ Disjoint B C ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n

number theoryadditive basisN/A6 sources

declared open · formalizederdos:872

True ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos872.L n) ≥ ε * ↑n

number theoryprimitive setspossible3 sources

declared open · formalizederdos:873

True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)

number theoryN/A3 sources

declared openerdos:875

Erdős problem 875

additive combinatoricsN/A2 sources

declared solved · formalizederdos:888

(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

number theorysquaresA3875845 sources

declared solvederdos:896

Erdős problem 896

number theorypossible3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science