Problems · Vela Mathematics Program

edges contain large subgraphs in which every two edges lie on specified short cycles? A dense high-girth construction refutes the statement when

declared openerdos:584

Must every graph with

n

vertices and

\delta n^2

\delta

may shrink with

n

graph theorycyclesN/A2 sources

declared openerdos:585

Erdős problem 585

graph theorycyclespossible

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 proved · formalizederdos:594

True ↔ ∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) → ∃ N, ∀ (k : ℕ), N ≤ k → ∃ v w, w.IsCycle ∧ w.length = 2 * k + 1

graph theoryset theoryN/A2 sources

declared open · formalized · $250erdos:595

True ↔ ∃ V, ∃ (_ : Infinite V), ∃ G, G.CliqueFree 4 ∧ ¬Erdos595.IsCountableUnionOfTriangleFree G

graph theoryset theoryN/A2 sources

declared open · formalizederdos:596

∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂), G₁.IsErdosHajnalExceptional G₂ ↔ (fun {U₁ U₂} => sorry) G₁ G₂

graph theoryramsey theoryset theoryN/A2 sources

declared openerdos:597

Erdős problem 597

graph theoryramsey theoryset theoryN/A

declared proved · formalizederdos:599

True ↔ ∀ (V : Type) (G : SimpleGraph V) (A B : Set V), Disjoint A B → G.IsIndepSet A → G.IsIndepSet B → ∃ ι a b p S, (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧ S ⊆ {v | ∃ i, v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

graph theoryset theoryN/A2 sources

declared open · formalizederdos:600

True ↔ ∀ (r : ℕ), 2 ≤ r → Filter.Tendsto (fun n => ↑(Erdos600.eFunction n (r + 1)) - ↑(Erdos600.eFunction n r)) Filter.atTop Filter.atTop

graph theorypossible2 sources

declared open · $500erdos:601

Erdős problem 601

graph theoryset theoryN/A

declared disproved (Lean)erdos:608

Erdős problem 608

graph theoryN/A2 sources

declared openerdos:609

Erdős problem 609

graph theoryramsey theorypossible

declared proved (Lean)erdos:610

Erdős problem 610

graph theorypossible4 sources

declared openerdos:611

Erdős problem 611

declared openerdos:612

Erdős problem 612

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

declared disproved (Lean) · formalizederdos:613

graph theoryN/A5 sources

declared openerdos:614

Erdős problem 614

graph theorypossible

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 openerdos:616

Erdős problem 616

graph theoryN/A2 sources

declared falsifiable · formalizederdos:617

∀ r ≥ 3, ∀ {V : Type} [inst : Fintype V] [DecidableEq V], Fintype.card V = r ^ 2 + 1 → ∀ (coloring : Sym2 V → Fin r), ∃ S k, S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

graph theoryN/A2 sources

declared proved (Lean) · formalizederdos:618

True ↔ ∀ (G : (n : ℕ) → SimpleGraph (Fin n)), (∀ (n : ℕ), (G n).CliqueFree 3) → ((fun n => ↑(G n).maxDegree) =o[Filter.atTop] fun n => ↑n ^ (1 / 2)) → (fun n => ↑(Erdos618.h2 (G n))) =o[Filter.atTop] fun n => ↑n ^ 2

graph theoryN/A5 sources

declared solved (Lean) · formalizederdos:619

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)

graph theoryN/A5 sources

declared openerdos:620

Erdős problem 620

graph theorypossible

declared proved (Lean) · formalizederdos:621

True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ), IsGreatest {k | ∃ A ⊆ G.edgeFinset, A.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → ({s(x, y), s(y, z), s(x, z)} ∩ A).card ≤ 1} a → IsLeast {k | ∃ T ⊆ G.edgeFinset, T.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → (T ∩ {s(x, y), s(y, z), s(x, z)}).Nonempty} t → 4 * (a + t) ≤ n ^ 2

graph theoryN/A5 sources

declared provederdos:622

Erdős problem 622

graph theorypossible

declared open · $1000erdos:625

Erdős problem 625

∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V) (k : ℕ), G.chromaticNumber = ↑k → G.CliqueFree k → ∀ (a b : ℕ), a ≥ 2 → b ≥ 2 → a + b = k + 1 → ∃ s, (SimpleGraph.induce s G).chromaticNumber ≥ ↑a ∧ (SimpleGraph.induce sᶜ G).chromaticNumber ≥ ↑b

declared openerdos:626

Erdős problem 626

graph theorychromatic numbercyclespossible

declared openerdos:627

Erdős problem 627

graph theorychromatic numberpossible

declared falsifiable · formalizederdos:628

graph theorychromatic numberN/A2 sources

declared openerdos:629

Erdős problem 629

graph theorychromatic numberpossible2 sources

declared provederdos:630

Erdős problem 630

declared provederdos:631

Erdős problem 631

declared disprovederdos:632

Erdős problem 632

declared provederdos:636

Erdős problem 636

declared provederdos:637

Erdős problem 637

declared openerdos:638

Erdős problem 638

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Sym2 (Fin n) → Fin 2), {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4

declared proved (Lean) · formalizederdos:639

graph theoryramsey theoryN/A5 sources

declared openerdos:640

Erdős problem 640

declared disprovederdos:641

Erdős problem 641

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

declared openerdos:642

Erdős problem 642

graph theorycyclespossible

declared openerdos:643

Erdős problem 643

graph theoryhypergraphspossible

declared disproved (Lean) · formalizederdos:666

graph theorypossible5 sources

declared openerdos:667

Erdős problem 667