Skip to content

Problems · Vela Mathematics Program

Narrowed todisproved ×formalized ×source:formal-conjectures ×Clear all

Problem ledger

14 problemsGraph view
declared disproved · formalized · $100erdos:43
If Sidon sets A,B⊆{1,…,N}A, B \subseteq \{1, \dots, N\} satisfy (A−A)∩(B−B)={0}(A-A) \cap (B-B) = \{0\}, must (∣A∣2)+(∣B∣2)≤(f(N)2)+O(1)\binom{|A|}{2} + \binom{|B|}{2} \le \binom{f(N)}{2} + O(1), where f(N)f(N) is the largest Sidon-set size in [N][N] - and can the bound be improved by a fixed proportion when ∣A∣=∣B∣|A| = |B|?
number theorysidon setsadditive combinatoricsA143824 · A227590 · A003022 · possible4 sources
declared disproved · formalized · $500erdos:92
sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))
geometrydistancespossible2 sources
declared disproved · formalizederdos:253
¬∀ (a : ℕ → ℕ), 0 < a 0 → Erdos253.RepresentsAPs a → Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) → subsetSums (Set.range a) ∈ Filter.cofinite
number theoryN/A2 sources
declared disproved · formalizederdos:266
¬∀ (a : ℕ → ℕ), ((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun x => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t))
irrationalityN/A2 sources
declared disproved · formalizederdos:442
False ↔ ∀ (A : Set ℕ), Filter.Tendsto (fun x => 1 / Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x) * ∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun x => 1 / (∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2 * ∑ nm ∈ (Erdos442.Set.bddProdUpper A x).toFinset, 1 / ↑(nm.1.lcm nm.2)) Filter.atTop Filter.atTop
number theoryN/A2 sources
declared disproved · formalizederdos:448
False ↔ ∀ (ε : ℝ), 0 < ε → {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1
number theorydivisorsA3974332 sources
declared disproved · formalizederdos:533
False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3
graph theoryN/A3 sources
declared disproved · formalizederdos:615
False ↔ ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum
graph theoryramsey theorypossible2 sources
declared disproved · formalizederdos:705
False ↔ ∃ k, ∀ (V : Set (EuclideanSpace ℝ (Fin 2))), V.Finite → (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3
graph theorychromatic numberN/A3 sources
declared disproved · formalizederdos:847
False ↔ ∀ (A : Set ℕ), Infinite ↑A → Erdos847.HasFew3APs A → ∃ n S, (∀ (i : Fin n), ThreeAPFree (S i)) ∧ A = ⋃ i, S i
additive combinatoricsN/A3 sources
declared disproved · formalizederdos:965
False ↔ ∀ (f : ℝ → Fin 2), ∃ A, ¬A.Countable ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≠ b → c ≠ d → f (a + b) = f (c + d)
ramsey theoryN/A2 sources
declared disproved · formalizederdos:1077
False ↔ ∀ ε > 0, ε < 1 → ∀ α > 0, α < 1 → ∀ᶠ (D : ℝ) in Filter.atTop, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑G.edgeSet.ncard > ↑n ^ (1 + α) → ∃ H, H.coe.IsBalanced D ∧ ↑H.verts.ncard > ↑n ^ (1 - α) ∧ ↑H.edgeSet.ncard > ε * ↑H.verts.ncard ^ (1 + α)
graph theoryN/A2 sources
declared disproved · formalizederdos:1092
False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)
geometrychromatic numberN/A5 sources
declared disproved · formalized · $50erdos:1128
False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ Erdos1128.IsMonochromaticBox f A₁ B₁ C₁
set theoryramsey theoryhypergraphsN/A2 sources