Skip to content

Problems · Vela Mathematics Program

Narrowed todisproved (Lean) ×formalized ×source:vibemathed ×Clear all

Problem ledger

13 problemsGraph view
declared disproved (Lean) · formalizederdos:26
Let A⊂NA\subset\mathbb{N} be infinite. Must there exist some k≥1k\geq 1 such that almost all integers have a divisor of the form a+ka+k for some a∈Aa\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 AA such that for every k≥1k\geq 1 the set of multiples of A+kA+k has upper density below 0.340.34.
number theorydivisorsN/A6 sources
declared disproved (Lean) · formalized · $500erdos:90
Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.
geometrydistancesA1867055 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:205
False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) n
number theorypossible6 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:397
False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite
number theorybinomial coefficientsN/A7 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 p2+p+1p^2+p+1 for some prime pp. Alexeev and Mixon establish that {1,2,4,8}\{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:846
False ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A
geometryN/A6 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) · 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:1138
False ↔ ∀ C > 1, Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x => match x with | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y
number theoryprimespossible6 sources
declared disproved (Lean) · formalizederdos:1141
False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}
number theoryprimesA2145836 sources