Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×hypergraphs ×Clear all

Problem ledger

8 problemsGraph view
declared open · formalizederdos:562
True ↔ ∀ r ≥ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑n
graph theoryramsey theoryhypergraphspossible2 sources
declared open · formalized · $500erdos:564
True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ 2 ^ (c * n) ≤ ↑(Combinatorics.hypergraphRamsey 3 n)
graph theoryramsey theoryhypergraphspossible2 sources
declared open · formalized · $500erdos:593
Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.
set theorygraph theoryhypergraphsN/A4 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 verifiable · formalizederdos:835
∀ {k : ℕ}, 3 ≤ k → k ≤ 8 → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber
graph theoryhypergraphsN/A3 sources
declared proved (Lean) · formalizederdos:1022
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
combinatoricshypergraphspossible6 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