OpenAI said on May 20 that an internal reasoning model had generated a proof refuting the unit distances conjecture, a planar geometry problem posed by Paul Erdős in 1946. The proof constructs infinite families of point sets with at least n^{1+δ} unit-distance pairs for some fixed δ > 0, overturning the long-standing view that the maximum number of such pairs among n points could not substantially exceed n^{1+o(1)}.
The announcement differed sharply from the company’s October 2025 claim, when a vice president said GPT-5 had solved ten Erdős problems. Thomas Bloom, the mathematician who curates the official problems database, dismissed that claim as a “dramatic misrepresentation” because the model had only retrieved solutions already in the literature. This time, nine external mathematicians verified the AI-generated counterexample, and Bloom’s website now lists problem #90 as refuted.
OpenAI released an 18-page PDF with the demonstration and a second document signed by Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood. The signatories described the paper as a “human-verified version” of the AI’s output, noting the raw output had been checked, rewritten, and contextualized.
The same day, mathematician Will Sawin, a signatory of the verification note, independently posted a preprint on arXiv that sharpened the result. Sawin’s work gave an explicit lower bound of more than n^{1.014} unit-distance pairs, compared with the non-explicit exponent in OpenAI’s original proof. The best known upper bound remains O(n^{4/3}), established by Spencer, Szemerédi, and Trotter in 1984. The new refutation does not determine the exact asymptotic maximum; it leaves a gap between the new lower bound and that 41-year-old ceiling.
The validation process marked a clear departure from the discredited October announcement. OpenAI’s vice president Kevin Weil had claimed GPT-5 solved ten Erdős problems; Bloom called it a misrepresentation because the model merely replicated known solutions. The nine mathematicians’ verification, and the database update, converted what would otherwise be another unreviewed company claim into a citable mathematical result.
OpenAI said a general-purpose model produced the initial proof autonomously, without domain-specific fine-tuning, through an automated loop of instruction drafting and scoring before human review. The company did not disclose the model’s name, the number of attempts, the compute budget, or complete logs. The mathematicians’ accompanying note stressed that the final exposition contained human contributions, as the AI’s output was rewritten and contextualized.
Several questions remain open: which model generated the proof, how the automated verifier was designed, how many runs were needed, and whether the mathematicians examined the raw AI output or an edited version. The result has not undergone formal peer review at a journal or been verified in a proof assistant such as Lean or Coq. The broader mathematical community, beyond the nine signatories, has yet to react independently.
Even with those caveats, the episode demonstrates that rigorous expert vetting can transform a premature corporate announcement into a credible mathematical advance. It shows that AI can contribute a novel disproof to an open problem when embedded in a process of human scrutiny, but it also underscores the distance between generating a counterexample and autonomous scientific discovery. For investors and strategists tracking AI’s progression toward reliable reasoning, the milestone is real but narrow: a single conjecture felled, not a general-purpose mathematician.