AI for Mathematics

Definition

The use of language models to produce new mathematical results — not to tutor, not to retrieve known theorems, but to settle questions the literature had left open — and the separate machinery used to check that what they produced is correct.

The field splits along that seam. Generation is a frontier-model capability, run at inference time with long chain-of-thought. Verification is a distinct artefact: a proof assistant such as Lean 4 re-checks the argument line by line, mechanically, without trusting the model that wrote it. The two halves have different vendors, different licences and different failure modes, and conflating them is the main way claims in this area get overstated.

Why It Matters

• It is the cleanest available test of whether a model produced something new. Most benchmark disputes reduce to harness configuration — see Eval Harness Configuration. A previously open conjecture has no harness to configure. Either the proof stands or it does not.
• Verification is mechanical in a way almost nothing else in evaluation is. A Lean certificate can be checked by anyone with a laptop and no access to the model, the weights, or the lab. That is a stronger form of reproducibility than any leaderboard offers.
• It is a pacing signal. Labs have begun quoting research output as evidence of capability instead of benchmark scores — see Frontier Pacing. When the claim moves from "scores 51 on an index" to "settled a question open since 1978", the thing being measured has changed, and so has who is qualified to check it.

State of the Art (2026-08-11)

A record moves by 0.000162, and the AI is refining an optimizer — AlphaEvolve, 2026-08-19. Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (arXiv:2608.16884) improves the best known upper bound on the matrix multiplication exponent ω from 2.371339 to 2.371177, in three steps: reformulating the optimization problem at the core of combination loss analysis (the laser-method refinement credited to Duan et al. 2022, Williams et al. 2024, Alman et al. 2025) so it can be solved in a larger setting, designing a new optimization algorithm for it, then refining that algorithm with AlphaEvolve (source).

The division of labour is the point, and it is the opposite of the usual framing. AlphaEvolve proves nothing here. It refines a search procedure that humans reformulated and designed, over a space humans defined, inside a method three prior papers built. That is a narrower and more legible claim than the entries below it — and unlike them it needs no certificate machinery: the previous record is a published number, the new one is a published number.

The magnitude belongs in the same breath as the result. The bound moves by 0.000162, records on ω have moved in increments of that size for years, and the paper calls itself a note. What it demonstrates is a tool contributing at the frontier of a well-worked problem, not a problem that moved.

Caveat carried from the paper page: no author or affiliation was read, so whether this is a Google DeepMind paper or third-party use of AlphaEvolve is not established here.

An unreleased Claude — Anthropic, 2026-08-10. The proven lower bound on the fraction of nontrivial zeros of the Riemann zeta function lying on the critical line moved from 41.6% to 67.2%, reported as the largest single improvement in the problem's history, displacing a figure that took decades of human work. The result is formally verified in Lean with the proof public, and reviewed by named external number theorists (Brian Conrey, Dan Goldston). Anthropic states it is not a path to a full proof and that the bound was an unintended byproduct of attempting the hypothesis itself (source).

This is the first entry on this page where the verification is public, machine-checkable and independent of the lab's own account. The generation/verification split described below is the reason that matters: it is the first result here a sceptical reader can check without being granted access to anything. The mechanism is the other half — 650 ideas, ~60 subagents, 2,400 shell commands, 31M output tokens in an agent harness — which makes this search at a scale a person cannot run rather than a model emitting a proof. Full detail on More than two thirds of the zeros of the Riemann zeta function lie on the critical line.

Astra — OpenAI, 2026-08-01. Ten results in mathematics and theoretical computer science, each shipped with a Lean 4 certificate and a chain-of-thought walkthrough, plus a 249-page manuscript. Named results include the first explicit non-sofic group, a disproof of Connes' Rigidity Conjecture, a quantum parallel repetition theorem for general two-player entangled games, Ehrhart's volume conjecture, and the first improvement to the general high-dimensional sphere-packing upper bound since 1978. Problems are stated to have been open at least ten years. Total token cost approximately $2,000 at Sol API prices (source).

The human step is not incidental. Coverage of the Astra release states that humans organized the proofs into papers, which were then converted into Lean certificates (source). The same division of labour appears in the earlier result: when an internal OpenAI reasoning model disproved the planar unit distance conjecture (Erdős, 1946) on 2026-05-20, professional mathematicians read the model's reasoning transcript, extracted the key ideas and rewrote them as a succinct formal proof, and Princeton's Will Sawin refined the bound to δ = 0.014 (source). In neither case is the end-to-end pipeline reported as autonomous.

What changed between May and August is scale and checkability: one result became ten, and human-refereed prose became machine-checkable certificates.

Verification tooling is open where generation is not. Leanstral 1.5 (Mistral AI, 2026-07-01/02) is an Apache 2.0 open-weight Lean 4 theorem prover with a free API endpoint. The asymmetry is worth naming: the models that generate these arguments are closed and, in Astra's case, not released at all, while the tooling that checks them is open.

Search-based discovery is a separate lineage. AlphaEvolve (Google DeepMind) reaches mathematical and algorithmic results by evolutionary search over programs scored against an evaluator, rather than by long-form reasoning; it reached GA on the Gemini Enterprise Agent Platform on 2026-07-10. Gemini 3.1 Deep Think is the reasoning-side counterpart in that lab's line.

The community has stated its terms. The Leiden declaration on artificial intelligence and mathematics — published June 2026, endorsed by the International Mathematical Union, signed by Terence Tao, Peter Scholze, Kevin Buzzard and Scott Aaronson among others — lists five risks: unreliable results, missing citations, dependence on closed commercial systems, exaggerated claims, and loss of scientific independence. OpenAI cites it in the Astra post (source).

Open Problems

• A Lean certificate proves the theorem, not the interest. Formalization confirms that the argument establishes the formal statement. It cannot confirm that the formal statement is the one mathematicians care about — the translation from informal conjecture to Lean proposition is itself a human judgement, and an error there produces a machine-checked proof of the wrong thing.
• Peer review has no defined role yet. A Lean-checked argument is not a peer-reviewed one, and no journal process read here has stated how it treats one.
• Attribution is unresolved. When a model generates the idea, a mathematician writes the paper and a prover checks it, no convention read here says how the result is credited or cited — the second risk named in the Leiden declaration.
• The claims are not independently reproducible. Astra is unreleased, and so is the Claude research version behind the zeta bound — both labs' headline mathematical results in 2026 come from models nobody outside the lab can run. The certificates can be checked by anyone; the generation cannot be repeated by anyone, which is the third Leiden risk stated concretely. Public verification narrows this gap without closing it.
• No shared measure exists. There is no benchmark, baseline or common problem set on which two labs' mathematical output can be compared — only incommensurable lists of results.

Key Papers

• Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (2026-08, arXiv:2608.16884) — ω bound 2.371339 → 2.371177; AlphaEvolve refines the optimizer rather than proving the result → Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (arXiv:2608.16884) (source)
• Claude / Anthropic, More than two thirds of the zeros of the Riemann zeta function lie on the critical line (2026-08-10) — bound raised 41.6% → 67.2%, Lean formalisation public at anthropics/zeta-23-lean, reviewed by Brian Conrey and Dan Goldston → More than two thirds of the zeros of the Riemann zeta function lie on the critical line (source)
• OpenAI, Ten advances in mathematics and theoretical computer science (2026-08-01) — 249-page manuscript, Lean 4 certificates on GitHub (source)
• OpenAI, An OpenAI model has disproved a central conjecture in discrete geometry (2026-05-20) — the planar unit distance problem, via Golod–Shafarevich theory and infinite class field towers (source)
• Leiden declaration on artificial intelligence and mathematics (2026-06) — IMU-endorsed statement of five risks (source)

Related Concepts

• Reasoning Models — the generation half of the pipeline
• Test-Time Compute (Inference-Time Compute Scaling) — what the long chain-of-thought runs consume
• Eval Harness Configuration — why an open conjecture is a cleaner claim than a benchmark score
• Frontier Pacing — research output used as a capability claim