Mathematical reasoning & formal theorem proving

Mathematics and software verification suffer from a trust bottleneck: proofs are long, reviewer time is scarce and errors slip through. Reasoning LLMs can now draft solutions, and coupled with a proof assistant such as Lean 4 every step is checked by a small trusted kernel, so a hallucinated proof is rejected automatically. The result is a verifiable AI use case: researchers get lemma search and proof automation, engineers get verified code and specifications, teachers get checked solutions.

Problem & value

• Today: formalising a theorem in a proof assistant is slow expert work; mathematicians check papers by hand; formal verification of software, protocols or smart contracts is limited to a few specialist teams.
• AI value: (1) solving, where reasoning models handle competition and research-level problems in natural language; (2) formal proving, where models generate Lean/Isabelle proofs that the kernel accepts or rejects; (3) autoformalisation, translating informal statements and papers into formal ones; (4) proof maintenance, repairing proofs broken by library updates.
• Key property: the verifier is exact, so output can be trusted without trusting the model. This makes it one of the few AI domains with a perfect reward signal for reinforcement learning.
• Evidence of progress: DeepMind's AlphaProof and AlphaGeometry 2 reached silver-medal level at IMO 2024, and in 2025 several systems (Google Gemini Deep Think, OpenAI, and the formal-proof startup Harmonic with Aristotle) reported gold-medal-level IMO performance [1][2]. Benchmarks such as miniF2F are close to saturation, while research-level and undergraduate-level suites such as PutnamBench remain far from solved [3][4].
• No reliable, sourced productivity figures exist yet for industry; measure locally.

Variants

• Research mathematics: lemma search, proof-step suggestion, formalisation of papers into Mathlib.
• Education: step-checked tutoring and exercise verification (see EDU-001); checking student proofs.
• Software and protocol verification: proofs about code, cryptography, smart contracts and distributed systems (Dafny, Verus, Lean, Isabelle, Rocq); links to CODE-019 and SCI-016 (hardware verification).
• Quantitative modelling: solver-backed reasoning for finance, actuarial or engineering formulas using computer algebra (SymPy, Mathematica, SageMath) and SMT solvers (Z3, cvc5).
• Private use: homework help and puzzle solving with a reasoning chat model; formal checking is optional.

How it works

1. problem (natural language / formal statement)
2. autoformalisation (LLM: statement
3. Lean 4) [human checks the statement]
4. premise retrieval (embedding search over Mathlib / project library)
5. proof search (LLM proposes tactics or whole proofs; best-first or tree search; sampling at scale)
6. verification (Lean kernel / Isabelle / Rocq compiles; errors fed back to the model)
7. repair loop (agent reads error messages, edits, retries; decomposes into lemmas)
8. accepted proof + audit (statement fidelity review by a human)

• Reasoning models produce informal strategies; specialised provers produce tactic or whole-proof Lean code, trained with reinforcement learning against the verifier on large synthetic problem sets.
• Tool use: agents call the Lean REPL or language server, exact?/aesop/omega automation, Sledgehammer (Isabelle), CAS and SMT solvers.
• Human-in-the-loop: the proof is trusted, but the formal statement may not capture the intended claim. A domain expert must review the statement, definitions and axioms (check for sorry, added axioms, vacuous truth).

Data preparation

Data needs are modest compared with other use cases: problem statements, informal proofs, formal libraries (Lean Mathlib, Isabelle AFP) and, for verification, specifications and source code. These sit in papers (LaTeX, PDF), course notes, wikis, git repositories and engineers' heads. Typical gaps: informal specifications, ambiguous notation, missing formal statements for informal results, scattered lecture material and no benchmark of own problems.

Preparation steps: collect problems with agreed formal statements; translate key definitions into the proof assistant library (autoformalisation with human check); structure code and specifications in version control (PREP-009); write down terminology and conventions (PREP-015); gather solved examples as gold standard (PREP-016); and build a small evaluation set of own problems (PREP-018). Tools: Lean with Mathlib, LeanDojo-style extraction, Pandoc for LaTeX conversion.

Expect only about 10 to 20 percent of effort in data preparation; most effort goes into formalising statements correctly. See GUIDE-003.

Implementation paths

Which path for whom

• Developer: Path B. Reasoning-model APIs combined with a local Lean or Isabelle toolchain give the strongest results with little setup.
• Enterprise (verification, safety-critical software): Path B. APIs plus in-house proof tooling suit pilot projects; keep proprietary specifications out of prompts or use EU regions.
• Public (universities, schools): Path C. Open provers and open-weight models on university compute avoid licence costs and keep research reproducible.
• Private: Path A. Consumer chat assistants with a free Lean installation are enough for learning and hobby use.

Path A — Buy (off-the-shelf)

• Reasoning assistants: frontier chat products with extended thinking (Anthropic Claude, OpenAI, Google Gemini Deep Think, Mistral, EU) for informal mathematics; computer algebra systems (Wolfram, Maple) with AI front-ends.
• Formal tools: Harmonic's Aristotle (Lean proofs as a service), Axiom Math and Math Inc (autoformalisation products, early access). Verification tooling: Imandra (UK), Certora (smart contracts), AWS Zelkova/Cedar tooling for policy verification.
• Choose A when: you need occasional help or a quick pilot; formal verification at scale is a specialist service.

Path B — Build on cloud APIs (recommended)

• Models: frontier reasoning models via API (Claude, Gemini, GPT, Mistral in EU regions) driven by an agent loop that calls a Lean 4 + Mathlib sandbox; feed compiler errors back; cap attempts and cost.
• Stack: Lean 4 and Mathlib, LeanDojo or the Lean REPL for programmatic interaction, Lean Copilot for in-editor suggestions, retrieval over Mathlib docstrings with an embedding model [5][6].
• Integration: CI that rejects any proof containing sorry or new axioms; results stored as certificates next to code.

Path C — Self-host (open source)

• Open-weight provers: DeepSeek-Prover-V2 (7B and 671B), Kimina-Prover, Goedel-Prover-V2 (Princeton), Seed-Prover (ByteDance, partly open) and Qwen/DeepSeek reasoning models for informal work [3].
• Serving: vLLM or SGLang; Lean workers in containers (many parallel compilers are CPU-bound).
• Hardware: HW2/HW3 for 7–32B provers; HW4 for the 671B-class models; search needs many samples per problem.
• Proof assistants: Lean 4 (Lean FRO), Isabelle (TU Munich/Cambridge), Rocq (Inria, France), all open source.

Path D — Custom training

Worthwhile for organisations with a private formal library (e.g. a verified OS, protocol or numerical library). Fine-tune a 7B–32B prover with expert iteration or RL using the proof assistant as reward. Needs a corpus of formal statements (thousands), a compute budget for sampling, and verification engineers. Public recipes exist [3].

State of the art (2026)

• Competition mathematics is essentially at gold-medal level for the best systems, in natural language and in Lean [1][2]. Open models trail closed ones but the gap on miniF2F is small; PutnamBench and research-level tasks remain hard, so check current leaderboards before choosing a model [3][4].
• Autoformalisation is the weakest link: statements are often subtly wrong, so evaluation focuses on fidelity.
• Whole-proof generation plus agentic repair has replaced pure tree search in most recent systems.
• Formalisation projects (Mathlib, Fermat's Last Theorem effort led by K. Buzzard) are starting to use AI for routine lemmas; large-scale AI-assisted formalisation of papers is an active area.
• Limits: failure on long, novel arguments; proofs that are valid but unreadable; dependence on library coverage; correct proof of a wrongly stated theorem; no guarantee that a model finds a proof even if one exists.

Shared resources & combinations

• Same stack (llm-reasoning + llm-code + agent-framework): SCI-011 AI scientist agents (verify generated claims), CODE-019 and SCI-016 (formal verification of hardware/RTL), SCI-013 (requirements formalisation in MBSE).
• Hardware: a shared vLLM server (HW3/HW4) serves reasoning, coding and proving; Lean workers need CPU only.
• Related: AGENT-001 (general agents), EDU-001 (tutoring with step checking).

Effort, cost & KPIs

• Path A: days; subscription or per-use pricing.
• Path B: 1–3 months for an agent plus Lean sandbox; cost driven by sampling many attempts per problem.
• Path C: 3–6 months; GPU node plus Lean expertise.
• Path D: 6+ months; needs proof engineers.
• KPIs: proof success rate at fixed budget (pass@k), cost per verified proof, statement-fidelity review pass rate, human review minutes per proof, share of lemmas automated, time to formalise a paper section.

People & change

Involve management for the decision on pilot scope, the department lead or professor as process owner, the researchers, engineers or teachers as end users, and IT for compute, API keys and toolchain installation. Data protection is rarely an issue because mathematical content is not personal; ask the DPO only if student work or employee data are submitted (GUIDE-005). Company specifications may be trade secrets: set rules in the AI policy (GUIDE-007).

Works council: usually no. The proof tools do not monitor behaviour, and the proof assistant itself checks results rather than people. If a company-wide AI platform logs individual prompts, §87(1) no. 6 BetrVG may apply to the platform, not to this use case. Inform the works council early anyway under §90(1) no. 3; schools and universities involve the staff council.

AI literacy: Art. 4 AI Act requires measures that support staff's AI literacy; show colleagues that a machine-checked proof is reliable but that the formal statement may still be wrong (GUIDE-006). Pilot with a small group on a few real problems. Typical concern: cheating in education or loss of mathematical skill. Address it by clear course rules, keeping humans responsible for stating and interpreting theorems, and treating the checker as the final authority (GUIDE-008).

Risks, regulation & compliance

• EU AI Act: minimal risk for research and education support (Art. 4 AI literacy applies). Educational use that evaluates learners or steers admissions can become Annex III high-risk; plain tutoring does not. Verification of safety components (medical devices, machinery) stays under sector rules; the AI output is evidence, not certification [7].
• GDPR: normally no personal data; if student work or researcher identities are processed, EU hosting and a data processing agreement apply.
• Intellectual property: unpublished research and proprietary specifications sent to a cloud API; prefer EU regions or Path C for sensitive content.
• Risks and mitigations: misformalised statements (expert review), over-trust in informal LLM proofs (require kernel check), hidden axioms/sorry (CI gate), benchmark contamination in vendor claims (test on your own problems).

Getting started

1. Install Lean 4 and Mathlib; reproduce a small proof by hand to learn the verification loop.
2. Run a reasoning model on 20 of your own problems, informally first, then through a Lean REPL agent loop.
3. Try an open prover (DeepSeek-Prover-V2 7B or Goedel-Prover-V2) on a single GPU and compare with an API model.
4. Add CI checks: no sorry, no new axioms, pinned Mathlib version, statement review checklist.
5. Pick one real target (a library lemma set or a specification) and track the KPIs above for a month.

Sources

1. Google DeepMind — AI achieves silver-medal standard solving IMO problems (AlphaProof, AlphaGeometry 2) — https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
2. Google DeepMind — Advanced Gemini Deep Think achieves gold-medal standard at IMO 2025 — https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/
3. DeepSeek-Prover-V2 paper (arXiv 2504.21801) — https://arxiv.org/abs/2504.21801
4. PutnamBench — https://github.com/trishullab/PutnamBench
5. Lean programming language and theorem prover — https://lean-lang.org/
6. Mathlib4 — https://github.com/leanprover-community/mathlib4
7. Regulation (EU) 2024/1689 (AI Act) — https://eur-lex.europa.eu/eli/reg/2024/1689/oj
8. LeanDojo — https://leandojo.org/