ai in mathematics

logic theorist proves theorems from principia symbolic

Newell, Simon, Shaw (RAND) · hand-checked · en.wikipedia.org historyofinformation.com

The first program to prove theorems. Working in the propositional calculus of Whitehead and Russell's Principia Mathematica, it proved 38 of the first 52 theorems of chapter 2 by backward chaining from the goal with three hand-written heuristics (substitution, detachment, chaining) and a memory of already-proved results. For theorem 2.85, the tautology (p ∨ q → p ∨ r) → (p ∨ (q → r)), it found a derivation shorter than the published one.

Nothing here is new mathematics: the target is decidable and every rule was human-specified. But it is the first time a machine produced a derivation an expert had not seen, and it established that heuristic search, not exhaustive enumeration, could work in a proof space. A paper co-authored with the program was famously rejected by the Journal of Symbolic Logic.

four colour theorem, by unavoidable sets and reducibility symbolic

Appel, Haken, Koch (Illinois) · accepted, later formalized · distributedmuseum.illinois.edu quantamagazine.org

Every planar graph is 4-colourable. The proof strategy, inherited from Kempe, Birkhoff and Heesch, has two halves. Unavoidability: a discharging argument (assign each vertex a charge by degree, Euler's formula forces the total positive, redistribute it) shows any minimal counterexample must contain one of a finite list of local configurations. Reducibility: each configuration in the list cannot occur in a minimal counterexample, checked by exhaustively testing colourings of its boundary ring. The final list had 1,936 configurations (1,476 in print, cut to 633 by Robertson, Sanders, Seymour and Thomas in 1996) and the reducibility checks took about 1,200 machine hours.

No AI; humans designed the discharging rules, the machine ground the cases. It is the origin of the "is a proof a proof if no human can read it" debate, and the baseline against which every later "the computer did the mathematics" claim should be measured.

enabled

four colour theorem formally verified in coq

the BBP formula for π, found by integer-relation search conjecture

Plouffe; Bailey, Borwein · proved by hand, Math. Comp. 1997 · en.wikipedia.org

An integer-relation algorithm (PSLQ) takes real numbers x_1..x_n computed to high precision and searches for integers a_i, not all zero, with Σ a_i x_i = 0. Plouffe fed it π together with a basis of polylogarithm values and the machine returned

π = Σ_{k≥0} 16^{-k} ( 4/(8k+1) − 2/(8k+4) − 1/(8k+5) − 1/(8k+6) )

Once stated, the identity is a one-page exercise (write each term as ∫_0^{1/√2} x^k/(1−x^8) dx and sum). The consequence was not: the formula gives a spigot algorithm for the n-th hexadecimal digit of π without computing the preceding ones, which everyone had assumed impossible. This is experimental mathematics in its pure form, and the methodological ancestor of the Ramanujan Machine: search generates the conjecture, a human proves it.

enabled

the ramanujan machine

robbins conjecture settled by an equational prover symbolic

McCune (Argonne), EQP · independently re-derived, published J. Algebra 1998 · cs.unm.edu mathworld.wolfram.com

A Robbins algebra is a set with a binary ∨ and unary ¬ satisfying associativity, commutativity, and the Robbins equation ¬(¬(x ∨ y) ∨ ¬(x ∨ ¬y)) = x. Robbins conjectured around 1933 that these three axioms characterise Boolean algebras. Tarski's school could not settle it. Winker had reduced the problem to exhibiting elements satisfying certain conditions (for instance c ∨ d = d for some c, d); EQP, an associative-commutative paramodulation prover, found an equational derivation of such a condition after about eight days of search.

This remains the strongest pre-2020 case of an automated system settling a genuinely open problem, and it is symbolic, not learned. The humans supplied the reduction and the search configuration; the machine found the last step. It is also the classic cautionary example for extrapolation: pure equational algebra is unusually machine-friendly, and the result did not generalise.

kepler conjecture: the proof a journal could not fully referee symbolic

Hales, Ferguson · Annals 2005 with a "99% certain" editorial note · arxiv.org annals.math.princeton.edu

No packing of congruent spheres in ℝ³ has density exceeding π/√18 ≈ 0.74048. Hales reduced Kepler's 1611 conjecture to a global optimisation over decomposition stars stratified by combinatorial type: roughly 5,000 cases, each bounded by interval arithmetic and linear programming, about 100,000 LP instances in total, 250 pages of text plus 3 GB of output.

A dozen Annals referees spent four years on it and reported they were "99% certain" but could not fully verify the computations. The journal published it anyway with a note about its unusual status. That outcome is what motivated Flyspeck and, indirectly, the modern formalization movement.

enabled

flyspeck: kepler formally verified

four colour theorem formally verified in coq formal

Gonthier (Microsoft Research), Werner (INRIA) · machine-checked by the Coq kernel · ams.org

Gonthier did not just transcribe Appel and Haken; he re-engineered the argument so that both the reasoning and the reducibility computations are Coq terms checked by the kernel. Planar embeddings became hypermaps, a purely combinatorial encoding (a set with two permutations) that turns planarity into an Euler-formula equation, and the configuration checks became programs whose execution inside the kernel constitutes proof. About 60,000 lines; nearly all of the trust rests on the kernel.

This is the moment "computer-assisted" and "formally verified" merged. The SSReflect tactic language and the Mathematical Components library that came out of it are direct ancestors of the Lean and mathlib infrastructure that every LLM prover after 2020 depends on.

relies on

four colour theorem, by unavoidable sets and reducibility

enabled

mathlib ported to lean 4

erdős discrepancy for C = 2, by SAT symbolic

Konev, Lisitsa (Liverpool) · DRUP certificate, later subsumed by Tao's full proof · arxiv.org en.wikipedia.org

Erdős conjectured that for every constant C and every infinite ±1 sequence there are d, n with |Σ_{i≤n} x_{i·d}| > C. Even C = 2 was open. Encoding "a length-n sequence of discrepancy ≤ 2 exists" as CNF (one Boolean per term plus counters bounding partial sums along each progression) and running a CDCL solver gave satisfiable at n = 1160 and unsatisfiable at n = 1161. The unsatisfiability certificate was about 13 GB, then widely noted as larger than Wikipedia.

The size of the certificate, not the depth of the mathematics, made the news. Tao proved the full conjecture for all C in September 2015 via the Elliott conjecture on multiplicative functions, work that grew out of Polymath5. A machine result focusing human attention is itself a recurring pattern.

flyspeck: kepler formally verified formal

Hales and ~20 collaborators (HOL Light, Isabelle) · machine-checked; Forum of Math. Pi 2017 · arxiv.org experimentalmath.info

Every link in the 1998 chain, now machine-checked: the text arguments, the ~23,000 nonlinear inequalities verified by interval arithmetic, the classification of tame hypermaps (Nipkow and Bauer, in Isabelle), and the LP bounds. Formalization exposed gaps and forced a substantial revision of the informal proof along the way, a pattern that recurs with the Liquid Tensor Experiment.

Eleven years, about twenty people. That is the yardstick for what "formalize a hard theorem" cost before LLM assistance.

relies on

kepler conjecture: the proof a journal could not fully referee

boolean pythagorean triples: the 200-terabyte proof symbolic

Heule, Kullmann, Marek · DRAT certificate checked by a verified checker · arxiv.org link.springer.com

Can {1..n} be 2-coloured with no monochromatic Pythagorean triple a² + b² = c²? Yes for n = 7824, no for 7825. The SAT encoding is direct (one Boolean per integer, one clause pair per triple); what makes it feasible is cube-and-conquer, where a look-ahead solver splits the problem into about a million balanced sub-problems that CDCL solvers then kill, plus symmetry breaking worth a factor of about 10⁵. Two days on 800 cores.

Kullmann and Gowers both voiced the standing critique of this whole lineage: the certificate contains no insight. You learn that 7825 is the threshold and nothing about why. Schur number five (Heule, 2017, S(5) = 160, a 2 PB certificate) and Keller's conjecture in dimension 7 (Brakensiek, Heule, Mackey, Narváez, 2019) extended the same method to other long-open finite questions.

enabled

the empty hexagon number g(6) = 30, then verified in lean

transformers do symbolic integration proof

Lample, Charton (Facebook AI) · ICLR 2020 · arxiv.org cs.nyu.edu

Serialise expression trees to prefix notation and integration becomes sequence-to-sequence. The trick is that training data can be generated backwards: differentiation is easy and total, integration is hard and partial, so differentiate random expressions to make (integral, function) pairs. An 8-layer transformer with beam search then reached 98% on the paper's integration test set versus 84% for Mathematica.

Ernest Davis's review is the necessary counterweight: the test set comes from the same generator as the training set and is biased toward functions that have short elementary antiderivatives. No new mathematics here, but two templates that everything later reuses: generate data in the easy direction, and let a cheap checker (here, differentiate the answer) filter an unreliable proposer.

enabled

transformers find global lyapunov functions

gpt-f: neural proofs merged into a formal library proof

Polu, Sutskever (OpenAI) · Metamath-checked; 23 proofs merged into set.mm · arxiv.org

A decoder-only transformer (up to 774M parameters) pretrained on maths-heavy web text, fine-tuned to predict the next Metamath proof step, and run inside best-first search with a learned value function. Proofs found by search became new training data (expert iteration). It reached 56% on a held-out set and, more memorably, produced 23 shorter proofs of existing theorems that human maintainers accepted into the main Metamath library.

The same category of result as Logic Theorist's theorem 2.85, 64 years later, at scale, in a live community library. Metamath's uniform low-level steps make it unusually tractable; the recipe did not transfer directly to Lean.

relies on

ai/GPT-2

the ramanujan machine conjecture

Raayoni, Gottlieb, Manor, Pisha, Harris, Mendlovic, Haviv, Hadad, Kaminer (Technion) · Nature; individual formulas proved or open · nature.com

Enumerate polynomial continued fractions a_0 + b_1/(a_1 + b_2/(a_2 + …)) with a_n = p(n), b_n = q(n) for integer polynomials, evaluate to hundreds of digits, and match against simple rational functions of π, e, Catalan's constant and ζ values. The search rediscovered many known identities and produced new conjectural ones, several since proved and several still open.

No neural networks: meet-in-the-middle enumeration and a gradient-descent variant. The depth of any single formula is modest and some mathematicians disliked the branding. Its status is exactly BBP's before Bailey and Borwein supplied a derivation: conjecture manufacture.

relies on

the BBP formula for π, found by integer-relation search

MATH and GSM8K benchmark

Hendrycks et al. (Berkeley); Cobbe et al. (OpenAI) · NeurIPS 2021 · arxiv.org arxiv.org

MATH is 12,500 competition problems (AMC and AIME level) with worked solutions; GSM8K is 8,500 grade-school word problems. Both grade by exact match on a final answer, so a model can be right for wrong reasons. Their importance is that they made "can a model do maths" a measurable quantity. MATH went from 6.9% (2021) to 50% (Minerva, mid-2022) to over 90% (frontier models, 2024); GSM8K saturated by 2024.

GSM8K's paper also introduced verifier reranking: sample many solutions, train a model to score them, keep the best. That idea is the direct ancestor of process reward models and of test-time-compute scaling. Both benchmarks draw on public archives that are in pretraining corpora, which is why FrontierMath and the formal benchmarks were built.

enabled

frontiermath

wagner: a neural policy refutes combinatorics conjectures construction

Wagner (Tel Aviv) · counterexamples checked exactly · arxiv.org

Turn a conjecture of the form "for all graphs G on n vertices, f(G) ≥ 0" into a single-player game: build the graph edge by edge, score −f(G), and train a policy to maximise the score with the deep cross-entropy method (sample episodes, keep the top few percent, do supervised learning on those, repeat). If the policy finds f(G) < 0, the conjecture is dead and the verification is a five-line script.

The most-cited refutation is a spectral conjecture, λ_1(G) + μ(G) ≥ √(n−1) + 1 for connected graphs, killed by a 19-vertex counterexample. The disproved conjectures were mostly machine-generated in the first place, and later work showed plain local search refutes several of them faster. The lasting contribution is the template: a construction problem where the machine's unreliability is free because verification is exact.

enabled

funsearch: cap sets from an evolutionary LLM loop, patternboost refutes a 30-year-old hypercube conjecture

miniF2F benchmark

Zheng, Han, Polu (OpenAI, École Polytechnique) · ICLR 2022 · arxiv.org

488 olympiad-level statements formalized in Metamath, Lean, and partly Isabelle and HOL Light. It made formal theorem proving comparable across systems and became the single number every prover paper reported for four years: GPT-f baseline ~25% (2021), ~41% with tree-search RL (2023), 50% for DeepSeek-Prover V1 (May 2024), 63.5% for V1.5 (August 2024).

Statements are public and proofs are checkable, so overfitting is a real risk; saturation is why PutnamBench and FrontierMath exist.

enabled

deepseek-prover

a knot-theory theorem found by feature attribution conjecture

Davies, Juhász, Lackenby, Williamson et al. (DeepMind, Oxford, Sydney) · Nature; theorem peer-reviewed separately · nature.com arxiv.org

A hyperbolic knot's complement carries a cusp whose flat torus has two distinguished translations, the meridian μ and longitude λ; their ratio determines the cusp shape. Separately, the signature σ(K) is a classical algebraic invariant (the signature of V + Vᵀ for a Seifert matrix V) that bounds the 4-ball genus. Nobody expected the algebraic invariant to be predictable from hyperbolic geometry.

DeepMind trained a network to predict σ(K) from a dozen geometric invariants and got high accuracy. Gradient attribution showed the prediction leaned almost entirely on the real and imaginary parts of the meridional translation and on the longitudinal translation. Lackenby defined the right combination, the natural slope slope(K) = −Re(λ/μ), and he and Juhász proved

|2σ(K) − slope(K)| ≤ c · vol(K) · inj(K)^{−3}

for an explicit constant c. The network proved nothing; it narrowed the search for which features mattered. The theorem, its statement and its proof are human. Davis's critique that this is exploratory data analysis with a press release has weight; the counter is that this specific connection was on nobody's radar.

kazhdan–lusztig polynomials: a conjectural recursion from a GNN conjecture

Blundell, Buesing, Davies, Veličković, Williamson · verified on 3M+ intervals; conjecture open · nature.com arxiv.org

For the symmetric group with Bruhat order, each pair x ≤ w has a Kazhdan–Lusztig polynomial P_{x,w}(q) whose coefficients are dimensions of intersection cohomology stalks of Schubert varieties. The computable recursion uses the group elements themselves. The combinatorial invariance conjecture (Lusztig, Dyer, around 1980) says P_{x,w} depends only on the isomorphism type of the interval [x,w] as a labelled directed graph.

A graph neural network trained to predict the coefficients from the interval graph alone succeeded, which is empirical evidence for the conjecture, and edge attribution highlighted particular subgraph structures. Williamson turned those into a hypercube decomposition of the interval and a conjectural recursion expressing P_{x,w} in terms of the pieces. Proving it for all intervals would prove combinatorial invariance for S_n. As of 2024 it remained open.

enabled

bruhat intervals that are large hypercubes

murmurations of elliptic curves conjecture

He, Lee, Oliver, Pozdnyakov · phenomenon verified on billions of curves; proved for modular forms by Zubrilina 2023 · arxiv.org quantamagazine.org

For an elliptic curve E/ℚ and a good prime p, the Frobenius trace is a_p = p + 1 − #E(𝔽_p). The team was training classifiers on LMFDB data to predict a curve's rank from its a_p sequence and getting suspiciously high accuracy. Trying to understand why, Pozdnyakov plotted the average a_p over curves of each rank, for about 10,000 curves in a narrow conductor window, as a function of p. Instead of noise: a smooth oscillating wave whose shape depends on rank parity, with the rank-0 and rank-1 curves near mirror images.

Nobody had seen it, partly because the standard normalisation a_p/√p and working at fixed conductor wash it out. Sutherland verified it on billions of curves and wrote to Sarnak and Rubinstein, who had no explanation. The machine learning is genuinely upstream and yet contributed nothing directly: a classifier succeeding is what prompted the "why?" that produced the plot. Zubrilina (October 2023) proved an explicit murmuration density for holomorphic modular forms ordered by level, via an Eichler–Selberg trace formula, published in Inventiones; the exact regime of the original observation is closely related but not identical.

minerva proof

Lewkowycz et al. (Google) · NeurIPS 2022, benchmark numbers only · arxiv.org

PaLM further pretrained on 118 GB of arXiv LaTeX and mathematical web pages, prompted with chain-of-thought and majority-voted over 64 samples, went from the prior 6.9% to 50.3% on MATH. The jump came from a data decision (keep the equations) plus two inference tricks, with no tools or verifier.

The authors' own error analysis found about 8% of correct MATH answers were reached by incorrect reasoning. That number is why the field moved toward formal and process-supervised evaluation: a system graded on final answers can be right for the wrong reasons, and on a problem whose answer is unknown you cannot tell.

relies on

ai/chain-of-thought prompting, ai/self-consistency, ai/PaLM

liquid tensor experiment completed formal

Commelin and the Lean community; challenge by Scholze · Lean 3 · leanprover-community.github.io

Scholze publicly asked, in December 2020, for the one theorem in condensed mathematics he was least sure of to be independently checked: a vanishing of Ext groups for liquid real vector spaces that makes the liquid theory a workable replacement for topological vector spaces. Eighteen months and dozens of contributors later it was fully formalized.

Formalization made the human proof better: tracking exactly which inputs were used showed the dependence on the Breen–Deligne resolution could be replaced by an elementary statement. This is the benchmark for what it costs to formalize modern research mathematics, and the bar later LLM-assisted formalization claims should clear.

alphatensor: matrix multiplication as a game construction

Fawzi et al. (DeepMind) · Nature; decompositions exactly checkable · nature.com github.com

Multiplying an m×n by an n×p matrix is a bilinear map encoded by a 3-tensor T. A decomposition T = Σ_{r=1}^{R} u_r ⊗ v_r ⊗ w_r into R rank-one terms is exactly an algorithm using R scalar multiplications, and the minimal R is the tensor rank. Strassen's 1969 rank-7 decomposition for 2×2 gives 49 for 4×4 by recursion. AlphaTensor plays TensorGame: state is the residual tensor, an action subtracts one rank-one term with small integer entries, reward is −1 per move, terminal when the residual is zero. An AlphaZero-style agent with MCTS, trained on synthetic decompositions plus self-play with heavy symmetry augmentation, found rank 47 for 4×4.

The caveats arrived within days and matter. The 47 is over 𝔽₂ only, where +1 = −1 gives the search a larger symmetry group; it yields no faster algorithm over the reals and says nothing about the exponent ω. Two months later Kauers and Moosbauer showed a random walk on a flip graph of schemes (local moves that preserve correctness and rank, taking a rank-reducing move when one appears) matched or beat AlphaTensor, including reaching rank 95 for 5×5 over 𝔽₂ by starting from AlphaTensor's 96. A real, checkable, novel object, oversold, and not near the frontier of what classical search could do with the same compute.

relies on

ai/alphazero and expert iteration

enabled

alphaevolve: 48 multiplications for 4×4, kissing number 593 in dimension 11

draft, sketch, prove proof

Jiang, Welleck, Zhou, Li, Liu, Jamnik, Lacroix, Wu, Lample · ICLR 2023; Isabelle-checked · arxiv.org

Have an LLM write an informal proof, translate it into an Isabelle proof sketch (a chain of have statements ending in the goal, each justification left as a hole), and hand the holes to sledgehammer. The model's job shrinks from "produce a correct proof" to "produce a correct decomposition", which is far more forgiving: individual steps can be rejected and the structure still carries the information. miniF2F-test went from 20.9% to 39.3%.

No new mathematics; the right interface between unreliable natural-language reasoning and a reliable checker. Every later system reuses the decomposition-plus-hammer shape.

relies on

ai/codex and humaneval

tao's experiments with gpt-4 as a collaborator proof

Terence Tao · self-reported · mathstodon.xyz unlocked.microsoft.com

Calibration, not a result. Tao asked GPT-4 not for the answer to a MathOverflow question but for strategies, as a collaborator would offer; it listed about eight, one of which (generating functions) worked. His assessment was deliberately deflationary: he would probably have got there anyway and had no further use for the model once he started. His phrasing, that 2023-level AI could "generate suggestive hints and promising leads to a working mathematician", became the sober citation for the period.

relies on

ai/GPT-4 and claude 1

leandojo and reprover proof

Yang, Swope, Gu, Chalamala, Song, Yu, Godil, Prenger, Anandkumar · NeurIPS 2023 · arxiv.org

Open infrastructure for interacting with Lean programmatically, a benchmark of 98,734 theorems extracted from mathlib with premise-level annotations, and ReProver, a retrieval-augmented tactic generator trained in one GPU-week. The bottleneck it targets is premise selection: proving a goal means invoking the right lemma out of about 200,000, and a model that must emit the name from memory fails on anything unseen. A dense retriever over lemma statements fixes that. The novel_premises split, test theorems whose proofs use lemmas never seen in training, exposed how much prior benchmark performance was memorisation.

Performance was well below closed systems; the significance is that it made the subfield reproducible outside big labs. DeepSeek-Prover and Lean Copilot build on it.

relies on

ai/retrieval-augmented generation

enabled

deepseek-prover

mathlib ported to lean 4 formal

the Lean community · by construction · leanprover-community.github.io

Over a million lines of coherent formalized mathematics (measure theory, functional analysis, commutative algebra, algebraic topology, number theory through modular forms) moved to a fast, metaprogrammable platform. Coherence is the property that matters: one algebraic hierarchy, one topology API, so it can be a target for automated systems.

Every subsequent LLM prover result on this page is denominated in Lean 4 mathlib. Without it there is no reward signal, no training corpus, and no verification.

relies on

four colour theorem formally verified in coq

enabled

polynomial freiman–ruzsa formalized in three weeks, the empty hexagon number g(6) = 30, then verified in lean, alphaproof and alphageometry 2 at IMO 2024, gauss autoformalizes the strong prime number theorem, claude formalizes fermat's last theorem in eleven days

polynomial freiman–ruzsa formalized in three weeks formal

Tao, Dillies, Mehta and ~20 contributors; theorem by Gowers, Green, Manners, Tao · Lean 4 · terrytao.wordpress.com teorth.github.io

PFR over 𝔽₂: if A ⊆ 𝔽₂ⁿ has small doubling, |A + A| ≤ K|A|, then A is covered by at most 2K^C translates of a subgroup no larger than A, for an absolute constant C (12 in the original proof). The proof is entropy-theoretic, replacing sets by random variables and doubling by Ruzsa distance d(X;Y) = H(X−Y) − ½H(X) − ½H(Y).

A brand-new research theorem was fully formalized within three weeks of the preprint. No AI: the speed came from Massot's blueprint tooling (the paper as a dependency graph of lemmas with per-node status, so twenty people work without collisions) and from mathlib already containing the entropy and Fourier machinery. The companion Prime Number Theorem project, launched in January 2024, stalled for lack of contour integration in mathlib. Library infrastructure, not model capability, is the rate limiter.

relies on

mathlib ported to lean 4

enabled

the equational theories project, gauss autoformalizes the strong prime number theorem

funsearch: cap sets from an evolutionary LLM loop construction

Romera-Paredes et al. with Ellenberg, Fawzi (DeepMind) · Nature; constructions exactly checkable · nature.com cs.nyu.edu

A cap set is a subset of 𝔽₃ⁿ with no three distinct elements summing to zero: no three-term progression, no "line" in the card game SET. Upper bounds had a famous breakthrough (Ellenberg and Gijswijt, 2016, O(2.756ⁿ)); lower bounds come from explicit constructions and are hard to move. The asymptotic record, capacity lim |A_n|^{1/n} ≥ 2.2180, had stood since Edel 2004.

FunSearch prompts a code model with the two best-scoring programs so far and asks for a better one; the candidate is executed against an exact evaluator; high scorers join an island-model population that is periodically culled. The model is a mutation operator, not a reasoner, and it writes a program that builds the object, so the output is readable. That readability mattered: the generated code implicitly assumed a symmetry nobody had noticed, Ellenberg spotted it, and re-running restricted to symmetric constructions gave a 512-element cap set in dimension 8 (previous 496) and capacity ≥ 2.2202. Also new online bin-packing heuristics beating best-fit. Davis's critique stands: the cap set problem is not solved, one lower bound moved a little, and the pivotal step was human.

relies on

ai/PaLM, wagner: a neural policy refutes combinatorics conjectures

enabled

patternboost refutes a 30-year-old hypercube conjecture, alphaevolve: 48 multiplications for 4×4, kissing number 593 in dimension 11

alphageometry proof

Trinh, Wu, Le, He, Luong (DeepMind, NYU) · Nature; proofs produced by a sound symbolic engine · nature.com

Olympiad plane geometry has a structural gift: given a fixed set of objects, the set of derivable facts is finite and computable. A symbolic engine (a deductive database of geometric rules plus Gaussian elimination over angles, ratios and distances) computes it. What it cannot do is invent new objects, and hard problems require exactly that: an unmentioned midpoint, a second circle intersection, a reflection. So a 151M-parameter transformer proposes auxiliary constructions and the engine does all deduction, which keeps every proof sound.

The real contribution is the data pipeline. Sample a random configuration, compute its deductive closure, trace each derived fact back to its minimal premises; if the trace needs a point outside the premise set, that point is a labelled construction. A billion diagrams gave 100 million training theorems with no human demonstrations. Result: 25 of 30 IMO geometry problems (2000–2022) versus 10 for the previous best and 25.9 for the average gold medallist. On IMO 2004 problem 1 it never used one hypothesis, proving a strictly more general statement. The domain is narrow and the deduction rules are hand-written.

relies on

ai/the transformer

enabled

alphaproof and alphageometry 2 at IMO 2024

the empty hexagon number g(6) = 30, then verified in lean symbolic

Heule, Scheucher; formalized by Subercaseaux, Nawrocki, Gallicchio, Codel, Carneiro, Heule · SAT proof, then the whole chain formally verified in Lean 4 · arxiv.org arxiv.org

Every 30 points in general position contain an empty convex hexagon, and 29 do not suffice. The last open case of the Erdős–Szekeres empty-polygon question: Horton showed empty heptagons can be avoided forever, Gerken and Nicolás showed enough points force an empty hexagon, and the threshold was unknown. The encoding uses order-type variables (the orientation of each triple) with signotope axioms, O(n⁴) clauses, and about 17,300 CPU hours.

Then the geometric encoding's soundness and the SAT proof were both formally verified in Lean. This is the strongest verification status on the page, and the standard the "AI proved X" claims of the same year should be read against.

relies on

boolean pythagorean triples: the 200-terabyte proof, mathlib ported to lean 4

deepseek-prover proof

Xin, Ren, Guo, Shao et al. (DeepSeek) · every counted success is Lean-checked · arxiv.org arxiv.org

Take 870k competition problems in natural language, autoformalize each into a Lean statement, filter aggressively (including a negation check that discards any statement the model can prove both ways, which catches mis-formalizations), generate proofs, and keep the ones Lean accepts: 8 million verified pairs to fine-tune a 7B model. V1 hit 50% on miniF2F-test. V1.5 (August) added RL where the reward is simply whether Lean accepts the proof, and a Monte-Carlo tree search with an exploration bonus to stop the sampler re-deriving the same proof, reaching 63.5%.

It showed the AlphaProof recipe's ingredients, mass autoformalization and RL against a verifier, were reproducible by a small team at 7B scale with open weights. The sample budgets are enormous (about 100k attempts per problem), so pass@N is not a solve rate in any human sense.

relies on

miniF2F, leandojo and reprover, ai/GRPO and reinforcement learning with verifiable rewards

enabled

alphaproof and alphageometry 2 at IMO 2024, erdős #728: "the most unambiguous instance"

BB(5) = 47,176,870, verified in coq symbolic

the bbchallenge collaboration · fully machine-checked in Coq · discuss.bbchallenge.org scottaaronson.blog

The fifth busy beaver value: the most steps a halting 5-state, 2-symbol Turing machine can take from a blank tape. Marxen and Buntrock's 1990 champion was conjectured optimal. Proving it means deciding halting for about 181 million machines after symmetry reduction, and proving non-halting for the ones that run forever, which in general needs ad hoc arguments. The collaboration built a library of verified deciders, each recognising a class of non-halting behaviour, and handled a few stubborn machines with bespoke proofs.

No AI; an open, largely anonymous distributed human effort with formal verification. The purest 2024 example of the non-AI computational lineage still delivering headline results. BB(6) is known to exceed 2↑↑↑5, so this is the end of the line.

alphaproof and alphageometry 2 at IMO 2024 proof

Google DeepMind; graded by Gowers and Myers · Lean proofs, machine-checked; Nature 2025 · deepmind.google nature.com

Four of six problems, 28 of 42 points, one below the gold cut. AlphaProof took P1 (all real α such that n | Σ_{k≤n} ⌊kα⌋ for every n: the even integers), P2 (pairs (a,b) with gcd(aⁿ + b, bⁿ + a) eventually constant: only (1,1)), and P6, the "aquaesulian function" problem, solved by 5 of 609 humans. AlphaGeometry 2 took P4 in 19 seconds. Both combinatorics problems went unsolved.

AlphaProof is an AlphaZero-style agent in Lean. A Gemini model autoformalized about a million informal problems into tens of millions of candidate formal statements; the agent then did RL with reward 1 if the proof compiles and 0 otherwise, an unhackable signal. The distinctive move is test-time RL: for a hard target, generate a family of variant problems and keep training on them at inference. That is why some problems took minutes and others up to three days, against the 4.5-hour human session.

The caveats are material: statements were formalized by humans (for P6 a non-trivial act), the time budget was not comparable, and no combinatorics. But the outputs are machine-checked proofs, which makes this the strongest "AI solves competition problems" claim of the year, and the contrast with o1 seven weeks later is the sharpest illustration of formal versus informal proving.

relies on

alphageometry, deepseek-prover, mathlib ported to lean 4, ai/alphazero and expert iteration, ai/GRPO and reinforcement learning with verifiable rewards

enabled

IMO 2025: gold in natural language

o1: test-time reasoning on AIME proof

OpenAI · vendor-reported · openai.com

AIME 2024 went from 13% (GPT-4o) to 74% single-sample, 83% with 64-sample consensus, and 93% reranking 1,000 samples. The spread between those three numbers is the most informative content: it shows how much of "reasoning" is search over samples. No proofs, no verifiable artifact, no published method. Answer-matching on a 15-problem integer-answer competition.

relies on

ai/o1

the equational theories project formal

Tao and ~50 contributors, plus Vampire and other provers · everything Lean-verified; closed April 2025 · terrytao.wordpress.com teorth.github.io

A magma is a set with one binary operation and no axioms. Take the 4,694 equational laws with at most four operations (up to symmetry) and determine the entire implication graph: 22,028,942 ordered pairs. Proving an implication is an equational derivation; refuting one is a magma satisfying the first law but not the second, sometimes necessarily infinite (the "Austin pairs").

Many tools, none dominant. Most pairs fell to automated provers and brute-force finite-magma search, a minority needed human ingenuity, and LLMs helped with code, constructions and formalization but were not the engine. Everything was reduced to Lean. Tao's stated goal was to test whether a large collaboration can be organised around a proof assistant as the shared source of truth, removing the need for participants to trust each other.

relies on

polynomial freiman–ruzsa formalized in three weeks

enabled

the equational theories project completes

transformers find global lyapunov functions construction

Alfarano, Charton, Hayat (Meta, École des Ponts) · NeurIPS 2024; each function individually checkable · arxiv.org

For ẋ = f(x) with f(0) = 0, a Lyapunov function V has V(0) = 0, V > 0 elsewhere, and ∇V · f < 0 elsewhere; its existence proves global asymptotic stability. There is no known general algorithm for finding one. For polynomial systems you can search polynomial V by sum-of-squares programming, which scales badly and does not cover non-polynomial f.

The move is backward data generation again: sample V first, then construct systems f for which it works, giving unlimited correctly-labelled data including non-polynomial cases no solver handles. Trained seq2seq models then propose V for new systems, and each proposal is checked symbolically. The models beat SOS solvers on the paper's distributions and produced Lyapunov functions for non-polynomial systems previously out of reach. The distributional caveat from 2019 applies, but the target is a real open problem, not a benchmark.

relies on

transformers do symbolic integration

patternboost refutes a 30-year-old hypercube conjecture construction

Charton, Ellenberg, Wagner, Williamson · counterexample checked by one shortest-path table · arxiv.org

Two phases, deliberately simple. Local: classical search (simulated annealing, hill climbing) from seeds produces many good constructions. Global: train a transformer from scratch on the best ones, serialised as tokens, so it learns the distribution of good objects; sample fresh seeds from it; repeat. No reward model, no chat model, exact verification at every step.

The headline: Graham and Harary asked how few edges a spanning subgraph of the hypercube Q_d can have while keeping diameter d, and conjectured a construction was optimal. For d = 6 PatternBoost found 81 edges against the conjectured 82. The authors are candid that on several other problems the method did nothing useful.

relies on

wagner: a neural policy refutes combinatorics conjectures, funsearch: cap sets from an evolutionary LLM loop

frontiermath benchmark

Epoch AI with 70+ mathematicians · private set, Epoch-run evaluations · epoch.ai the-decoder.com

Hundreds of original, unpublished research-adjacent problems whose answers are specific computable objects (a large integer, an algebraic number, a matrix) that are essentially impossible to guess and easy to check. Typical problems take an expert hours to days. Tao and Gowers were among the assessors, and the contemporaneous view was that it would resist AI for years. At release no model scored above 2%.

Six weeks later OpenAI announced o3 at 25.2%, and the same day it emerged that OpenAI had funded the benchmark and had access to most problems and solutions. Epoch kept a holdout. The result is real and important, and its epistemics are the weakest on this page: vendor-announced, final-answer grading, evaluation conditions unpublished. Carry that contrast, o3's 25% versus AlphaProof's Lean-checked P6, into everything that follows.

relies on

MATH and GSM8K

enabled

the first proof challenge, a hadamard matrix of order 668; elliptic curves of rank 30 and 31

alphaevolve: 48 multiplications for 4×4, kissing number 593 in dimension 11 construction

Google DeepMind · constructions exactly checkable; humans improved the 48 within a month · deepmind.google arxiv.org

FunSearch's successor: a population of Python programs that generate constructions, mutated by Gemini, scored by a human-written verifier. Three headline results. A rank-48 decomposition of the 4×4 matrix-multiplication tensor, the first improvement on Strassen-recursion's 49 in 56 years for that format, initially over ℂ; within a month human mathematicians found an isotropy under which the complex scheme projects onto ℚ, giving a rational rank-48 scheme valid over any ring of characteristic ≠ 2. An explicit configuration of 593 non-overlapping unit spheres touching a central one in dimension 11, up from 592. And on a suite of about 50 open problems, rediscovery of the state of the art in roughly 75% and improvement in roughly 20%.

Constructions, not theorems: AlphaEvolve searches, it does not prove. The 20% also means it failed on 80%, and Tao's later study is candid that it made no progress on analytic number theory even with expert hints.

relies on

funsearch: cap sets from an evolutionary LLM loop, alphatensor: matrix multiplication as a game, ai/gemini 2.5

enabled

mathematical exploration and discovery at scale, bruhat intervals that are large hypercubes

IMO 2025: gold in natural language proof

OpenAI (experimental model); Google DeepMind (Gemini Deep Think) · DeepMind graded by IMO coordinators; OpenAI self-graded by former medallists · deepmind.google techcrunch.com

Both systems scored 35 of 42, five of six problems, missing only the combinatorics problem 6, under the human conditions: two 4.5-hour sessions, no tools, no internet. One year after AlphaProof needed Lean and up to three days per problem for silver, general-purpose reasoning models produced gold-standard prose proofs on the clock.

The two announcements were not equivalent. DeepMind's was certified by the IMO's own coordinators with the contestant rubric; OpenAI announced first, before official grading concluded, graded by three former medallists it engaged itself. Ten days later Harmonic's Aristotle produced Lean-verified proofs of the same five problems and ByteDance's Seed-Prover got four in Lean during the contest window, which removes the grading question but not the statement-fidelity one: a Lean proof shows the Lean statement, not necessarily the English one.

relies on

alphaproof and alphageometry 2 at IMO 2024, ai/GRPO and reinforcement learning with verifiable rewards, ai/RL on chain-of-thought and the test-time compute scaling law

enabled

aletheia: erdős #1051 and a paper written by itself, IMO 2026: perfect scores, and the grading tiers that got lost

gauss autoformalizes the strong prime number theorem formal

Math Inc. (Gauss), on Tao and Kontorovich's blueprint · Lean-verified · math.inc github.com

The project that had stalled for eighteen months for lack of contour integration in mathlib was finished by an autoformalization agent in three weeks: π(x) = li(x) + O(x·exp(−c(log x)^{3/5}(log log x)^{−1/5})), over 25,000 lines and about 1,100 theorems and definitions. Gauss interleaves natural-language and Lean reasoning and runs autonomously for hours against the compiler, on top of the human blueprint. In February and March 2026 it formalized Viazovska's sphere-packing theorems in dimensions 8 and 24, the latter over 200,000 lines in about two weeks.

Known theorems, not new ones. But the mental model "a Fields-Medal theorem is a multi-year formalization project" stopped being true here. Han's own note is telling: "there is no single human who is really familiar with this artifact."

relies on

polynomial freiman–ruzsa formalized in three weeks, mathlib ported to lean 4

enabled

claude formalizes fermat's last theorem in eleven days

unstable singularities in fluid equations construction

DeepMind with Gómez-Serrano, Buckmaster, Wang et al. · preprint; numerical profiles, rigorous proof pending · arxiv.org deepmind.google

Whether smooth initial data can blow up in finite time is the central question of mathematical fluid dynamics and, for Navier–Stokes, a Millennium Prize problem. Progress comes from self-similar solutions that converge to a fixed profile in rescaled coordinates. Chen and Hou's computer-assisted proof for Euler with boundary (2022) used a stable profile, but for boundary-free Euler and for Navier–Stokes the expectation is that no stable singularity exists, so any blow-up must be unstable: a saddle point that naive solvers slide off.

Physics-informed neural networks as the ansatz for the profile and scaling exponent, trained with a high-precision Gauss–Newton optimiser rather than Adam, drove residuals down to double-precision round-off and found new unstable families for incompressible porous media, Boussinesq, and 3D Euler with boundary, plus an empirical near-linear relation between scaling rate and instability order. Precision matters because a computer-assisted proof needs a rigorously controlled ball around the numerical approximation. This is AI as a numerical method, not a prover, and it is not a proof of Navier–Stokes blow-up; DeepMind's own framing is "a new playbook".

enabled

finite-time blow-up with smooth forcing for IPM, boussinesq and 3D euler

gpt-5 supplies a step in a quantum complexity theorem proof

Aaronson, Witteveen, with GPT-5 Thinking · verified by the authors; preprint · scottaaronson.blog

Jeffery and Witteveen had a QMA amplification protocol with doubly exponentially small completeness error. The new paper proves that is optimal for black-box amplification. The stuck point was the behaviour of the top eigenvalue of a Hermitian matrix E(θ) as θ varies. After half an hour of back-and-forth and several wrong suggestions, GPT-5 proposed tracking Tr[(I − E(θ))^{−1}] = Σ 1/(1 − λ_i(θ)), which blows up exactly when an eigenvalue approaches 1 and is analytically tractable.

Aaronson is candid: the suggestion "should have been obvious" with more literature time, the function surely appears in random matrix theory in the training data, and a blog commenter proposed det(I − E), which works better. He frames the sweet spot as unsticking experts, not writing papers. A calibration point against everything that follows.

relies on

ai/GPT-5

the "GPT-5 solved 10 Erdős problems" fiasco proof

Bubeck, Sellke, Weil (OpenAI); Bloom (erdosproblems.com) · retracted in effect; the literature finds were real · the-decoder.com erdosproblems.com

A now-deleted post by an OpenAI vice president said GPT-5 had "found solutions to 10 previously unsolved Erdős problems". What had happened was literature search, and a genuinely good one: for problem #339, GPT-5 Pro located a 2003 paper that had settled it twenty years earlier under different vocabulary, and Sellke reported ten such "open" problems with existing solutions. But "open" on erdosproblems.com means Bloom is not aware of a solution, not that none exists. Bloom called the amplified claim "a dramatic misrepresentation"; Hassabis called it "embarrassing".

The reputational damage hardened priors right before the wave of genuine results. It is the single most useful reference point for reading corporate mathematics announcements, and when the same lab announced the unit distance disproof seven months later, the community's warmer reaction was informed by the contrast. Tao's AI-contributions wiki now lists over 80 literature-search finds in their own category.

relies on

ai/GPT-5

enabled

early science acceleration experiments with gpt-5, an openai model disproves the erdős unit distance conjecture

point convergence of nesterov's method, open since 1983 proof

Jang, Ryu (UCLA), with GPT-5 Pro · preprint by domain experts · arxiv.org

Nesterov's accelerated gradient method achieves the optimal O(1/k²) rate on convex smooth functions, but "objective values converge" is weaker than "the iterates converge to a specific minimiser": on a flat set of minimisers they could wander forever. Whether {x_k} converges at all was open for 42 years. It does.

Three days and about twelve hours of hands-on work. Ryu first had the model solve the continuous-time analogue, the ODE limit where the analysis is cleaner, then propagated the Lyapunov-style argument back to discrete time, verifying and repairing each step. Squarely human-in-the-loop: the expert chose the problem and the reduction strategy. The pattern is "AI compresses months into days for an expert", not autonomous discovery.

relies on

ai/GPT-5

mathematical exploration and discovery at scale construction

Georgiev, Gómez-Serrano, Tao, Wagner · preprint with public per-problem repository; several constructions Lean-formalized · arxiv.org terrytao.wordpress.com

AlphaEvolve on 67 problems in analysis, combinatorics, geometry and number theory. Concrete movement: the Sidon set upper-bound constant from 1.96365 to 1.9526…; finite-field Kakeya sets beating the best bound by an O(q) term in three dimensions, later formalized via AlphaProof; new hybrid Nikodym constructions; Gerver's moving sofa rediscovered from scratch; Talenti's Gagliardo–Nirenberg extremisers recovered.

The methodology matters more than any constant. Three working modes: discovery with obfuscation (hide the problem's provenance so the model cannot retrieve the known answer), parametric generalisation (evolve a program in n, so the search yields a family rather than a point; this is how IMO 2025 problem 6 fell), and verifier co-evolution, which requires exploit-proof verifiers because the system will otherwise game floating point. Tao is explicit that designing those verifiers is where the human skill now lives, and equally explicit about the failures on analytic number theory.

relies on

alphaevolve: 48 multiplications for 4×4, kissing number 593 in dimension 11

enabled

alphaevolve improves the matrix multiplication exponent

early science acceleration experiments with gpt-5 proof

OpenAI with Bubeck, Sellke, Sawhney, Coester, Yin · verified by named human authors; preprint · arxiv.org erdosproblems.com

OpenAI's careful answer to the October fiasco: an 89-page report with named human verifiers for every claim. Four new mathematics results. Gradient descent with step size η ≤ 1.5/L produces a convex sequence of objective values, improving the classical 1/L (the true threshold is 1.75/L). Erdős #848, whether the largest A ⊆ {1..N} with ab + 1 never squarefree is {n ≡ 7 mod 25}, settled for large N by combining a GPT-5 idea with online commenters' density bounds. New lower bounds for follow-the-leader online algorithms. Inequalities between path, star and "wye" subgraph counts in trees.

Real but modest, conversational and expert-framed throughout. The change in tone from a month earlier is the point.

relies on

the "GPT-5 solved 10 Erdős problems" fiasco, ai/GPT-5

enabled

an openai model disproves the erdős unit distance conjecture

the equational theories project completes formal

Tao and a large open collaboration · all 22,028,942 implications Lean-verified · arxiv.org

Every implication among the 4,694 simplest magma laws is now settled and checked. Within nine days of the September 2024 launch the graph was 99.866% complete; the residue took over a year and produced a genuinely new object, magma cohomology, invented to handle a family of stubborn non-implications. Automated provers and LLMs generated bulk proofs and counterexample magmas at a scale no human team could match; volunteers handled the hard cases; Lean checked everything. This is the template Tao then reused for the Erdős problems effort.

relies on

the equational theories project

erdős #728: "the most unambiguous instance" proof

GPT-5.2 Pro prompted by Barreto; Lean by Aristotle; assessed by Tao · Lean-verified; human write-up arXiv:2601.07421 · erdosproblems.com arxiv.org

Erdős proved in 1968 that a!·b! | n! forces a + b ≤ n + O(log n). Problem #728 (Erdős, Graham, Ruzsa, Straus, 1975) asks whether that slack is attainable: for C > 0, are there infinitely many a, b, n of comparable size with a!·b! | n!·(a+b−n)! and a + b > n + C log n? Substituting turns it into binomial divisibility, C(N,k) | C(N,a), and prime by prime into Kummer's theorem: the p-adic valuation of a binomial coefficient counts the carries when adding in base p. The model found integers whose base-p expansions generate many carries across all relevant primes simultaneously, with b = n/2, a = n/2 + O(log n), for any window C₁ log n < a + b − n < C₂ log n. Nobody had a solution to retrieve.

Tao called it "perhaps the most unambiguous instance" of AI solving an open problem, and said the win "says more about speed than difficulty": the problem was obscure, arguably ambiguous, and had degenerate readings that had to be excluded by hand. By this point the Aristotle pipeline (frontier model finds the argument, Aristotle formalizes it, a forum participant curates) was producing Erdős solutions roughly weekly, alongside ten documented cases where AI claims were flatly wrong.

relies on

deepseek-prover, ai/GPT-5

enabled

erdős #1196 and #1217: a new method for primitive sets

bruhat intervals that are large hypercubes conjecture

Ellenberg, Libedinsky, Plaza, Simental, Williamson, with AlphaEvolve · human proofs; preprint · arxiv.org quomodocumque.wordpress.com

Bruhat order on the symmetric group controls Schubert varieties, Kazhdan–Lusztig theory and cluster algebras. Which posets occur as intervals? For the simplest case, a hypercube of dimension d, how large can d be inside S_n? AlphaEvolve, asked to search for permutations with unusually large "d-invariant", evolved a generator whose small-n outputs the human authors recognised as a pattern that works in general: for n a power of 2, intervals isomorphic to hypercubes of dimension Θ(n log n), the maximum possible up to a constant, in a 50-year-old heavily studied order.

The cleanest example on this page of the machine's actual comparative advantage: not proving, but noticing an object nobody thought to look for. The theorem is human-proved.

relies on

alphaevolve: 48 multiplications for 4×4, kissing number 593 in dimension 11, kazhdan–lusztig polynomials: a conjectural recursion from a GNN

aletheia: erdős #1051 and a paper written by itself proof

Google DeepMind (Gemini 3 Deep Think agent); Feng; Kovač et al. · #1051 Lean-verified; eigenweights preprint under a human author of record · erdosproblems.com arxiv.org arxiv.org arxiv.org

Aletheia iterates generate → verify → revise in natural language with heavy tool use for literature navigation. It proved Erdős–Graham #1051: if a_n grows with liminf a_n^{1/2ⁿ} > 1, then Σ 1/(a_n a_{n+1}) is irrational. The follow-up is the pretty part: Barreto, Kang, Kim, Kovač and Zhang then found the sharp threshold, replacing 2 with the golden ratio φ; growth limsup a_n^{1/φⁿ} = ∞ forces irrationality and any slower growth admits rational sums. The machine opened the door, humans found the threshold.

The same agent determined the "eigenweights" in Feng, Yun and Zhang's higher arithmetic Hirzebruch proportionality for all classical groups, via symmetric-group representation theory; Feng is the author of record and the abstract says the paper "documents work of a (custom) AI Agent". Of a 700-problem semi-autonomous Erdős sweep, DeepMind claims four solutions; erdosproblems.com credits three (#1051, and refutations of the strongest forms of #654 and #1040, whose main forms remain open).

relies on

IMO 2025: gold in natural language, ai/gemini 3

the first proof challenge benchmark

11 research mathematicians; entrants incl. OpenAI and Aletheia · expert-assessed; results contested · 1stproof.org scientificamerican.com arxiv.org

Ten unpublished research lemmas, the kind you hand a strong graduate student, several of which had resisted their own authors for years; one week; no human mathematical input allowed. Unpublished means retrieval is impossible; lemma-sized means grading is tractable.

The results depend on who is counting. Organisers judged only two of the ten public-model solutions unambiguously correct, with the remark that the correct ones "have the flavor of 19th-century mathematics". OpenAI claimed six likely correct; Aletheia was credited with six by majority expert assessment. The unresolved methodological problem was outside submissions with covert human help: "once there's humans involved, how do we judge how much is human and how much is AI?" A stricter second round followed in March.

relies on

frontiermath

erdős #1196 and #1217: a new method for primitive sets proof

GPT-5.4 Pro prompted by Price; write-up by Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang, Tao · #1196 Lean-verified; preprint with Tao and Lichtman as authors · arxiv.org erdosproblems.com

A set is primitive if no element divides another. Erdős showed in 1935 that Σ_{a∈A} 1/(a log a) is bounded over all primitive sets; the conjecture that primes maximise it was Lichtman's 2023 theorem. Problem #1196 (1968) asks the large-numbers version: for primitive A ⊂ [x, ∞), is the sum < 1 + o(1)? The model proved the sharp form, Σ_{a>x} 1/(a log a) ≤ 1 + O(1/log x). Problem #1217 (1966) on divisibility chains was proved without even needing the density hypothesis it came with.

What makes this the strongest "AI produced a method" claim on the page: the model's output suggested a general framework, Markov chains with von Mangoldt weights, which the authors say was "overlooked by the prior literature since Erdős's seminal 1935 paper", and which reproves Lichtman's Annals-level theorem in about a page. Lichtman is a co-author. Still a preprint.

relies on

erdős #728: "the most unambiguous instance"

enabled

erdős #4: first movement on large prime gaps since 2018

an openai model disproves the erdős unit distance conjecture proof

internal OpenAI reasoning model; digested by Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Matchett Wood · checked by nine external mathematicians; #90 marked disproved (Lean); explicit bound by Sawin · arxiv.org arxiv.org erdosproblems.com quantamagazine.org

Let u(n) be the most pairs at distance exactly 1 among n points in the plane. The √n × √n lattice gives n^{1+c/log log n}, and Erdős conjectured in 1946 that u(n) = n^{1+o(1)}. The upper bound O(n^{4/3}) of Spencer, Szemerédi and Trotter had stood since 1984, and Valtr showed it holds for a non-Euclidean metric too, so beating it needs something specifically Euclidean. Erdős offered $500.

The conjecture is false. The model built an infinite family of point sets with at least n^{1+ε} unit distances for a fixed ε > 0, and the construction comes from algebraic number theory. Erdős's lattice is the ring of integers of a fixed imaginary quadratic field; the model let the field vary, climbing an infinite class field tower of Golod–Shafarevich type to get CM fields of growing degree with bounded root discriminant, which keeps the lattices from spreading out. Split primes and pigeonhole give algebraic numbers of absolute value 1 with bounded denominators, and projecting the lattice to the plane gives the point set. The digested exponent is about 1 + 6×10⁻³⁸, a refutation on principle; Sawin optimised it within days to an explicit n^{1.014}.

A general-purpose reasoning model, not a maths system, not aimed at this problem. Quanta called it "the first historically significant proof to come from an AI model". The published argument is human-cleaned and simplified, and the model is unreleased. At ICM 2026 the panel treated it as the watershed, and noted the technique it exposed seeded human breakthroughs on the sum-product problem.

relies on

the "GPT-5 solved 10 Erdős problems" fiasco, early science acceleration experiments with gpt-5

enabled

the leiden declaration, astra: ten open problems with zero-sorry lean certificates, claude: more than two thirds of zeta zeros are simple and on the line

the leiden declaration benchmark

16 researchers from 15 universities; endorsed by the IMU · 130+ signatories; presented at ICM 2026 · leidendeclaration.ai cacm.acm.org

The governance response: disclose AI tools and compute used; provide formal proofs where feasible; accept human responsibility for correctness. The stated worry is that AI-generated proofs threaten "the accuracy, reliability and independent verifiability of mathematical research" and that companies bypassing peer review threaten "the integrity of proof and attribution". Its first test came within eight weeks, when OpenAI cited the declaration in the Astra announcement and then, facing prior-art complaints, reportedly read it as supporting attribution to AI rather than to earlier human authors.

relies on

an openai model disproves the erdős unit distance conjecture

enabled

astra: ten open problems with zero-sorry lean certificates, the long tail, and the profession takes stock

IMO 2026: perfect scores, and the grading tiers that got lost proof

Huawei Celia and RedNote dots-note-3.0 (officially graded); Claude Fable 5, GPT-5.6 Sol, Kimi K3, AxiomProver (self-administered) · official IMO certification for two systems only · scmp.com

Two systems scored 42 of 42 under the IMO's own process, the first perfect AI scores, including the combinatorics and geometry that had defeated every system a year earlier; seven of 666 humans did the same. Four more systems scored 42 on the same problems in a run by Menlo Ventures' Deedy Das, graded by Claude-based agents rather than human medallists, whose own repository says to treat the scores as "strong but not authoritative". Most coverage merged the tiers.

That the lightest model in a Chinese open-source-bound family saturates the IMO says competition mathematics is no longer a frontier benchmark. Neither OpenAI nor DeepMind appears in the officially graded 2026 results.

relies on

IMO 2025: gold in natural language

a counterexample to the jacobian conjecture in dimension 3 construction

Alpöge with Claude Fable 5; digested by Tao · elementary and checkable in minutes; no preprint or Lean as of September · terrytao.wordpress.com johndcook.com

Keller's 1939 conjecture: a polynomial map F: ℂⁿ → ℂⁿ with non-zero constant Jacobian determinant is globally invertible with polynomial inverse. Constant Jacobian makes F a local diffeomorphism everywhere; the question is whether local upgrades to global. Eighty-seven years, a large literature of false proofs, a known reduction to the cubic-homogeneous case.

The counterexample is explicit in ℂ³:

F(z₁,z₂,z₃) = ( (1+z₁z₂)³z₃ + z₂²(1+z₁z₂)(4+3z₁z₂),
                z₂ + 3z₁(1+z₁z₂)²z₃ + 3z₁z₂²(4+3z₁z₂),
                2z₁ − 3z₁²z₂ − z₁³z₃ )

with det DF = −2, yet three distinct points share an image. That settles every dimension n ≥ 3 negatively and leaves n = 2, the case tied to the Dixmier conjecture, open. Verification is trivial next to discovery: a computer algebra system checks it in seconds. Tao's digestion exists because the identities "appear like a massive miracle" and the AI's output supplied no geometric motivation. How it was found has not been revealed.

relies on

ai/claude fable 5 and mythos 5

astra: ten open problems with zero-sorry lean certificates proof

OpenAI (unreleased Astra) · Lean 4, zero sorrys, publicly buildable; no journal review; two prior-art complaints · openai.com siliconangle.com arxiv.org

A 249-page manuscript and Lean certificates for ten results each open ten or more years, for roughly $2,000 of inference. The first explicit non-sofic group: a group is sofic if it can be approximated by finite symmetric groups in a precise metric sense (Gromov 1999), soficity implies Gottschalk surjunctivity, Kaplansky direct finiteness and Connes embedding for the group algebra, and no non-sofic group had been known for 27 years. A disproof of Connes's rigidity conjecture for von Neumann algebras (not the embedding problem, refuted in 2020 by MIP* = RE). The inequality part of Ehrhart's volume conjecture, whose equality case fell independently days later to GPT-5.6 Sol, Claude Fable 5 and the Danus system. The first improvement to the high-dimensional sphere-packing upper bound since 1978. An n⁴/log n lower bound for the permanent, n^{1/400} hardness for the closest vector problem, an exponential parallel repetition theorem for quantum games, better binary and spherical codes, and three Erdős problems, including super-exponential growth of multicolour triangle Ramsey numbers.

Bloom rated the ten above the unit distance result. Then two of them drew named complaints: Steven Miller said the sphere-packing proof reused an argument from his 2016 paper without credit, and Francesco Fournier-Facio identified the non-sofic construction as combining 2016 and 2019 papers without acknowledgement. OpenAI said it would take responsibility and issue updates. A zero-sorry build guarantees the Lean statements, not that they faithfully render "there exists a non-sofic group" as group theorists mean it, which is exactly the gap Palomar was built to check two weeks later.

relies on

an openai model disproves the erdős unit distance conjecture, the leiden declaration, ai/GPT-6 astra

enabled

palomar: a registry of lean-verified mathematics

counterexample to the HRT conjecture construction

Faulhuber, Petersen, van Velthoven, Voigtlaender, with ChatGPT; digested by Tao · human-written proof with numerical certification · terrytao.wordpress.com

Heil, Ramanathan and Topiwala conjectured in 1996 that for any non-zero f ∈ L²(ℝ) and any finite set of distinct time-frequency points, the shifts e^{2πiξ_k·} f(· − x_k) are linearly independent. Known for three points, for lattices, for special configurations, and otherwise intractable for thirty years. The counterexample uses twelve shifts of a Schwartz function on the lattice ℤ × ½ℤ, and needs a numerical bound: an operator norm difference must fall below 1/3, and it comes in at about 0.333032.

ChatGPT helped with the initial strategy; the final arguments were written by hand, and Tao cites the paper as the model of responsible disclosure. His assessment tempers the drama: it "extends only slightly beyond previously known positive results", from three points to twelve, off the standard lattice. The tight margin is where an independent recomputation would be valuable.

claude: more than two thirds of zeta zeros are simple and on the line proof

unreleased Claude research model, driven by Sumner; verified by Alpöge and Furman; reviewed by Conrey and Goldston; reproved by Lamzouri · expert-reviewed, Lean-formalized, independently reproved; not journal-refereed · anthropic.com arxiv.org arxiv.org github.com scientificamerican.com

The Riemann Hypothesis says every non-trivial zero of ζ(s) has real part 1/2. The standard partial result is a positive proportion: what fraction of zeros, counted with multiplicity in the limit, provably lie on the line? Levinson got a third in 1974, Conrey two fifths in 1989, Bui, Conrey and Young 41.05% in 2010, and Pratt, Robles, Zaharescu and Zeindler 5/12 ≈ 41.67% in 2020. Fifty-two years moved the bound about eight points. This moved it to 67.25% simple and on the line, and 83.62% distinct, unconditionally, with extensions to Dirichlet L-functions.

The method breaks from Levinson's mollifier calculations. It takes a finite compression of Weil's Hermitian form (the explicit-formula quadratic form whose positivity is equivalent to RH), represents it as a Gram matrix, and counts positive directions with a rank–trace inequality and Sylvester's law of inertia, fed by a second-moment computation over the zeros and by unconditional pair-correlation input from Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh. Three weeks later Lamzouri gave a shorter human proof of the same numbers, replacing the matrix framework with a Hilbert-space inequality; his abstract calls the AI argument "technically intricate" with a mechanism "not immediately transparent".

How it was found: two Claude Code sessions, 31 million output tokens, about 650 candidate ideas, roughly 60 subagents running 2,400 shell commands, subagents hunting counterexamples, 54 arXiv papers pulled to check novelty, then an independent re-derivation. The operator, not a mathematician, mostly told it to keep going. The verification package is the strongest on this page: two Anthropic mathematicians as authors of record, the two people who held the previous records as reviewers, a Lean formalization registered in Palomar, released transcripts, and an independent reproof.

This is not progress toward RH, and Anthropic said so. Maynard: "even being very optimistic, there is no pathway for any of these approaches to deal with the actual Riemann hypothesis"; density 1 on the line is compatible with a sparse set of zeros off it. What he does endorse: "the problem was in need of a new real idea, which this new result seems to provide."

relies on

ai/claude fable 5 and mythos 5, ai/context engineering: compaction, memory, subagents, an openai model disproves the erdős unit distance conjecture

enabled

sendov's conjecture, for all degrees, the navier–stokes rumour, finite-time blow-up with smooth forcing for IPM, boussinesq and 3D euler

sendov's conjecture, for all degrees proof

an AI tool used by Mazur; digested and Lean-formalized by Tao · Lean-verified; registered in Palomar · terrytao.wordpress.com

If a polynomial of degree n ≥ 2 has all roots in the closed unit disk, then within distance 1 of every root there is a critical point. Conjectured in 1958, known by case analysis for small n and, by Tao's own 2020 compactness argument, for all sufficiently large n with no effective threshold. The new proof covers every n ≥ 2 and is elementary: basic algebra and the Maclaurin inequality, nothing beyond the fundamental theorem of algebra.

The raw output was about 90,000 lines of Lean. Tao spent several days, with heavy AI assistance, turning it into a readable argument and a 15,000-line formalization. That six-fold compression is the concrete measure of the digestion debt AI proofs create. This one got paid because Terence Tao paid it, which does not scale. The originating system is not named in the source.

relies on

claude: more than two thirds of zeta zeros are simple and on the line

enabled

palomar: a registry of lean-verified mathematics

a hadamard matrix of order 668; elliptic curves of rank 30 and 31 construction

Anthropic researchers with Claude; Alpöge, Howell · self-certifying objects; Epoch attribution provisional · epoch.ai epoch.ai

Two FrontierMath Open Problems solved by search. A Hadamard matrix is an n×n ±1 matrix with HHᵀ = nI; they can exist only for n ≡ 0 mod 4, the conjecture that they always do is open since 1893, and 668 had been the smallest unknown order since 428 fell in 2005. Then explicit elliptic curves over ℚ with 30 and, three days later, 31 independent rational points, breaking Elkies's chain of records (28 in 2006, 29 with Klagsbrun in 2024); the ranks are exactly 30 and 31 assuming BSD and GRH.

Both are self-certifying: multiply the matrix, compute a height-pairing determinant. Epoch marked them AI-solved provisionally, pending details of the human share, and the next day marked the inverse Galois problem for M₂₃ as human-solved despite AI involvement because an author said the boundary "is not clear". Epoch's bar, that the core ideas be unambiguously the machine's, is the most rigorous attribution standard in use. Its tier breakdown is the best calibration number of the year: of 50 open problems, 6 solved by AI, 5 of them "moderately interesting", 1 a "solid result", none of the 9 rated "major advance" or "breakthrough".

relies on

frontiermath, ai/claude fable 5 and mythos 5

alphaevolve improves the matrix multiplication exponent construction

DeepMind with Alman and Vassilevska Williams · certified numerical solution; preprint with the human record-holders · arxiv.org

ω < 2.371177, from 2.371339. Since Coppersmith and Winograd, progress on the exponent comes from the laser method and its combination-loss refinements, at whose core sits a large, badly conditioned non-convex optimisation. The paper reformulates it in a larger setting, designs a new optimiser, and lets AlphaEvolve evolve the optimiser's code. Twelve years have moved ω from 2.3728639 to here; each step is hard, all are galactic, and the AI's role is optimisation rather than insight.

relies on

mathematical exploration and discovery at scale

palomar: a registry of lean-verified mathematics formal

Lean FRO and ICARM; advisory board incl. Tao, Avigad, Kra, Vakil, Venkatesh · live, arXiv-style, explicitly not peer review · terrytao.wordpress.com

The structural response to AI proof announcements outrunning human verification. A submission is a challenge file stating the result in Lean, a solution module, and an informal description. Two checks: a tool called Comparator confirms the solution proves exactly the challenge statement with no extra axioms, and an LLM review checks that the informal description matches the formal one. The second check is the crux, because the failure mode of AI Lean proofs is not a wrong proof (Lean forbids that) but a formal statement that does not say what the English claims. Over 116 results registered by late August, including Tao's Sendov formalization and Anthropic's zeta project. It validates statement fidelity, not significance or prior art; it would not have caught the Astra complaints.

relies on

astra: ten open problems with zero-sorry lean certificates, sendov's conjecture, for all degrees

enabled

the long tail, and the profession takes stock

erdős #4: first movement on large prime gaps since 2018 proof

GPT-5.6 Pro, prompted on the erdosproblems.com forum · recorded on erdosproblems.com; no preprint, no Lean · erdosproblems.com

How large can p_{n+1} − p_n be infinitely often? Rankin's 1938 shape, Erdős's $10,000 for an arbitrarily large constant (settled 2016 by Maynard and by Ford, Green, Konyagin and Tao), and then all five together in 2018:

p_{n+1} − p_n ≫ log n · log log n · log log log log n / log log log n

The model improved this to ≫ log n · log log n / log log log log n, combining new sieving ideas with the 2018 framework. Analytic number theory is exactly where AlphaEvolve had conspicuously failed a year earlier, and the 2018 argument is not a soft target, so this is the most technically impressive Erdős contribution on the page. It is also the least documented: verification rests on the forum. It deserves scrutiny it has not yet received.

relies on

erdős #1196 and #1217: a new method for primitive sets, ai/GPT-6 astra

the long tail, and the profession takes stock benchmark

whataifound.org; Venkatesh, Vakil, Kontorovich at ICM 2026 · heterogeneous · whataifound.org quantamagazine.org

By September the rate of AI-attributed results had reached roughly one per day: an independent registry lists 112 entries, 65 well-verified, 45 AI-led, 5 contested, ranging from Marton's inner bound not being tight to an Albertson–Berman counterexample later reproduced without AI, to a claimed complex structure on S⁶ that should be treated with maximum caution. Bloom's warning applies: 100-to-200-page AI papers posted by non-mathematicians that "no human has read". erdosproblems.com stood at 565 solved and 652 open, and Alon observed that once AI began solving them, pursuing them lost appeal for humans.

At the ICM panel nobody disputed that AI now produces new mathematics. The live disagreements are about verification infrastructure, attribution, funding and pedagogy. Venkatesh: mathematics is closer to storytelling than to proof production. Vakil: "proof is not the central activity", and beware anti-intellectualism dressed as AI-driven necessity. Tao, earlier in the year: "scattered successes among a big sea of unreported failures", and "this guy's got a shovel, this guy's got a pickax, together we can bore a tunnel."

relies on

palomar: a registry of lean-verified mathematics, the leiden declaration

claude formalizes fermat's last theorem in eleven days formal

Anthropic (internal research model comparable to Fable 5.1); reviewed by Buzzard · Lean 4, zero sorrys, three standard axioms; statement matched to Mathlib's by Comparator · anthropic.com lean-lang.org aiweekly.co

Kevin Buzzard's Imperial project to formalize Fermat's Last Theorem launched in 2024 with EPSRC funding to 2029 and a blueprint that experts expected to take the better part of a decade. Claude produced a complete machine-checked proof in a little under two weeks of wall-clock time: 13 million lines of Lean, about 30,300 theorems proved and 29,500 used, more than five times the size of Mathlib, following the Darmon–Diamond–Taylor exposition of Wiles's argument rather than the 1995 original, and adapting pieces of the Imperial blueprint. The final artefact uses only Lean's three standard axioms with no sorry, and Comparator confirmed the top-level statement matches Mathlib's own.

How it ran: several dozen agents in parallel on the Prove2Me platform, about 6 billion output tokens. The first attempt failed; roughly 7% of the non-boilerplate lines come from abandoned efforts. Anthropic's own caveat is that the proof "is likely much longer than it needs to be". Buzzard called it "an extraordinary autoformalization achievement" spanning algebra, harmonic analysis, geometry and number theory.

This is a known theorem, not new mathematics, and the same category as Gauss's strong PNT a year earlier. What changed is the scale: the largest formalization ever built, by a wide margin, in under two weeks. The open question it raises is the one Han flagged for the PNT project, now at 13 million lines: no human is familiar with this artefact, and a proof that only the kernel has read is a different kind of object from one the community has absorbed.

relies on

gauss autoformalizes the strong prime number theorem, mathlib ported to lean 4, ai/context engineering: compaction, memory, subagents, ai/claude fable 5.1 and mythos 5.1

enabled

the navier–stokes rumour, finite-time blow-up with smooth forcing for IPM, boussinesq and 3D euler

the navier–stokes rumour proof

an X post; amplified widely; no lab claim · no paper, blog, Lean repo or Clay submission exists · kingy.ai explainx.ai x.com

Two days after the FLT announcement, a viral claim said Claude had solved Navier–Stokes, the proof was "out for expert review", and Anthropic would announce before its IPO. It began as one user's stated prediction and gained weight when Tao posted a hypothetical about AI solving the problem, which some read as inside knowledge; Tao said he knew of no breakthrough. A second version, over the following days, said OpenAI had an internal proof for the forced problem. As of this entry nothing exists publicly from either lab: no paper, no post, no formalization, and the Clay Institute lists the problem as open.

The rumour is worth an entry because it is the failure mode the reading checklist predicts. Two verified, Lean-checked results in a month made a third claim plausible on vibes alone, and the specific unverified assertion attached itself to the nearest real work, which is the next entry. Read that one for what actually happened.

relies on

claude: more than two thirds of zeta zeros are simple and on the line, claude formalizes fermat's last theorem in eleven days

finite-time blow-up with smooth forcing for IPM, boussinesq and 3D euler proof

Alpöge (Anthropic), Buckmaster (NYU), with Coiculescu on IPM; building on Córdoba and Martínez-Zoroa; assessed by Tao · Lean-formalized; preprints released incomplete; heavily AI-assisted · terrytao.wordpress.com officechai.com officechai.com

The real result behind the rumour. Three preprints, about 57, 76 and 112 pages, prove that smooth initial data can develop a finite-time singularity under a smooth external forcing term for the incompressible porous medium equation, the two-dimensional Boussinesq equation, and the three-dimensional incompressible Euler equations. Córdoba and Martínez-Zoroa had shown blow-up for IPM with rougher, less physical forcing; getting the forcing all the way to smooth is the harder version, and Alpöge and Buckmaster found a variant of their method that extends to Boussinesq and Euler. Tao's summary of the strategy: iteratively build the solution by repeatedly adding small high-frequency corrections to a previous forced solution, keeping the forcing smooth while the solution becomes increasingly singular toward the blow-up time.

Tao called it "a remarkable achievement" and said the construction "has a high likelihood of also extending to Navier–Stokes", and that blow-up from smooth data with no forcing at all should eventually be feasible. That is a research direction with, in his words, enormous remaining technical difficulties, particularly around spatial cutoffs; it is not a Navier–Stokes proof, forced or unforced, and the Millennium problem concerns the unforced equation. A separate group (Ganeshram, Duruisseaux, Anandkumar) reports numerical evidence and certified ingredients for unforced Euler with the quantitative certification unfinished.

The AI share is documented in the papers: Claude wrote the Lean code under Alpöge's direction, and did literature work, drafting and the bookkeeping of constants. Tao's description of the raw output is the digestion problem stated bluntly: the authors spent weeks turning "the worst writeup we had ever seen in the history of mathematics" into something professional, and the preprints were released before that was finished because of external events. Those events are the dispute: Buckmaster says OpenAI told him it had an internal hundred-page forced Navier–Stokes proof by the same narrow approach, begun only after learning of his work, that he was pressured over co-announcement and authorship, and that he never got a clear answer on whether the model had seen his Codex-stored drafts, while stating "I have not seen it". Bubeck called the allegations "false and inflammatory". Nothing from OpenAI has been made public.

relies on

unstable singularities in fluid equations, claude: more than two thirds of zeta zeros are simple and on the line, claude formalizes fermat's last theorem in eleven days