An OpenAI reasoning model autonomously disproved Erdős’s 80-year-old unit distance conjecture, constructing point sets with n^(1+δ) unit-distance pairs, verified by external mathematicians.
Key Takeaways
The model disproved the conjecture that u(n) = n^(1+o(1)), producing configurations with at least n^(1+0.014) unit-distance pairs for infinitely many n.
The proof imported tools from algebraic number theory – infinite class field towers and Golod-Shafarevich theory – into a combinatorial geometry problem, a connection no one anticipated.
The prior lower bound dated to Erdős’s 1946 square grid construction; the upper bound O(n^(4/3)) has stood since Spencer, Szemerédi, and Trotter in 1984.
The chain of reasoning spanned 125 pages of summarized chain-of-thought; the model used no math-specific scaffolding or targeted training.
Fields medalist Tim Gowers and number theorist Arul Shankar both confirmed the result constitutes original mathematical discovery, not assistance.
Hacker News Comment Review
Debate around “LLMs just interpolate” framing is contested: commenters note the proof was produced in plain language without Lean verification, which undercuts the “pattern matching on formal systems” dismissal.
Several commenters observe Erdős problems dominate AI math headlines because they are easy to state and naturally benchmark first-generation AI math work, not because AI is uniquely suited to them.
There is broad agreement the bottleneck has shifted: the hard part was never computation but generating coherent long-range arguments; a 125-page reasoning trace resolving a frontier problem changes that prior.
Notable Comments
@trostaft: flags that the proof bypassed Lean entirely – plain language in and out – making it a stronger demonstration of raw reasoning than formal-verification narratives suggest.
@bananaflag: “Erdős problems are easier to state, thus they make a great benchmark for the first year of AI mathematics.”
