OpenAI Model Produces Counterexample to Erdős's Unit-Distance Conjecture

OpenAI reports that an internal general-purpose reasoning model produced a counterexample to Erdős's conjectured near-linear upper bound for planar unit distances. The proof constructs infinitely many $n$-point configurations with at least $n^{1+\delta}$ unit-distance pairs for some fixed $\delta>0$, contradicting the proposed $n^{1+o(1)}$ behavior; it does not close the remaining gap to the known $O(n^{4/3})$ upper bound.

The official proof states that the problem was solved in a completely automated fashion: the model received an AI-written problem statement, its response was evaluated by an AI grading pipeline, and human researchers began examining it afterward. The manuscript records subsequent AI-assisted verification and rewriting, while a companion paper by Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood gives a human-digested and human-verified argument; that paper also says Codex assisted expository refinement.

OpenAI does not disclose the internal model's product name or version. The proof, companion remarks, and rewritten reasoning trace are public, and the official materials document external mathematical checking, but the result remains recorded here as an unverified counterexample rather than as an OpenTCS endorsement.

Sources: OpenAI announcement thread · OpenAI technical announcement

Related Materials: Planar Point Sets with Many Unit Distances · Remarks on the Disproof of the Unit Distance Conjecture · Rewritten Chain of Thought for the Solution