OpenAI says one of its general-purpose reasoning models found a construction disproving the conjectured n\^{1+O(1/log log n)} upper bound in Erdős’s planar unit-distance problem.
The linked post includes a proof PDF and an abridged chain-of-thought writeup. The proof statement says the original model output was later checked by an AI grading pipeline and by mathematicians, and that Will Sawin simplified and strengthened the argument.
The mathematical claim, as I understand it, is that there are finite point sets in the plane with more than n\^{1+δ} unit distances for some fixed δ > 0 and infinitely many n, so the expected near-linear upper bound cannot hold. The true growth rate is still open, with the classical upper bound around O(n\^{4/3}).
Curious what people here think of the construction itself, especially the use of Golod-Shafarevich/class-field-tower ideas in what looks at first like a discrete geometry problem.