Erdős problem 1067

Does every graph with chromatic number $\aleph_1$ contain an infinitely connected subgraph with chromatic number $\aleph_1$ ?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1067.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1067.leanErdos1067.erdos_10673 linesExact file

1False ↔2  ∀ (V : Type) (G : SimpleGraph V),3    G.chromaticCardinal = Cardinal.aleph 1 → ∃ H, H.coe.chromaticCardinal = Cardinal.aleph 1 ∧ H.coe.InfinitelyConnected

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:1067
PLBY Lean proofsErdosProblems.Erdos1067

Reported activity

Reported by these sources. Not reviewed here.

Formalization
Erdős AI contributions wiki · 28 Jan, 2026
Machine
Aleph Prover, Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry