Skip to content

Erdős problem 130

For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

130.lean

Retained formal statement1 of 1

Let A⊂R2A\subset\mathbb{R}^2 be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in AA, where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?

The chromatic number can be infinite: there is an infinite general-position set whose integer-distance graph admits no finite proper colouring. How large the *clique* number can be is not addressed here.

FormalConjectures/ErdosProblems/130.leanErdos130.erdos_1303 linesExact file
True ↔  ∃ A,    A.Infinite ∧ EuclideanGeometry.InGeneralPosition A ∧ (SimpleGraph.IntegerDistancePlaneGraph A).chromaticNumber = ⊤
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.