Overview
- An OpenAI reasoning model produced a construction of planar point sets that yields more unit‑distance pairs than the classic conjectured bound, refuting a formulation of Paul Erdős's unit distance problem.
- OpenAI researchers and outside mathematicians checked the argument, formalized the proof in the Lean proof assistant, and have submitted the work to academic journals for review.
- The construction mixes algebraic number theory with discrete geometry in ways human researchers had largely dismissed, and other mathematicians have already refined the quantitative bounds using the same ideas.
- Prominent figures in mathematics, including Timothy Gowers, Noga Alon, and Daniel Litt, publicly praised the result after human verification efforts confirmed the core argument.
- Key verification gaps remain because OpenAI has not released the model's raw chain‑of‑thought and the paper is still awaiting full independent peer review, prompting debate over standards for validating AI‑produced mathematics.