Disproof of the Erdős unit-distance conjecture
A reasoning model produced the core construction disproving a 1946 conjecture in discrete geometry, finding point configurations with more unit-distance pairs than the conjecture permitted.
- Lab
- OpenAI
- Model
- GPT-5 series reasoning model
- Field
- Mathematics
- Date
- 2026-05-20
- Problem posed
- 1946 · open 80 yrs
What was found
The model produced a construction beating the conjectured bound, with an inexplicit exponent greater than 1. Nine mathematicians - Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood - published a human-verified version of the argument; Sawin separately made the exponent explicit at n^1.014. Gowers called it 'the first example of a result produced autonomously by an AI that I find exciting in itself.'
Novelty check
The unit-distance problem dates to Erdős (1946). Prior bounds were well documented; the construction is new.
Caveats and known objections
Human mathematicians shaped the problem framing and verified the construction. The explicit n^1.014 exponent is Sawin's refinement, not the model's output: the model's own bound was inexplicit. The strength of the endorsement from Gowers is notable but is a judgment, not a formal check.
Machine-checked elsewhere
PalomarPALOMAR-2026-08-08-000001
kim-em/erdos-unit-distance-comparator at be6c2ee4c9fb · checked 2026-08-14
ProvedUnitDistance.erdos_unit_distance_uniform_constant_false
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Palomar's record describes this as certifying the literal negation of the uniform-constant form of the conjecture, from a Mathlib-only statement of that negation. That is narrower than this entry's claim, which is why the entry stays at independently checked rather than moving to formally verified.
The open problem
MathDBErdős unit-distance conjecture
315785
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
History of this entry
- CorrectedRecorded the MathDB record for this result as a registration.
- CheckedPalomar registered Kim Morrison's comparator wrapper as PALOMAR-2026-08-08-000001, a machine-checked formalization by someone outside the group that produced the writeup. The verification grade did not move: what is proved formally is the uniform-constant form, which is narrower than this entry's claim. source ↗
- AddedEntered the registry graded Independently checked and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded independently checked for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Disproof of the Erdős unit-distance conjecture. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-05-erdos-unit-distanceBibTeX
@misc{whataifound-openai-2026-distance,
title = {Disproof of the Erdős unit-distance conjecture},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Independently checked. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-05-erdos-unit-distance}
}