OpenAI claims a general-purpose reasoning model found a counterexample to Erdos's unit-distance bound [D]

OpenAI posted a math result today claiming that 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. Announcement: Proof PDF: Abridged reasoning writeup: The mathematical claim, as I understand it, is that there are finite planar point sets with than n^{1+δ} unit distances for some fixed δ > 0 and infinitely many n. That would rule out the expected near-linear upper bound, though it does not determine the true asymptotic growth rate.