News · August 2026 · 4 min read
A conjecture mathematicians had believed since 1946 turned out to be wrong — and an AI model found the counterexample.
Paul Erdős posed the unit distance problem in 1946: if you scatter a set of points across a flat plane, what's the largest number of point-pairs that can sit exactly one unit apart? For nearly 80 years, mathematicians broadly assumed simple square-grid arrangements were about as good as it gets.
Earlier this year, an OpenAI research model found otherwise. It produced an infinite family of point arrangements that beat the square-grid assumption, built on a genuinely unexpected connection to algebraic number theory rather than a straightforward geometric trick. External mathematicians reviewed the argument, and one of the refinements to the result came from a mathematician at Princeton who tightened the model's original bound.
The more interesting part is what happened next: the entire proof was translated into Lean, a system that checks mathematical arguments step by step in a way a computer can verify, rather than relying purely on human reviewers reading through it. That translation was completed within about a week by a separate team, and it means the result doesn't rest on trusting the AI's reasoning at face value — every logical step can be independently confirmed by machine.
That distinction matters more than the specific problem. AI tools have spent the last couple of years mostly demonstrating that they could complete well-defined tasks faster than people. A machine-checked, genuinely novel proof of a problem that had resisted expert mathematicians for eight decades is a different kind of claim — it's a case of an AI system contributing something new to one of the fields with the least tolerance for hand-waving.
This isn't an isolated event. Formal-verification tools built specifically to check AI-generated proofs are actively being developed and used to formalize other results, including problems from Erdős's broader body of open questions. As that verification infrastructure matures, it lowers the risk that "AI solved a hard problem" turns out to mean "AI produced something that looked right until someone checked it closely" — which has been a real failure mode in the field before.
Worth watching in the coming months: whether the formal proof survives full peer review, and whether this becomes a repeatable pattern rather than a one-off headline.