Erdős problem 130 · problems.science

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

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

130.lean

Retained formal statement1 of 1

Let $A\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 $A$ , 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

1True ↔2  ∃ A,3    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.

Sources

Search problems.science