---

Claim. The particular question of Problem 130, whether the chromatic number of the integer-distance graph can be infinite, is answered yes. The manuscript Integer-Distance Graphs in General Position by Lloyd.H asserts that there is a countably infinite set $A\subseteq\mathbb R^2$ with no three points on a line and no four on a circle whose integer-distance graph $G(A)$ is a disjoint union of finite connected triangle-free graphs of unbounded chromatic number, so that

$$\chi(G(A))=\aleph_0 \qquad\text{and}\qquad \omega(G(A))=2 .$$

The argument, as the claim's summary describes it, has four stages. Finite triangle-free graphs of large chromatic number are taken as induced subgraphs of Johnson graphs, found by a container-and-sampling argument. Each such graph is realized as a point set through a parametrization by products of complex numbers with rational coordinates, chosen so that the edges have rational lengths while one simultaneous specialization keeps every non-edge length irrational and avoids all collinear and concyclic triples and quadruples; a scaling then makes exactly the edge lengths integers. Finally the finite components are placed by translations, one after another, so that no integer distance and no collinearity or concyclicity arises across components. The witness is a specific set, and its clique number $2$ says nothing about other admissible sets.

Submission note. Posted to erdosproblems.com as a proof claim by Lloyd.H (account Lherdos) on 17 July 2026, giving "Gpt 5.6 Sol Ultra" as the AI used:

We claim that there is a countably infinite set $A\subseteq\mathbb R^2$ in full general position whose integer-distance graph is a disjoint union of finite connected triangle-free graphs with unbounded chromatic numbers. The finite components are induced subgraphs of Johnson graphs, obtained by a container-and-sampling argument. A rational complex-product parametrization realizes each component faithfully: edges have rational lengths, while simultaneous specialization keeps every nonedge length irrational and avoids all collinear or concyclic degeneracies. Scaling then makes exactly the edges integral. Finally, the components are translated inductively so that no cross-component integral distances or mixed degeneracies occur. Thus $\chi(G(A))=\aleph_0$ and $\omega(G(A))=2$.

Covers. The second, particular question: the chromatic number of the graph can be infinite, and even for a triangle-free graph with finite components, and, since the chromatic number never exceeds $\aleph_0$, the chromatic-number half of the first question. The first question's clique-number part is not settled: the witness has clique number $2$, and the claim does not determine how large the clique number can be as the set ranges over all infinite sets in this general position; Anning and Erdős's theorem, recorded on the problem page, excludes only an infinite complete subgraph.

Depends on. No page of this wiki.

Claimant and postings. The claim was posted on the site's proof-claims tab for the problem on 17 July 2026 from the account Lherdos and is credited there to Lloyd.H, with the AI system named on the tab as Gpt 5.6 Sol Ultra; the repository's own disclosure names OpenAI Codex as used for the proof, the Lean development and the manuscript. The manuscript's byline prints its author as "LLOYD.H", the name the tab credits rather than the account's name, so the page lists Lloyd.H as the author. The manuscript and the Lean sources are hosted in the GitHub repository cat-stack-boop/erdos-130-lean, linked above at its revision of 19 July 2026, whose last change narrows the stated scope to a partial solution. The repository's README reports a Lean 4 development pinned to Lean 4.30.0-rc2 and a fixed Mathlib revision, with the public declarations Erdos130.erdos_problem_130_partial (the affirmative answer to the infinite-chromatic question), Erdos130.erdos_problem_130_strong_partial (the witness with finite components, exact chromatic cardinal and clique number two) and Erdos130.finite_specialization (the faithful finite realization), and reports that their axiom closures are propext, Classical.choice and Quot.sound only. None of these files was built or audited by this corpus, nor were the formal statements compared with the problem's wording, so the page lists no formalized evidence.

Acceptance. None documented. The site labels the problem OPEN and its page does not credit the result. The claim was submitted on the tab as a full solution; on 17 July 2026 a commenter reported rebuilding the Lean development from a clean clone and checking its axioms, and noted that the clique-number question stays open, and on 19 July 2026 a site moderator changed the claim to a partial one after the claimant asked about its scope. Neither comment is acceptance: the first is a third-party build report, not a review of the manuscript, and the second concerns the claim's scope. No journal record, arXiv posting or review of the manuscript is known. The claim is therefore claimed. Another Lean proof of the same particular question, by a different construction, is Star Fleet Math's development, posted on its site by 15 July 2026, two days before this claim (its claim page), which the formal-conjectures catalog links as the statement's formal proof; neither development is known to cite the other.