FormalizationCombinatoricsErdős #90
Erdős problem #90
Formalization of an existing proof. Contribution type: Formalization.
LFCR
Combinatorics · May 20, 2026
Erdős unit-distance conjecture
A fixed δ>0 and infinitely many n with ν(n)≥n^(1+δ), disproving that asymptotic conjecture.
Scope and what remains
A disproof does not determine the exact maximum. The later real sum-product disproof is a separate human follow-up.
Contributors
OpenAI's unnamed model generated the construction; the announcement names Noga Alon, Tim Gowers, Arul Shankar and Jacob Tsimerman as external readers. Later human extensions require their own credits.