Remarks on the Disproof of the Unit Distance Conjecture ↗
Near-linear Euclidean conjecture refuted · observed Oct 13, 2026
Source status dated May 20, 2026 · observed Oct 13, 2026
The n^(1+o(1)) upper bound, not the exact extremal growth.
Publication v5
Record details
Erdős unit-distance problem →Coverage & review
Coverage of this curation
Original question, distinct results, proof provenance, selected history and an explanatory schematic.
Formal proofs: A pinned Lean submission reports the asymptotic counterexample with exact Euclidean pair counting. External execution and independent OpenMath review remain pending.
AI-assisted work: OpenAI’s unnamed internal model generated the original construction. The nine companion-paper authors provide human exposition and checking; Will Sawin’s announced exponent refinement has separate credit. The plby/Erdos90 project supplies the linked formal submission; its checked README does not identify an individual formalization author.
Search scope & review
Selected primary papers, exact formal declarations, project provenance and official descriptions checked on 13 October 2026.
Checked Oct 13, 2026 · independent review pending.
- Selected evidence and literature; independent mathematical review and external proof execution remain pending.
General status observations
Source identities & rights
Erdős problem 90: unit distances ↗
Erdős Problems · metadata-link · Original source license and document rights apply.
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished. Rights / source terms
1 cited entry · exact source identity
- Version
- erdos-unit-distances:source:question:v1
- Revision
- Observed 2026-10-13
- Content SHA-256
- 69f159e038a00a4e2accd2859c543fae19cb8588517a91d40dfd93482a799f93
- Source update
- Unavailable
- Observed
- 2026-10-13
- Check cadence
- 90 days
- Problem 90; historical question and background ↗
erdos-unit-distances:entry:question:v1
Planar Point Sets with Many Unit Distances ↗
OpenAI · metadata-link · Original source license and document rights apply.
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished. Rights / source terms
1 cited entry · exact source identity
- Version
- erdos-unit-distances:source:proof:v1
- Revision
- 2026-05-20
- Content SHA-256
- 62b5de8cacdfbc0f13ae1940aa81659cd233e6945b936612fbeab0ab8ab3d383
- Source update
- Unavailable
- Observed
- 2026-10-13
- Check cadence
- 90 days
- Theorem 1.1 and Statement on AI Use ↗
erdos-unit-distances:entry:proof:v1
Remarks on the Disproof of the Unit Distance Conjecture ↗
Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, Melanie Matchett Wood · metadata-link · Original source license and document rights apply.
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished. Rights / source terms
1 cited entry · exact source identity
- Version
- erdos-unit-distances:source:remarks:v1
- Revision
- 2026-05-20
- Content SHA-256
- 7c2f90d0792d05503d326102321743340790209a12ceb9ead923f357df7be45f
- Source update
- Unavailable
- Observed
- 2026-10-13
- Check cadence
- 90 days
- Theorem 1.1; Sections 1.1–1.3 and 2 ↗
erdos-unit-distances:entry:remarks:v1
OpenAI unit-distance announcement ↗
OpenAI · metadata-link · Original source license and document rights apply.
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished. Rights / source terms
1 cited entry · exact source identity
- Version
- erdos-unit-distances:source:announcement:v1
- Revision
- 2026-05-20
- Content SHA-256
- a9595610782b273048827b1d87bc81b4ed99298722f08bd1f967c7ee469b9559
- Source update
- Unavailable
- Observed
- 2026-10-13
- Check cadence
- 90 days
- The unit distance problem; mathematicians on the result ↗
erdos-unit-distances:entry:announcement:v1
Unit-distance counterexample in Lean ↗
plby/Erdos90 project · metadata-link · Original source license and document rights apply.
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished. Rights / source terms
1 cited entry · exact source identity
- Version
- erdos-unit-distances:source:lean:v2
- Revision
- 2062b0e6c9770c81e397bfe41148e90b92ca0567
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-13
- Check cadence
- 90 days
- src/submission/Submission.lean; ChallengeDeps.lean pair-count definition ↗
erdos-unit-distances:entry:lean:v2
Publication history
- Problem ID
- problem-erdos-unit-distances
- Publication checksum
- 28cae28b13039a92e6166d245c24630f0964e73b18f30707e69668f9a870588d
- Published
- 2026-10-13T19:35:02.812984+00:00
- Publication reason
- Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 1 · Oct 13, 2026
Source-linked pilot import; independent mathematical review remains pending.
- Version 2 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 3 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 4 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 5 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 6 · Oct 21, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.