The unit distance problem is a well-known question in discrete geometry first posed by Paul Erdős in 1946. Erdős himself posed a conjecture defining an upper bound for the problem and offered $500 for a proof or disproof. This week OpenAI published a paper demonstrating that an internal model had disproved the conjecture. Days later, Anthropic shared an independent disproof derived by their internal Mythos model without access to the internet.

On May 20, 2026, a team including Noga Alon, Timothy Gowers, and Will Sawin published a paper in which an OpenAI model had contributed the core construction in a disproof of Erdős's unit-distance conjecture. The paper ran 125 pages. Six days later, Anthropic announced that Claude Mythos had independently found its own disproof: shorter, more elegant but slightly weaker than the earlier result.

This is an account of how these systems work, what they proved, and what the proofs mean for the future of mathematics.

Paul Erdős and the Problems That Outlived Him

Paul Erdős (1913–1996) was the most prolific mathematician of the twentieth century. Over the course of his career he published more than 1,500 papers with more than 500 co-authors. His work touched on so many fields that a mathematician's Erdős number functions as a citation graph: if you collaborated with Erdős directly your number is 1; collaborate with someone who did and it is 2. Most working mathematicians have an Erdős number.

Erdős was famously itinerant, and his work posing and solving discrete problems across fields secured his place as the prototypical example of what W.T. Gowers (a coauthor on the OpenAI paper) famously termed the "problem-solver" mathematician, which Gowers contrasted with the "theory-builder." For problems he thought were particularly difficult or interesting Erdős would offer small monetary rewards for solutions, and, since his death in 1996, these rewards have become a kind of short-hand for the difficulty of a given Erdős problem.

In 2015 a group of five mathematicians solved the only $10,000 Erdős problem, on prime gaps. A photograph taken 30 years earlier in 1985 shows Erdős and one of those mathematicians, Terry Tao, then 10 years old, contemplating a problem from combinatorics together on the vinyl chairs of the University of Adelaide. That problem, solved by two other mathematicians in 2010 and more complicated than Erdős may have realised, might properly have been a $250 problem.

The Erdős–Straus conjecture, still open, states that for every integer the fraction decomposes into three unit fractions:

for positive integers .

Computers have confirmed the decomposition for every , yet no general proof exists for arbitrary . Erdős attached a $50 bounty to the problem, and eighty years later the check still has not been cashed. It is one of hundreds of conjectures from his catalogue that remain open.

The Unit-Distance Conjecture: Eighty Years

In 1946, Erdős posed a question about point sets in the plane. Given points in , how many pairs of points can lie at unit distance from one another? Define:

The integer grid, rescaled, achieves at least unit distances. Erdős conjectured that this was essentially optimal:

The best upper bound, proved by Spencer, Szemerédi, and Trotter in 1984 using incidence geometry, sits at . So for forty years the truth about was known to lie somewhere in the corridor between Erdős's lower bound of and the Spencer–Szemerédi–Trotter ceiling of , and nobody knew which end was tight. Improving either bound by even an factor was a known hard problem.

On May 20, 2026, that problem was solved.

IMO 2024: Four Problems, One Point from Gold

To understand how these systems handle research-level mathematics, it helps to understand how they performed on competition mathematics first. The International Mathematical Olympiad is the world's most prestigious mathematics competition for students under 20, in which contestants have to solve six problems over two days. Gold medalists typically solve four or five. Problems 3 and 6 are designed to be particularly difficult.

In July 2024, DeepMind's AlphaProof and AlphaGeometry 2 were given all six problems from the Bath competition the same day every human contestant received them.

One point away from a gold medal performance. AlphaProof solved P1 (algebra), P2 (number theory), and P6 (functional equations). AlphaGeometry 2 solved P4 (geometry) in nineteen seconds.

What It Means to Formally Prove

A proof, in the ordinary sense, is a convincing argument addressed to a human reader. It is often left up to the reader to fill in unstated steps, resolve ambiguities, and read in the norms of mathematical culture. When Andrew Wiles announced his proof of Fermat's Last Theorem in 1993, it contained a gap that the referee Nick Katz flagged during peer review later that year. Wiles, working with his former student Richard Taylor, repaired the argument and published the corrected proof in 1995.

A formal proof is something else. It is a syntactic object: a sequence of inference steps, each a valid application of an explicit deduction rule, from axioms to a conclusion. Formal proofs cannot contain gaps or ambiguities, and a successful formal proof is "checked" by a machine at compile time.

Lean 4 is the current standard for formal mathematics. Propositions are types. A proof of a proposition is a term inhabiting that type. The Lean type checker verifies this claim mechanically. A Lean 4 proof of the irrationality of :

theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by
  rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_cast]
  exact_mod_cast Nat.Prime.irrational_sqrt (by norm_num)

If the type checker accepts this, the theorem is proven. Mathlib, the community- maintained Lean library, has grown to millions of lines of formally verified mathematics covering analysis, algebra, topology, and number theory.

A formal proof either compiles or it does not. The reward signal is binary and unambiguous.

AlphaProof: Reinforcement Learning on Formal Mathematics

AlphaProof couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, the same system behind AlphaGo and its successors. The language model generates Lean 4 tactics and the Lean compiler provides the reward signal.

Proofs are written as sequences of short tactics, which is the natural action space for a Monte Carlo tree search. The proof tree is structured as an AND/OR graph: OR-nodes represent alternative proof strategies; AND-nodes represent subgoals that must all be proven before a node is marked complete. Completed subgoals are never revisited.

The policy gradient update over a trajectory :

Because Lean proofs either compile or they do not, the environment is clean in a way that most RL setups are not. There is no reward shaping, no proxy metric, and no heuristic value function. The Lean type checker simply returns a verdict, and the model then updates on it directly.

During training, AlphaProof generated new problem variants, attempted proofs, and added successful proofs back into the training distribution. A fine-tuned Gemini model was used to autoformalize natural language problem statements into Lean goals and produced roughly 80 formal variants per problem.

Reward Linearization

Training on binary proof-verification rewards seems like it should be very effective, but it also poses a fundamental challenge: the signal is sparse. Most proof attempts fail, especially early in training. A model generating 1,000 proof attempts and receiving 1 successful compilation gets almost no gradient signal. At an intuitive level, there are not enough successful outcomes to give the model a sense of which strategies are more likely to succeed.

Reward linearization, the technique described in the SWE-Check paper from Cognition AI (2026), addresses this by translating the binary reward offered by proof verification into a step-level dense reward. For a partial proof of length , the reward assigned to the current step is the probability that a completion from this state will verify:

This probability is estimated empirically by sampling many completions and measuring what fraction compile. Tactics that systematically produce valid proofs receive higher reward and tactics that tend to terminate proof attempts receive lower reward. Critically, this technique preserves the feature of proof verification that makes it useful in the first place: the proof is still either correct or incorrect. Reward linearization does not relax the verification criterion, so the terminal reward remains binary. Linearization makes the intermediate gradient dense while keeping the final objective exact.

The technique generalizes to any task where the reward is a property of an entire sequence but individual steps have differential predictive power over the final outcome: code generation, proof synthesis, formal verification of hardware. The shared structure is a binary oracle over a sequence, and dense intermediate feedback derived from that oracle's statistics.

For AlphaProof specifically, this is the difference between learning from one signal per attempted proof and learning from one signal per tactic step. That ratio is what turns RL on formal mathematics from an intractable search problem, where the vast majority of attempts terminate in failure with nothing to learn from, into a regime where every step is informative and scale starts to pay off. The clean Lean verdict is what makes the technique honest, and the dense intermediate reward is what makes the training tractable.

AlphaGeometry 2: Neuro-Symbolic Construction

Many Euclidean geometry proofs hinge on a single clever geometric addition to the problem diagram. These might be as simple as a perpendicular bisector, a circle drawn through three existing points, or the addition of a new point chosen because it has a useful property.

This technique is called an auxiliary construction, and, in human-derived proofs, it is often an expression of deep insight into the nature of the problem and its solution. The rest of the work of the proof is formalizing and writing up the insight that is expressed through the construction, with careful attention to the correct application of axioms and theorems.

That step is hard to mechanize because an auxiliary construction cannot be derived from the problem statement by following rules. AlphaGeometry 2 sidesteps this by splitting the job between two systems that take turns. A Gemini mixture-of-experts language model, trained on 300 million synthetic geometry theorems, looks at the current diagram and proposes a construction.

The proof then passes to a symbolic deduction engine called DDAR, rewritten in C++ for low latency, which tries to grind out the rest of the proof using standard geometric rules. If DDAR gets stuck, control bounces back to the language model, which suggests another construction, and the cycle repeats. Several beam searches run in parallel and share a common pool of discovered facts so that progress on one branch helps the others.

AlphaProof Nexus: Nine Erdős Problems

The AlphaProof Nexus paper (arXiv:2605.22763) extends the system to open research problems. Starting from 353 open Erdős conjectures and 492 OEIS conjectures, the system solved 9 Erdős problems and proved 44 OEIS conjectures at a cost of roughly $60 to $300 per solved problem.

For each solved problem the team produced two artifacts: the Lean 4 formal proof, compiled against Mathlib, and a natural language prose proof written by a mathematician but based on the Lean proof.

The nine solved Erdős problems varied in field and difficulty. Three of the nine are reproduced below to give a sense of this range:

• Problem 125 (1996): Let be the integers whose base-3 representation uses only digits , and be the integers whose base-4 representation uses only digits . Does have positive lower density? Answer: No. Proof via inductive thinning using the Diophantine approximation .
• Problem 138 (1981): Do Van der Waerden numbers satisfy ? Answer: Yes.
• Problems 12(i) and 12(ii) (1970, open 56 years): Existence of an infinite set such that no element divides the sum of two larger elements, and such that for all . Proved via Behrend-style constructions for dense 3-AP-free sets.

Beyond the Erdős corpus the system also proved a 15-year-old open question on log-concavity of Hilbert functions in codimension 3, found a counterexample to Ben Green's Problem 57 on quadratically structured function spaces, and resolved a conjecture on monochromatic quantum graphs. The cost for each was a few hundred dollars in inference spend.

OpenAI: Disproving the Unit-Distance Conjecture

On May 20, 2026, OpenAI researcher Lijie Chen announced that an internal reasoning model had produced a counterexample to Erdős's unit-distance conjecture. The result emerged during a broader evaluation of open Erdős problems and was, in Chen's description, a side quest of that effort. Fields Medalist Tim Gowers, who signed the companion verification paper, said he would recommend the result for acceptance in the Annals of Mathematics without hesitation.

The construction achieves

for a fixed . Will Sawin subsequently refined the bound to .

The model that produced the proof is not a math-specialized system. It is a generalist reasoning model trained on a broad slice of mathematical literature rather than fine-tuned on a formal-proof corpus, closer in lineage to the systems behind ChatGPT and Codex than to AlphaProof. The argument was generated in a single pass as a 125-page natural-language document. The exposition was then refined through interaction with Codex and split into a primary proof paper and a human-verified companion.

The Setup

Chen authored the primary paper with computational support from the model. Mark Sellke and Mehtaab Sawhney, both OpenAI mathematicians, verified the argument step by step. A 19-page companion paper, "Remarks on the disproof of the unit distance conjecture," was signed by Noga Alon, Thomas Bloom, Tim Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood. The companion does not claim new mathematics. Its role is to translate the model's output into human-readable form, check the argument, and place the result in mathematical context.

The Construction

The classical approach to producing many unit distances fixes a CM field, embeds its ring of integers into the plane as a lattice, and scales a bounded region until enough lattice points fall inside. Taking recovers the standard Gaussian-integer construction and the baseline bound that Erdős already knew in 1946. Eighty years of work to push this further by choosing cleverer fixed fields ran into the same wall. As Sawin observes in the companion paper, the prime number theorem for prime ideals recovers Erdős's bound exactly, giving no indication that the choice of field provides leverage.

The model's contribution is to invert the strategy. Rather than fixing and scaling the region, keep the region fixed and let the degree grow without bound. Embed into (where ) via the Minkowski embedding, intersect with a fixed polydisc, and project to a single complex coordinate. Norm-one elements of contained in the polydisc each produce a unit distance under projection. A pigeonhole over ideal classes gives a count growing like

for split prime ideals and class number .

For the construction to gain on the grid, the root discriminant must remain bounded as . That condition is exactly what an infinite Golod-Shafarevich class field tower provides, and the Mythos section below treats this machinery in detail. The structural move that the OpenAI argument makes, and that earlier work did not, is to recognize the degree itself as the parameter to vary rather than the choice of field at fixed degree.

Mythos and the Unit-Distance Disproof

Anthropic's paper, "Integral points on norm-one tori and the Erdős unit-distance exponent," was produced by Claude Mythos and published around May 26, 2026, six days after the OpenAI paper and one day before this article.

The main theorem:

for an absolute constant , along an infinite sequence of integers . Since much more slowly than , this refutes Erdős's conjecture.

The construction uses algebraic number theory in a way that Erdős would likely have appreciated, and probably would not have predicted.

The Construction

Fix a number field with at least one real embedding. The norm-one torus of is:

The ring of integers has rational points on this torus. By Dirichlet's unit theorem, the group of units has rank , where is the number of real embeddings and the number of pairs of complex embeddings. For fields with large rank, projecting -points of the affine conic to via a real embedding yields point sets with many unit-distance pairs.

The key to the disproof is in controlling the field. To keep the root discriminant bounded while , the paper uses the Golod-Shafarevich criterion:

where is the -rank of the class group and is the -rank of units.

When this holds, the Hilbert -class field tower of is infinite. Applied to a real quadratic field with enough prime divisors in its discriminant, this produces an infinite totally real tower , each extension unramified everywhere, with bounded root discriminant as degrees grow without bound.

A quadratic twist at one real place introduces a complex embedding while keeping the tower structure intact. Van der Corput's lattice point theorem then converts the unit group rank into unit-distance directions. Louboutin's bound on the residue of the Dedekind zeta function and Zimmert's regulator estimate control the covolume. The stated lower bound follows.

The paper is roughly 15 pages. The OpenAI paper, covering overlapping but distinct territory, is 125 pages long. Mathematician Daniel Litt noted that Mythos's bound is "slightly worse in absolute terms" than the OpenAI result but the proof is more concise. Will Sawin, one of the OpenAI paper's authors, subsequently improved the upper bound to (arXiv:2605.20579).

Neither proof closes the gap to the Spencer-Szemerédi-Trotter ceiling of , which remains open, so Erdős's 1946 unit-distance conjecture (that ) is now definitively disproved. But the broader question is still open: where the true exponent actually lies remains unsolved.

What Changes Now

There are two immediate implications that flow from advances in AI model mathematics capabilities, and they both have to do with how the new strengths of these models interact with the strengths of their human counterparts in advancing the field. The significance of these systems is not speed. Human mathematicians do not need to be faster at olympiad problems.

The first has to do with the changing nature of what a proof of a problem means for our collective understanding. The formally verified proof shifts the question from whether a given proof is correct to the more subtle question of what the implications of a given proof might be. Formally verified proofs collapse a distinction that has existed since mathematics began: the distinction between a proof that is convincing and a proof that is correct. Once AlphaProof produces a proof the Lean type checker accepts, the question of whether the theorem is true is, in a strict sense, settled. The type checker has already validated every step, so the result no longer hinges on community consensus, peer review, or the chance of later retraction; any error would have been caught at compile time. The theorem is closed. But, as the paper written by mathematicians to accompany the disproof produced by OpenAI's internal model goes to show, a verified proof is not, in itself, the best way to communicate the insight that the proof embodies.

The second has to do with problem selection, and the nature of the problems in which advanced AI models appear to have a particular advantage. In some senses it has been possible to quickly verify proofs to problems in several fields since the release of Lean 3 in 2017. But taking advantage of the strengths of these tools still required the translation from mathematical intuition to machine-checkable syntax. The bottleneck was never verification. The Lean type checker has always been able to verify a proof in milliseconds. The bottleneck was always writing the proof in the first place: the translation from mathematical intuition to machine-checkable syntax could take weeks per theorem. That bottleneck is now, for a growing class of problems, lifted.

Right now that is true only for a subset of problems. Problems requiring genuinely new conceptual frameworks remain out of reach. But that subset is larger than it was one year ago. Nine open Erdős problems were solved for a few hundred dollars each. An eighty-year conjecture was disproved first by OpenAI and then, six days later, by Anthropic, in what appears to be about fifteen pages.

Erdős was, in the eyes of many, the platonic problem solver. Through the breadth of his mathematical talent, his broad collaboration, and his extreme focus, unusual even in a field of practitioners known for their intensity, Erdős produced solutions to problems that drew on tools from across the discipline. It seems particularly apt then that the progress of advanced AI models through the field of mathematics, which mathematicians note is characterised by superhuman persistence and the ability to draw from areas of math that are rarely found together, is being marked with reference to problems Erdős himself created.

In 1985, the same year that the photo was taken with a ten-year-old Terry Tao, Noga Alon published a paper with Erdős about the application of graph theory to additive number theory. Along with a handful of other papers, this grants Alon an Erdős number of 1. If we consider, generously perhaps, OpenAI's internal model a coauthor alongside Alon on this latest paper, then that model might have an Erdős number of 2. Whatever advances future models make in mathematics, this will remain a landmark achievement.

He left money on the table, on checks that have since expired, and now some of those tables are being cleared.

References

1. Anthropic. Integral points on norm-one tori and the Erdős unit-distance exponent. Technical paper by Claude Mythos, May 2026.
2. Alon, N., Bloom, T., Gowers, W.T., Litt, D., Sawin, W., Shankar, A., Tsimerman, J., Wang, V., Wood, M.M. Remarks on the disproof of the unit-distance conjecture. arXiv:2605.20695, May 2026.
3. Chen, L. Planar Point Sets with Many Unit Distances. With computational support from an internal OpenAI reasoning model; verified by M. Sellke and M. Sawhney. May 2026.
4. OpenAI. An OpenAI model has disproved a central conjecture in discrete geometry. Announcement, May 20, 2026.
5. Sawin, W. An explicit lower bound for the unit-distance exponent. arXiv:2605.20579, May 2026.
6. Tsoukalas, G. et al. Advancing Mathematics Research with AI-Driven Formal Proof Search. arXiv:2605.22763, May 2026. (AlphaProof Nexus paper.)
7. Google DeepMind. Alphaproof and AlphaGeometry 2 solve IMO problems at silver-medal level. Nature, 2025. doi:10.1038/s41586-025-09833-y.
8. Google DeepMind. AlphaProof Nexus Results. github.com/google-deepmind/alphaproof-nexus-results. Apache 2.0 / CC-BY 4.0.
9. Feng, R., Ling, J., Garg, R., Stephan, M. Introducing SWE-Check: 10x Faster Bug Detection. Applied Compute / Cognition AI, 2026. [reward linearization technique]
10. de Moura, L., Ullrich, S. The Lean 4 Theorem Prover and Programming Language. CADE, 2021.
11. Mathlib Community. The Lean Mathematical Library. CPP, 2020. leanprover-community.github.io/mathlib4_docs.
12. Spencer, J., Szemerédi, E., Trotter, W.T. Unit distances in the Euclidean plane. Graph Theory and Combinatorics (1984), 293–303.
13. Tao, T. The Erdős Discrepancy Problem. Discrete Analysis 1 (2016). arXiv:1509.05363.
14. Golod, E.S., Shafarevich, I.R. On the class field tower. Izv. Akad. Nauk SSSR 28 (1964), 261–272.
15. Erdős, P. On sets of distances of points. Amer. Math. Monthly 53 (1946), 248–250.