Vela Mathematics Program: problems

Narrowed todisproved (Lean) ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

59 problems · 1/2Number SourcesGraph view

declared disproved (Lean) · formalizederdos:16

False ↔ ∃ A B, Erdos16.Erdos16Set = A ∪ B ∧ (∃ a, ∃ d > 0, A = {x | ∃ m, x = a + m * d}) ∧ Erdos16.density_zero B

number theoryadditive basisprimesA0062855 sources

declared disproved (Lean) · formalizederdos:26

A\subset\mathbb{N}

be infinite. Must there exist some

k\geq 1

such that almost all integers have a divisor of the form

a+k

for some

a\in A

? The question as posed follows negatively from Davenport–Erdős (1951). The AI result settles Tenenbaum's harder variant, also negatively: there is an infinite

A

such that for every

k\geq 1

the set of multiples of

A+k

has upper density below

0.34

number theorydivisorsN/A6 sources

declared disproved (Lean) · formalizederdos:34

False ↔ ∀ (c : ℝ), 0 < c → ∃ N, ∀ n ≥ N, ∀ (p : Equiv.Perm (Fin n)), ↑(Erdos34.consecutiveSums n p).card < c * ↑n ^ 2

number theoryA389241 · A234813 · A3901875 sources

declared disproved (Lean) · formalized · $10erdos:56

∀ {A : Finset ℕ}, Erdos56.WeaklyDivisible 0 A ↔ A = ∅

number theoryintersecting familyN/A5 sources

declared disproved (Lean) · formalized · $500erdos:90

Conjectured upper bound on how many pairs among

n

points in the plane can be exactly one unit apart.

geometrydistancesA1867055 sources

declared disproved (Lean) · formalized · $50erdos:105

False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}

geometryN/A5 sources

declared disproved (Lean) · formalizederdos:125

False ↔ ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity

number theorybase representationsA3670906 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared disproved (Lean) · formalizederdos:194

False ↔ ∀ k ≥ 3, ∀ (r : ℝ → ℝ → Prop), IsStrictTotalOrder ℝ r → ∃ s, s.IsAPOfLength k ∧ (List.Pairwise r s ∨ List.Pairwise (flip r) s)

arithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:198

∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2

additive combinatoricssidon setsarithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:199

False ↔ ∀ (A : Set ℝ), ThreeAPFree A → ∃ S, S.IsAPOfLength ⊤ ∧ S ⊆ Aᶜ

arithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:204

False ↔ ∃ n a, have D := {d | d ∣ n ∧ d > 1}; (∀ (x : ℤ), ∃ d ∈ D, x ≡ a d [ZMOD ↑d]) ∧ ∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x, x ≡ a d [ZMOD ↑d] ∧ x ≡ a d' [ZMOD ↑d']) → d.gcd d' = 1

covering systemsN/A5 sources

declared disproved (Lean) · formalizederdos:205

False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) n

number theorypossible6 sources

declared disproved (Lean) · formalizederdos:206

False ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), Erdos206.EventuallyGreedy x

number theoryunit fractionsN/A5 sources

declared disproved (Lean) · formalizederdos:209

False ↔ ∀ (d : ℕ), 4 ≤ d → ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))), A.card = d → (∀ L ∈ A, Erdos209.IsLine L) → ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) → (∀ (p : EuclideanSpace ℝ (Fin 2)), Erdos209.pointMultiplicity A p ≤ 3) → Erdos209.HasGallaiTriangle A

geometryN/A4 sources

declared disproved (Lean)erdos:231

Erdős problem 231

combinatoricsN/A3 sources

declared disproved (Lean) · formalizederdos:280

False ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)

number theorycovering systemsN/A5 sources

declared disproved (Lean) · formalizederdos:328

False ↔ ∀ (C : ℕ), 0 < C → ∃ t, ∀ (A : Set ℕ), (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) → ∃ P, ⋃ i, P i = A ∧ Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < C

number theoryadditive combinatoricsN/A4 sources

declared disproved (Lean) · formalizederdos:331

False ↔ ∀ (A B : Set ℕ), ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count A n)) → ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count B n)) → {(a₁, a₂, b₁, b₂) | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite

number theoryadditive combinatoricsN/A5 sources

declared disproved (Lean) · formalizederdos:333

False ↔ ∀ (A : Set ℕ), A.HasDensity 0 → ∃ B, A ⊆ B + B ∧ (fun N => ↑(B ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => √↑N

number theoryadditive basisN/A6 sources

declared disproved (Lean) · formalizederdos:337

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasis → ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) → Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTop

number theoryadditive combinatoricsadditive basisN/A5 sources

declared disproved (Lean) · formalizederdos:363

False ↔ {S | Erdos363.IsValidCollection S}.Finite

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:397

False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite

number theorybinomial coefficientsN/A7 sources

declared disproved (Lean) · formalizederdos:399

False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

number theoryfactorialsN/A5 sources

declared disproved (Lean) · formalized · $25erdos:426

False ↔ ∃ c, 0 < c ∧ ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, c * (2 ^ n.choose 2 / ↑n.factorial) ≤ ↑H.uniqueSubgraphCount

graph theorypossible5 sources

declared disproved (Lean) · formalizederdos:429

False ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (A : Set ℕ), A.Infinite → (∀ (N : ℕ), (A ∩ Set.Icc 1 N).ncard ≤ f N) → (∀ (p : ℕ), Nat.Prime p → ∃ b, ∀ a ∈ A, ↑a ≠ b) → ∃ n, ∀ a ∈ A, Nat.Prime (n + a)

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:453

False ↔ Erdos453.EventuallyHasPrimeWitness

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:505

∃ n S, Bornology.IsBounded S ∧ 0 < Metric.diam S ∧ ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)

geometrypossible5 sources

declared disproved (Lean) · formalizederdos:537

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ ε * ↑N → ∃ a₁ ∈ A, ∃ a₂ ∈ A, ∃ a₃ ∈ A, ∃ p₁ p₂ p₃, Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧ a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃

number theorypossible5 sources

declared disproved (Lean) · formalizederdos:613

False ↔ ∀ n ≥ 3, ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], G.edgeFinset.card = (2 * n + 1).choose 2 - n.choose 2 - 1 → ∃ B D, ∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n

graph theoryN/A5 sources

declared disproved (Lean) · formalizederdos:649

False ↔ ∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → ∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q

number theorypossible5 sources

declared disproved (Lean) · formalizederdos:666

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ H ≤ SimpleGraph.hypercube n, ε * ↑n * 2 ^ (n - 1) ≤ ↑H.edgeSet.ncard → (SimpleGraph.cycleGraph 6).IsContained H

graph theorypossible5 sources

declared disproved (Lean) · formalizederdos:692

False ↔ ∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∀ (n : ℕ), UnimodularOn (δ n) (n + 1)

number theorydivisorsN/A5 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 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 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 disproved (Lean) · formalizederdos:775

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

graph theoryhypergraphspossible5 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 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 disproved (Lean) · formalizederdos:867

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

additive combinatoricspossible5 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 disproved (Lean) · formalizederdos:897

False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun x => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) = ⊤ → Filter.limsup (fun n => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

number theoryN/A6 sources

declared disproved (Lean)erdos:927

Erdős problem 927

graph theorypossible3 sources

declared disproved (Lean) · formalizederdos:958

False ↔ ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → (EuclideanGeometry.distanceSet A).card = n - 1 ∧ Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) = Finset.Icc 1 (n - 1) → Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A

distancesgeometryN/A5 sources

declared disproved (Lean) · formalizederdos:967

False ↔ ∀ (a : ℕ → ℕ), StrictMono a → 1 < a 0 → (Summable fun k => 1 / ↑(a k)) → ∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0

number theoryanalysisN/A5 sources

declared disproved (Lean) · formalizederdos:990

False ↔ ∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.support.card * Real.log (Erdos990.M f))

analysisN/A6 sources

declared disproved (Lean) · formalizederdos:1034

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑n ^ 2 / 4 < ↑G.edgeSet.ncard → ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 2 - ε) * ↑n < ↑Y.card

graph theorypossible5 sources

declared disproved (Lean) · formalizederdos:1037

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) → (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard → ∃ s, Erdos1037.IsTrivialSet G s ∧ C * Real.log ↑n < ↑s.ncard

graph theoryN/A5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science