Part II: Machine Learning for Theorem Proving

Wenda Li

University of Edinburgh

ICML 2026 Tutorial — Proving Theorems with Lean and Machine Learning

Where we are

Part I, in one line: Rémy showed you Lean as a proof language — how humans write trusted ML-theory proofs.

Part II flips the arrow: machines writing the proofs.

1. The game of theorem proving: history & methodology

2. Success stories

3. Overview of approaches & benchmarks

4. Limitations & the near future

5. Demonstration + wrap-up

Why should an ICML audience care?

1. Verified reward: theorem proving is the rare domain with a perfect, cheap, automatic reward signal — a paradise for RL and test-time search.

2. Frontier capability benchmark: IMO gold (2025), Putnam 12/12, first research-level results — progress is fast and measurable.

3. You can use it today: AI copilots for formalising your own ML theory.

Could your next ML theory paper come with a machine-checked appendix?

§1 · Theorem proving in Lean as a game

The "AlphaGo for mathematics" framing — with a twist:

the action space is infinite, and the "board" is a proof state (or state of Lean).

A brief history: symbolic → neural

Takeaway: ML for theorem proving is older than the LLM era — but the LLM era changed everything.

Classical ML tasks in theorem proving

Tactic prediction + proof search

A proof assistant is a game engine — state: local context + goal(s); action: a tactic; terminal reward: kernel accepts ⇒ 1, else 0 — no false positives.

Yang et al., "Formal Mathematical Reasoning: A New Frontier in AI" (2024)

The core loop: agent–prover interaction

Everything in §3 is an instance of this loop with different design choices.

§2 · How far have we come?

miniF2F pass rate:

≈29% (GPT-f/PACT, 2021) → 99.6% (Seed-Prover, Jul 2025)

— with AlphaProof scoring perfect on miniF2F-valid along the way (test-time RL; Nature 2025).

The yardstick of the field for four years — now saturated.

AlphaProof: silver at IMO 2024

What it did:

• 4/6 problems, 28/42 — one point below the gold cutoff.

• Solved P1, P2, and P6 (hardest; only 5 human contestants solved it); AlphaGeometry 2 solved P4 in 19 s; both combinatorics problems unsolved.

How:

• AlphaZero-style RL over Lean; ~1M informal problems autoformalised into ~80–100M formal statements as the RL curriculum.

• Test-time RL: generating and proving variants of the target problem — minutes for one problem, up to three days for the others.

Honest caveats: days per problem (humans get 2×4.5 h); statements manually formalised by humans. Peer-reviewed: Nature, Nov 2025.

IMO 2025: formal gold — and the fine print

• Aristotle (Harmonic): gold-level — P1–P5 with Lean-verified proofs (35/42); announced after honouring IMO's embargo. P6 unsolved by every AI system.

• Seed-Prover (ByteDance): official, IMO-confirmed 30/42 = silver within its 3-day window; lemma-style whole-proof generation.

• Informal golds, both 35/42: Gemini Deep Think (within the 4.5 h limit, graded by IMO coordinators) and an OpenAI experimental model (self-graded, not IMO-certified).

• Why formal matters — and the fine print: formalised inputs, extended compute windows, undocumented handling of "determine the answer" parts. Trust the proofs, interrogate the conditions.

IMO 2026 is July 15–16 in Shanghai — right around this tutorial. Expect fresh results.

Beyond competitions: AI discovers new mathematics

The unit-distance problem falls (May 20, 2026): an internal OpenAI reasoning model produced an original construction disproving Erdős's ~80-year-old planar unit-distance conjecture — point sets with n^{1+\delta} unit distances.

• The construction imports class field towers and Golod–Shafarevich — a genuinely different corner of mathematics; within days, Will Sawin refined it to an explicit exponent \delta \approx 0.014.

The Lean follow-up — verification catching up to discovery:

• Aleph Prover: a 33,087-line Lean 4 formalisation 8 days after the announcement — modulo two classical results taken as trusted assumptions.

• Parallel community + AI effort on the Lean Zulip: a fully-from-the-axioms formalisation, still in progress as of late June.

An AI system found the mathematics; formal proof is how we trust it at this speed.

Beyond competitions: research mathematics at scale

• Sphere packing in dimensions 8 & 24 (Math Inc., Dec 2025): the autoformalisation agent Gauss, with the existing project team, finished the Lean formalisation of Viazovska's Fields-Medal proofs — dim 8 in 5 days, dim 24 in ~2 more weeks. The human team had estimated ~6 months for dim 8 alone.

• De Giorgi–Nash–Moser theory (Armstrong & Kempe, Apr 2026): a central chapter of modern PDE regularity theory — ~56,000 lines of Lean in about two weeks, with LLM agents writing all the Lean ("no human hand touched the Lean files").

• Quantitative stochastic homogenisation (Armstrong & Kuusi, Jun 2026): the same workflow applied to their own current research paper — formalisation keeping pace with the research frontier.

Honest framing: the mathematics + proof architecture came from humans; AI removed the formalisation cost barrier (months → days).

Beyond mathematics: AI-authored verified software

The same recipe is spilling into program verification — proving code correct.

• lean-zip (Kim Morrison, 2026) — a fully verified DEFLATE / gzip / ZIP codec in Lean 4, with inflate (deflate data) = ok data proved for every input: ~32,000 lines, 1,100+ theorems, zero sorrys.

  • The kicker: implementation and proofs written almost entirely by loosely-supervised AI agents working from a plan document — long-horizon agentic formalisation, not a single prover call.

  • And it's practical: 2–3× faster than OCaml's decompress, within ~2× of zlib.

• A field organising around this: Software Verification in Lean 2026 (INRIA Paris, Apr 2026) — Lean automation (de Moura), verified SymCrypt, post-quantum crypto & TLS 1.3, specification quality.

One proving engine, two frontiers: research mathematics and trustworthy real-world software — advancing together.

What made this possible?

Three ingredients, mapping back to the core loop:

1. Verified reward at scale — Lean as an RL environment; no reward hacking on the final answer.

2. Autoformalisation closing the data gap — AlphaProof's ~1M informal → ~80–100M formal curriculum; Lean Workbook's 57k contest problems; Herald's 580k statement pairs.

3. Test-time compute — search, variants, lemma trees, days of thinking.

Let's open the hood and organise the design space.

§3 · The design space

† Aristotle: per its paper, a tactic-level prover (MCGS + expert iteration) inside an agentic informal-lemma loop; it now clearly works with repositories, but that part is not in the paper.

Approach 1: stepwise RL + search

{
"proof_label": "unidmrn",
"goal": "[[ ]] |- U. U. ‘’ A
    = ( dom A u. ran A )",
"proof_step": "[[ |- A = B |- C = B ]]
    |- A = C \\
{{ A : U. U. ‘’ A }} \\
{{ B : ( ran ‘’ A u. dom ‘’ A ) }} \\
{{ C : ( dom A u. ran A ) }}",
"proof_step_hash": "37yZVNorgF8=",
"parent_hash": ["n4Kl7judEN4="]
}

Approach 1 in action: HTPS and AlphaProof

HTPS — MCTS over proof hypertrees: selection / expansion / back-propagation.

AlphaProof — the AlphaZero recipe at scale: autoformalised curriculum + search.

Approach 2: whole-proof generation with LRMs

The paradigm: treat the entire proof as a sequence — sample complete proofs, check with Lean, resample or repair on failure. Chain-of-thought / LRM reasoning made this viable: informal sketch interleaved with formal output.

The 2025 default: RL fine-tuning of reasoning models to emit complete Lean proofs.

• Kimina-Prover: 80.7% miniF2F preview → 92.2% with test-time search.

• DeepSeek-Prover-V2 (671B): 88.9%; subgoal decomposition.

• Goedel-Prover-V2: 90.4% with self-correction at only 32B — an 8B variant matches the 671B DeepSeek.

Key tricks: informal CoT before the formal proof; subgoal decomposition; sample-and-repair / self-correction loops.

Approach 2 in action: Kimina-Prover

Style comparison: step vs. whole-proof, same theorem

IMO 1962 P2 — "find all x with √(3−x) − √(x+1) > 1/2" (answer: −1 ≤ x < 1 − √31/8):

theorem imo_1962_p2 (x : ℝ) (h₀ : 0 ≤ 3 - x) (h₁ : 0 ≤ x + 1)
    (h₂ : 1 / 2 < Real.sqrt (3 - x) - Real.sqrt (x + 1)) :
    -1 ≤ x ∧ x < 1 - Real.sqrt 31 / 8 := by
  constructor
  linarith
  rw [← sub_pos]
  field_simp [Real.sqrt_lt] at h₂ ⊢
  apply lt_of_le_of_lt
  rw [mul_comm]
  rw [sub_eq_add_neg]
  apply lt_of_le_of_lt
  rw [← lt_sub_iff_add_lt]
  ring_nf
  rw [← lt_sub_iff_add_lt]
  linarith [Real.sq_sqrt (by linarith : 0 ≤ 1 + x)]
  rw [Real.sqrt_lt (by norm_num)]
  rw [Real.sqrt_lt] <;> nlinarith
  norm_num at this

Approach 3: growing & reusing lemmas

Cost honesty: the test-time / self-play end is the most expensive corner of the design space.

Approach 3 in action: lemma pools & skill libraries

Approach 4: training-free & agentic proving

As base LLMs got stronger, "no fine-tuning" became competitive:

• Delta Prover: decomposition + iterative reflection — 95.9% miniF2F with an off-the-shelf model.

• Hilbert (Apple): recursive informal-reasoning + formal-proof construction — 70% PutnamBench (SOTA at release, Sep 2025; since surpassed).

• Agentic scaffolds: Numina-Lean-Agent (Claude Code + Lean MCP), Aristotle-as-product, general LLM + Lean REPL tool use.

Discussion point: will scaffolds keep beating bespoke fine-tuning as frontier models improve? — the "bitter lesson at test time" question.

Approach 4 in action: Hilbert and Numina-Lean-Agent

Hilbert — recursive decomposition: prover ↛ shallow solve ↛ subgoal decomposition, recurse.

Numina-Lean-Agent — a coding agent + Lean MCP tools: kernel feedback, retrieval, informal proving, discussion.

Benchmarks: competition math is saturated

• miniF2F (488 problems) saturated: 99.6%. PutnamBench (672 problems): 50% → 99.4% in under a year.

• The frontier has moved to research-level problems, where numbers collapse:

  • FATE (research-level algebra): at release, best system 3% on FATE-H, 0% on FATE-X — while informal reasoning on the same problems scores 71%/33%. Formalisation, not reasoning, is the bottleneck.

  • Formal Conjectures (DeepMind): 2,615 statements incl. 1,029 open conjectures — contamination-free by construction.

Benchmarks: program verification in Lean

A fast-growing benchmark family where the theorem is "this program meets its spec":

• Verified code generation — model writes implementation + spec + proof:

  • CLEVER (161, HumanEval-derived): anti-shortcut curation — no test-case supervision or LLM-written specs; generated specs must be proved equivalent to hidden ground truth.

  • Verina (189): end-to-end from natural language — code, spec, and proof, each graded separately.

  • VeriSoftBench (≈500): repository-scale — whole verified Lean repos with dependencies, not isolated functions.

  • FVAPPS (4,715): the largest — competitive-programming tasks with auto-generated specs as sorry theorems.

• Proving verification conditions from deployed code:

  • NTP4VC (600 VCs, from 7.5k+ candidates): real kernel code (Linux, Contiki) through Why3/Frama-C, rendered in Lean, Isabelle, and Rocq.

Constructions differ widely — spec provenance, scale, granularity — so read the construction before the leaderboard.

Where we stand

† Aristotle: per its paper, a tactic-level prover (MCGS + expert iteration) inside an agentic informal-lemma loop; it now clearly works with repositories, but that part is not in the paper.

• The trend: tactic-level → repository-level. Academia mostly explores repo-level scaffolds; industry may attempt repo-level training.

• Tactic/whole-proof training is still worth exploring: proving with extremely small models (Pythagoras-4B beats the 671B DeepSeek), advanced tactic usage (e.g. grind), canonical proof formats.

§4 · Coping with a flood of machine proofs

AI can now generate verified formal proofs by the thousand.

The frontier question is no longer "can a machine prove it?" but what humans still have to do:

• Can we trust the proofs? (reward hacking)

• Who supplies the definitions?

• Can we read & maintain what the machine emits?

Limitation 1: can we trust the flood?

The reward is "the kernel accepts" — but an agent optimising hard finds cracks:

• Gaming the harness, not the kernel — DeepSeek-Prover-V2: apply? inserts a "synthetic sorry" whose warning gets suppressed by an unrelated error — a pipeline that only checks "no errors, no sorry" accepts a bogus proof (analysis: Thomas Zhu).

• Extending the trusted base — native_decide pulls the Lean compiler + C++ runtime into the TCB; a past kernel soundness gap (since patched) failed to flag it. #print axioms is the audit.

A "perfect verifier" is only as trustworthy as the harness around it — and an RL objective will find every gap.

How humans cope: #print axioms audits; Comparator & SafeVerify — sandboxed re-checking against a trusted statement file; independent kernel implementations, raced on lean-kernel-arena.

Limitation 2: definitions & problem formulation

The prover proves the statement you write, not the one you mean — and Lean's totality conventions ("junk values": x / 0 = 0, Real.sqrt (-1) = 0) make it easy to state something else entirely, then cheerfully verify it.

The Riemann Hypothesis: Loeffler & Stoll's formal RH read "if s is not a negative even integer and ζ(s) = 0 then Re(s) = 1/2." Buzzard & Ellenberg asked: what about s = 1, ζ's pole? Totality hands riemannZeta 1 a junk value — had it been 0, the statement would be trivially false, and not RH. By luck it is ½(γ − log 4π) ≈ −0.98 — now certified by riemannZeta_one_ne_zero. Whether the statement was RH hinged on an unexamined junk value.

Everyday version: ∀ n m : ℕ, (n - m) + m = n silently drops n ≥ m (truncated subtraction) — and vacuous misformalisations: contradictory hypotheses prove anything.

Mathematics is largely about choosing definitions & abstractions — which current systems essentially can't. A machine-checked ✓ certifies the proof — never that you asked the right question.

Near future 1: the data flywheel & broader domains

• Data augmentation for LLM training: verified synthetic proofs as high-quality reasoning data — formal math as a training ground that improves general reasoning (the reverse direction: TP for ML).

• Large-scale autoformalisation: formalising the mathematical literature (textbooks → papers), enabling search & verification over mathematics as a corpus.

• Formal-driven discovery: proof search as a discovery instrument, not just a checker — DeepMind agents (LLM + Lean feedback + AlphaProof) closed 9 open Erdős problems and 44 OEIS conjectures.

Near future 2: verified programs & verified ML

Two directions to watch:

• Verified programs — e.g. WybeCoder (Meta): prove-as-you-generate — code, invariants, and proofs co-evolve during generation.

• Verified ML — e.g. TorchLean (LeanDojo group): neural networks as first-class Lean objects, with one semantics for execution and proof.

Full-circle vision: ML theory proved in Lean (Part I) + AI proving assistance (Part II) ⇒ trustworthy-by-construction ML papers and systems.

The bottleneck is shifting from "can we prove it" to "what should we prove".

Demo: three tools, same problem

All demo material: github.com/Wenda302/ICML26_demo

1. Claude + lake build — a general coding agent proving inside a Lean repo.

2. Leanstral 1.5 (Mistral, open weights) — an agentic open prover.

3. Aristotle (commercial) — natural-language problem → verified Lean proof.

(Numina-Lean-Agent is just as viable — no time to demo it today.)

Practical guidance: which tool when

• Claude / Codex + lake build — the generic, easiest entry: no scaffold at all, works in any Lean repo; you pay for the model.

• Leanstral 1.5 — open-weight model + open-source generic harness (vibe), high-quality proofs; free right now.

• Aristotle — closed-source but very easy to use and very strong on hard problems; appears optimised against a fixed Lean version.

• Numina-Lean-Agent — open-source harness optimised for hard problems; bring your own agentic LLM (Claude, DeepSeek Pro 4) and expect customisation effort.

Summary of Part II

1. Theorem proving = a game with a perfect verifier — ideal for RL + search.

2. 2024–26: IMO silver → gold → Putnam 12/12 → new mathematics: an Erdős conjecture disproved, open problems closed by formal proof search, and research-scale formalisations in days instead of months.

3. Design space: stepwise / whole-proof / repository-level × trained / training-free; benchmarks moving from puzzles to research & engineering.

4. The open gaps are human-facing: trust, definitions & formulation, maintainable proofs — likely not solved by scale alone.

5. You can use these tools on your own ML theory today.

Resources & Q&A

All materials will be available from the tutorial website:

leanmachinelearning.org/icml-tutorial/

Thank you — questions?