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.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/130.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Erdos130.erdos130_infinite_chromatic

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • argument

    VibeMathed

    Machine
    GPT-5.6 Star Fleet (Claude Fable 5 referee)
    Reported outcome
    partial
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page