---

Paul O'Donnell, High girth unit distance graphs, Ph.D. dissertation, Rutgers, The State University of New Jersey, New Brunswick; the title page is dated October 1999, and the page name carries the first day of that month because no day is printed. Page references below are to the dissertation. The result appeared in two papers: Paul O'Donnell, Arbitrary girth, 4-chromatic unit distance graphs in the plane. Part I: Graph description, Geombinatorics 9 (2000), no. 3, 145–150, and Part II: Graph embedding, Geombinatorics 9 (2000), no. 4, 180–193. The journal's archive lists them in its issues of January and April 2000 and holds no copies online; the page ranges follow the zbMATH records.

The result. Theorem 28 of the dissertation (Section 1.7.4, p. 26) states that for every $k\ge3$ there is a unit distance graph in the plane with girth $k$ and chromatic number $4$. The question asks for a $k$ such that every finite unit distance graph of girth at least $k$ is $3$-colorable. Theorem 28 gives, for each $k$, a finite graph of girth $k$ (hence of girth at least $k$) with $\chi=4$ and a unit distance embedding, so once its point set carries no unit distance other than the edges, which the paragraph on faithfulness below addresses, no such $k$ exists and the answer is no.

Definitions. O'Donnell's unit distance graphs are not the problem's. Section 1.2 (pp. 5–6) calls a placement of a graph's vertices at distinct points of the plane with adjacent vertices exactly at distance one a proper unit distance embedding, and a graph that has one a unit distance graph; non-adjacent vertices may also lie at distance one, and Section 1.3.5 removes only coincident vertices. The problem, and the formal-conjectures statement, use the faithful graph on a finite point set, with an edge exactly when the distance is $1$. A point set realizing O'Donnell's graph may therefore carry extra unit distances, whose faithful graph has more edges and possibly shorter cycles, so Theorem 28 alone does not give a faithful unit distance graph of girth $k$, although its chromatic number stays at least $4$.

The construction. By the theorem of Erdős and Hajnal (Theorem 25) there is, for every $k$ and $g$, a $k$-uniform $4$-chromatic hypergraph of girth $g$; O'Donnell takes $g>k/3$. Its vertices, the foundation vertices, stay an independent set, and each hyperedge receives a new $k$-cycle attached to it: the cycle's $k$ vertices are joined to the hyperedge's $k$ vertices by a perfect matching (Section 1.2, p. 5). For odd $k$, any $3$-coloring of the foundation vertices leaves a hyperedge monochromatic, and the odd cycle attached to it, whose vertices must avoid that color, cannot be colored with the remaining two colors; one color for the foundation vertices and three for the cycles suffice, so the graph has chromatic number exactly $4$ (Theorem 26). Every cycle other than an attached $k$-cycle passes through foundation vertices that consecutive attached cycles join, so they form a cycle of the hypergraph and the cycle has length at least $3g>k$; the girth is exactly $k$ (Theorem 27). The graph is then realized in the plane by the embedding procedure developed earlier in the dissertation for the girth-9 and girth-12 graphs: taking a hypergraph with the fewest vertices, O'Donnell $3$-colors all of its vertices but one with no monochromatic hyperedge, places each color class in a small ball around one of three centers $C_1,C_2,C_3$ and the last vertex in a small ball around a fourth center $C_4$, so that the vertices of every hyperedge lie in at least two of the balls, which is what the embedding lemmas need to attach every cycle at unit distance and to remove coincidences (Theorem 28, p. 26). For even $k$ a $k$-cycle is added to a $4$-chromatic unit distance graph of girth greater than $k$.

Faithfulness. The site's thread records the objection: a post of 2026-01-27 relays a reviewer's view, given on another site, that O'Donnell's construction is not faithful as the problem requires, and disagrees with it. The dissertation nowhere excludes unit distances between non-adjacent vertices, so the step from Theorem 28 to the faithful graph of the problem is supplied elsewhere: the Lean file linked above, whose header says that it reconstructs O'Donnell's attached-cycle construction and supplies an explicit finite generic perturbation proving that the realization can be chosen injective with no accidental unit non-edges. The curator's label, placed after that thread, is on the site's faithful statement.

Earlier partial constructions. Wormald (1979) built a $4$-chromatic unit distance graph of girth $5$ on $6448$ vertices; O'Donnell (1994) a $4$-chromatic unit distance graph of girth $4$ on $56$ vertices; Chilakamarri (1995) an infinite family of girth $4$ whose smallest member has $47$ vertices. These rule out $k\le5$ but leave the question open; Theorem 28 settles it for every $k$.

Acceptance. The site's curator, Thomas Bloom, labels the problem disproved and credits O'Donnell's dissertation; the label followed the site's thread of 2026-01-27, in which readers located Theorem 28 and the dissertation's text. The dissertation's result appeared in the two Geombinatorics papers of 2000, Part I describing the graphs and Part II embedding them, so the result is refereed. Feng and others (2026) list Problem 705 among the problems for which their Gemini-based research agent, Aletheia, pointed to existing literature, namely O'Donnell's work (source card); that is a literature pointer, not a new result. This page states Theorem 28 and its proof outline (pp. 25–26) and does not restate the embedding lemmas of Sections 1.3–1.6 that the proof invokes.

Formalization. A third party formalized the solution: not_erdos_705 in src/latest/ErdosProblems/Erdos705.lean of https://github.com/plby/lean-proofs, Boris Alexeev's repository, pinned above at the commit of 2026-09-15 (the proof entered the repository on 2026-08-16). The file declares itself a Lean formalization of a solution to the problem, names Paul O'Donnell as informal author and Codex and GPT-5.6 Sol as formal authors, so it is a link on this page rather than an independent claim. Its theorem states, for the faithful graph UnitDistancePlaneGraph V on a finite set $V$ of points of the Euclidean plane, that no $k$ makes every such graph of girth at least $k$ $3$-colorable; the perturbation step described above is part of the file. It imports only Mathlib and the repository's own utilities and contains no sorry. The formal-conjectures catalog (the record link, pinned to the commit of 2026-09-18 that added the pointer) tags its statement erdos_705 as research solved and cites this file as the formal proof. This repository has not built the file, printed its axioms or audited its definitions against the problem, so the claim carries no formalized evidence.