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-02)

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. The certificates can be checked by anyone; the generation cannot be repeated by anyone outside OpenAI, which is the third Leiden risk stated concretely.
• 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

• 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