Erdős unit-distance problem

Unit-distance conjecture disproved

Model / AI: OpenAI (unreleased), Sol

an OpenAI reasoning model disproved Erdős's 1946 conjecture by constructing point sets with at least n^(1+δ) unit distances, for a fixed δ > 0 and infinitely many n; outside mathematicians checked it and wrote companion remarks. An early Lean development rested on named classical inputs; Boris Alexeev then had OpenAI's Sol autoformalize the result assuming nothing beyond the axioms of mathematics, about 1.2M lines, which Buzzard compiled himself.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Paper — Unit-distance conjecture disproved
• Paper — companion remarks
• Lean — Lean development
• Context — Buzzard compiled himself