Erdős Problem #90

The problem

Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $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.

∎