An explicit lower bound for the unit distance problem

An AI model disproved a 1946 Erdős conjecture, confirmed by an independent mathematician

what the source states

Sawin's abstract states that sets of n points exist in the plane containing more than n^1.014 pairs at unit distance, and that this "improves on very recent work of a team at OpenAI, who proved the same result with an inexplicit exponent greater than 1, drastically improving on the best previous lower bound and disproving a conjecture of Erdős." Per Sawin's paper, the OpenAI work was carried out by Lijie Chen using an internal model, with Mark Sellke and Mehtaab Sawhney verifying correctness.

what we infer

This is the load-bearing verification for the whole AI-mathematics line, and it is deliberately anchored on Sawin rather than on OpenAI's announcement: an independent working mathematician states the result in his own paper and builds on the construction, so the fact does not rest on a company's word about its own unreleased model. As evidence it is filed against ORCH-C040 because it is the strongest available instance of a machine producing genuinely new research-level mathematics. Its force is bounded by the scoping recorded on ORCH-C041: it bears on the motivation rung only, and the Penrose-side response (ORCH-E025) contests whether a novel result inside an existing framework touches the argument at all.

limitations

• Preprint, not journal-published at import.
• Attribution of the original result depends on Sawin's characterization plus Quanta reporting; the OpenAI announcement page itself timed out on two direct fetch attempts and was not read by this import.
• The model is internal and unreleased, so the process that produced the result cannot be independently examined.
• Bears on the Gödelian motivation only — no bearing whatever on microtubule, anesthesia, or collapse claims.