Version 1

Three major AI research organizations—OpenAI, Harmonic, and Google DeepMind—have each produced AI systems capable of generating or verifying non-trivial mathematical proofs, with the most striking result being OpenAI's unreleased general-purpose reasoning model disproving the Erdős unit distance conjecture, a problem open since 1946 [1]. Harmonic's Aristotle system generates proofs checkable in the Lean formal verification language [2], and DeepMind's system grounds every reasoning step in Lean before proceeding [3]. The convergence of these results in late May 2026 has drawn coverage from Nature, Quanta Magazine, The Guardian, and New Scientist, suggesting this registers well beyond the AI-enthusiast community.

Mathematical proofs verified by machines offer a stronger correctness guarantee than AI benchmark scores, which can reward pattern-matching rather than genuine reasoning [1]. If AI can routinely find counterexamples and proofs in long-open problems, the pace of mathematical discovery could accelerate substantially, with downstream effects on software verification, chip design, and scientific computing [2]. The shift from 'trust me, this is right' to 'check me, this is right' changes the epistemics of AI-assisted knowledge production in ways that extend well beyond pure mathematics.

In late May 2026, three major AI research organizations produced results that together mark a significant threshold in AI-assisted mathematics. The most dramatic was OpenAI's: an unreleased, general-purpose reasoning model produced a counterexample disproving the Erdős unit distance conjecture, a discrete-geometry problem that had stood open since Paul Erdős posed it in 1946 [1]. Critically, the model received no special mathematical training, scaffolding, or problem-specific targeting. Princeton mathematician Will Sawin subsequently sharpened the result to demonstrate more than n^1.014 unit-distance pairs for arbitrarily large point sets, and external mathematicians—including some who had previously been skeptical of OpenAI's mathematical claims—co-signed verification [1]. The Neuron argued that this constitutes a cleaner test of genuine AI reasoning capability than standard benchmarks precisely because a mathematical proof must survive line-by-line expert review rather than rewarding pattern-matched guesses [1].

At the same time, Harmonic's Aristotle system has been generating proofs formally checkable in Lean, a proof assistant language that provides machine-level correctness guarantees [2]. Harmonic co-founder Tudor Achim has framed this as an epistemological shift: AI moving from 'trust me, this is right' to 'check me, this is right,' with implications extending beyond pure mathematics into software verification, chip design, and scientific computing [2]. Achim has predicted AI could prove the Riemann Hypothesis by 2028—a claim that represents either a serious forecast or an extreme extrapolation depending on one's read of the current capability trajectory [2]. Separately, Google DeepMind published research on a Lean-grounded theorem-proving system; commentator Rohan Paul highlighted that the architectural key is forcing every reasoning step through Lean's verifier before proceeding, rather than generating proofs freely and checking afterward [3].

The central live debate among observers concerns what these results actually demonstrate about AI reasoning. DeepMind's system, as Paul summarized, shows that AI can search for proofs inside 'carefully constrained worlds'—it does not reason like a human mathematician, but rather achieves reliability by grounding each move in a formal verifier [3]. OpenAI's result cuts the other direction: a general-purpose model with no mathematical specialization found a counterexample to a decades-old open problem, suggesting the capability is not confined to systems purpose-built for formal mathematics [1]. Whether these approaches represent complementary paths or reveal a fundamental tension between constrained-formal and open-ended reasoning is unresolved.

The breadth of media coverage—spanning Nature, Quanta Magazine, The Guardian, New Scientist, TechCrunch, and major social platforms—signals that the mathematical and broader scientific communities are engaging with these results seriously. The convergence of independent results from three different organizations within a narrow window makes it harder to attribute the progress to any single team or technique, strengthening the case that the field has crossed a meaningful threshold rather than producing isolated demonstrations.