Problems · Vela Mathematics Program

declared proved (Lean)erdos:716

Erdős problem 716

graph theoryhypergraphspossible3 sources

declared provederdos:717

Erdős problem 717

declared provederdos:718

Erdős problem 718

declared openerdos:719

Erdős problem 719

graph theoryhypergraphspossible

declared proved · $100erdos:720

Erdős problem 720

declared not provableerdos:736

Erdős problem 736

declared provederdos:737

Erdős problem 737

declared openerdos:738

Erdős problem 738

declared not provableerdos:739

Erdős problem 739

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe r

declared open · formalizederdos:740

graph theorychromatic numberN/A2 sources

declared decidable · formalizederdos:742

∀ (a b : ℕ), (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b

graph theoryN/A2 sources

declared falsifiableerdos:743

Erdős problem 743

graph theoryN/A2 sources

declared disprovederdos:744

Erdős problem 744

declared provederdos:745

Erdős problem 745

declared provederdos:746

Erdős problem 746

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

declared proved (Lean) · formalizederdos:750

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

declared disproved (Lean) · formalizederdos:751

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

declared provederdos:752

Erdős problem 752

graph theorycyclesN/A

declared disproved (Lean) · formalizederdos:753

declared solvederdos:758

Erdős problem 758

declared solvederdos:759

Erdős problem 759

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

declared proved (Lean) · formalizederdos:760

declared openerdos:761

Erdős problem 761

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

declared disproved (Lean) · formalizederdos:762

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

declared solved (Lean)erdos:765

Erdős problem 765

graph theoryturan numberA0068553 sources

declared openerdos:766

Erdős problem 766

graph theoryturan numberpossible

declared provederdos:767

Erdős problem 767

graph theoryturan numberpossible

declared disproved (Lean) · formalizederdos:775

graph theoryhypergraphspossible5 sources

declared solvederdos:777

Erdős problem 777

graph theorycombinatoricsN/A

declared openerdos:778

Erdős problem 778

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

declared disproved (Lean) · formalizederdos:794

graph theoryhypergraphsturan numberN/A5 sources

declared provederdos:797

Erdős problem 797

declared provederdos:799

Erdős problem 799

declared provederdos:800

Erdős problem 800

graph theoryramsey theoryN/A

declared provederdos:801

Erdős problem 801

graph theoryramsey theoryN/A

declared openerdos:802

Erdős problem 802

declared disprovederdos:803

Erdős problem 803

declared disprovederdos:804

Erdős problem 804

graph theorypossible

declared openerdos:805

Erdős problem 805

graph theorypossible

declared disprovederdos:807

Erdős problem 807

additive combinatoricsgraph theoryN/A

declared disprovederdos:808

Erdős problem 808

declared openerdos:809

Erdős problem 809

declared openerdos:810

Erdős problem 810

declared openerdos:811

Erdős problem 811

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + c

declared open · formalizederdos:812

graph theoryramsey theoryA0594422 sources

declared openerdos:813

Erdős problem 813

graph theorypossible

declared provederdos:814

Erdős problem 814

graph theorypossible

declared disprovederdos:815

Erdős problem 815