Erdős Problem #90

Full solution by OpenAI internal model (20 May 2026). 3 AI contributions are recorded in all.

Problem
Erdős problem #90 (geometry, distances); current status: disproved (Lean)
Credit
OpenAI internal model · AI on its own
Checked
Listed in Tao's wiki
Timeline
First AI contribution 2026-05-20 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
SOLVEDPer Tao's AI-contributions wiki

The problem

Does every set of nn distinct points in R2\mathbb{R}^2 contain at most n1+O(1/log⁡log⁡n)n^{1+O(1/\log\log n)} many pairs which are distance 1 apart?

Statement quoted from erdosproblems.com/90, maintained by Thomas Bloom. Original source: [Er46b][Er61,p.243][Er75f,p.100][Er81,p.13][Er82e,p.61][Er83c,p.52][Er85,p.2][Er90,p.475][Er94b,p.267][Er95,p.14][Er97c,p.68][Er97e,p.528][Er97f,p.5][Va99,4.67]. Current status there: disproved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Humans Outcome
20 May, 2026 AI on its own OpenAI internal model — 🟢 Full solution
26 May, 2026 AI on its own Claude Mythos — 🟢 Full solution
21 May-9 Jun, 2026 AI working with humans GPT-5.5 Pro Ingo Althöfer, Michael Emmerich, Paata Ivanisvili, Tomasz Kania, leloy, mlewko, Eric Naslund, norxornor, Will Sawin, Carl Schildkraut, spiderduckpig, Tseng 🟢 Improved explicit bound

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎