Erdős problem 1067 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1067.lean

Retained formal statement1 of 2

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

Komjáth [Ko13] proved that it is consistent that the answer is no. This was improved by Soukup [So15], who constructed a counterexample using no extra set-theoretical assumptions. A simpler elementary example was given by Bowler and Pitz [BoPi24].

This was formalized in Lean by Alexeev using Aristotle and Aleph Prover.

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.

Sources

Search problems.science