Overview
- OpenAI says an internal general-purpose reasoning model autonomously produced a roughly 125‑page proof that disproves Paul Erdős’s planar unit distance conjecture, a result first announced on Wednesday.
- The proof constructs an infinite family of planar point sets that achieve about n^(1+0.014) unit‑distance pairs, a quantified superlinear improvement over long‑standing grid constructions.
- Multiple outside experts, including Tim Gowers and Will Sawin, reviewed and helped formalize the argument and Sawin provided a refined quantitative statement.
- OpenAI reports the argument has been formalized in the Lean proof assistant and submitted for journal consideration, but the company has not released the model’s raw reasoning and full peer review is still pending.
- If sustained, the result could shift how research and formal verification are done by showing AI systems can link distant fields such as algebraic number theory and geometry, yet it also spotlights the need for open data, independent audits, and careful validation before wider adoption.