Skip to content

Problems · Vela Mathematics Program

Narrowed tosource:erdos-problems ×Clear all

Problem ledger

1,217 problems · 12/25NumberSourcesGraph view
declared decidableerdos:551
Erdős problem 551
graph theoryramsey theoryN/A
declared openerdos:552
Erdős problem 552
graph theoryramsey theoryA006672
declared provederdos:553
Erdős problem 553
graph theoryramsey theoryA000791 · possible
declared openerdos:554
Erdős problem 554
graph theoryramsey theorypossible
declared openerdos:555
Erdős problem 555
graph theoryramsey theoryA389313 · possible
declared decidableerdos:556
Erdős problem 556
graph theoryramsey theoryA389335
declared openerdos:557
Erdős problem 557
graph theoryramsey theoryN/A
declared openerdos:558
Erdős problem 558
graph theoryramsey theorypossible
declared disprovederdos:559
Erdős problem 559
graph theoryramsey theorypossible
declared openerdos:560
Erdős problem 560
graph theoryramsey theorypossible
declared openerdos:561
Erdős problem 561
graph theoryramsey theoryN/A
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 openerdos:563
Erdős problem 563
graph theoryramsey theoryhypergraphsN/A
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 provederdos:565
Erdős problem 565
graph theoryramsey theorypossible
declared open · formalizederdos:566
True ↔ ∀ (p : ℕ) (G : SimpleGraph (Fin p)), (∀ (S : Finset (Fin p)), 2 ≤ S.card → (SimpleGraph.induce (↑S) G).edgeSet.ncard ≤ 2 * S.card - 3) → ∃ c > 0, ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj], (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncard
graph theoryramsey theoryN/A2 sources
declared open · formalizederdos:567
True ↔ Erdos567.Q3.IsRamseySizeLinear
graph theoryramsey theoryN/A2 sources
declared openerdos:568
Erdős problem 568
graph theoryramsey theoryN/A
declared openerdos:569
Erdős problem 569
graph theoryramsey theoryN/A
declared provederdos:570
Erdős problem 570
graph theoryramsey theoryN/A
declared openerdos:571
Erdős problem 571
graph theoryturan numberN/A
declared openerdos:572
Erdős problem 572
graph theoryturan numberpossible
declared openerdos:573
Erdős problem 573
graph theoryturan numberA006856
declared disprovederdos:574
Erdős problem 574
graph theoryturan numberpossible
declared openerdos:575
Erdős problem 575
graph theoryturan numberN/A
declared openerdos:576
Erdős problem 576
graph theoryturan numberpossible
declared provederdos:577
Erdős problem 577
graph theoryN/A
declared provederdos:578
Erdős problem 578
graph theoryN/A
declared open · formalizederdos:579
True ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), Erdos579.octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → c * ↑n ≤ ↑G.indepNum
graph theoryturan numberN/A2 sources
declared decidableerdos:580
Erdős problem 580
graph theoryN/A
declared solvederdos:581
Erdős problem 581
graph theorypossible
declared proved (Lean) · formalized · $100erdos:582
True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G
graph theoryramsey theoryN/A5 sources
declared falsifiableerdos:583
Erdős problem 583
graph theoryN/A
declared openerdos:584
Must every graph with nn vertices and δn2\delta n^2 edges contain large subgraphs in which every two edges lie on specified short cycles? A dense high-girth construction refutes the statement when δ\delta may shrink with nn.
graph theorycyclesN/A2 sources
declared openerdos:585
Erdős problem 585
graph theorycyclespossible
declared disprovederdos:586
Erdős problem 586
number theorycovering systemsN/A
declared solved · formalizederdos:587
∃ O > 0, ∃ O' > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos587.MaxNotSqSum N) ≤ O' * Real.nthRoot 3 ↑N * Real.log ↑N ^ O
number theoryA3720402 sources
declared open · $100erdos:588
Erdős problem 588
geometryA006065 · A008997
declared openerdos:589
Erdős problem 589
geometrypossible
declared proved · formalized · $250erdos:590
OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0) (Ordinal.omega0 ^ Ordinal.omega0) 3
set theoryramsey theoryN/A2 sources
declared proved · formalized · $250erdos:591
True ↔ OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) 3
set theoryramsey theoryN/A3 sources
declared open · formalized · $1000erdos:592
∀ (β : Ordinal.{u}), β.card ≤ Cardinal.aleph0 → OrdinalCardinalRamsey (Ordinal.omega0 ^ β) (Ordinal.omega0 ^ β) 3 ↔ sorry β
set theoryramsey theoryN/A2 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 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 open · formalizederdos:598
∀ (m : Type u_1) [Infinite m], True ↔ ∃ c, ∀ (X : Set m), Cardinal.mk ↑X = Erdos598.κ → c '' {s | ↑s ⊆ X} = Set.univ
set theoryramsey theoryN/A3 sources
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