AlphaProof

A DeepMind AI system for formal mathematical proof, built on the lean-theorem-prover. Surfaced by lean-for-programmers (created as its own page during a lint pass — it was referenced repeatedly but had no page).

What we know (from the source)

• Uses Lean as its proof-checking substrate, and reached silver-medalist level at the International Mathematical Olympiad.
• Cited alongside LeanDojo, miniF2F, and ProofNet as evidence that Lean is the common backbone of recent AI-mathematics work.

Why it matters here

AlphaProof is the clearest concrete instance of the AI-agent ↔ formal-methods bridge the synthesis notes: an AI system mechanizing reasoning via a checkable formal language. It rhymes with the LLM-agent theme behind gbrain — an agent producing results that are verifiable, not merely plausible, which connects to the honesty/ no-unsupported-claims thread around claude-opus-4-8.

Superseded as the cluster’s high-water mark (2026-08-01)

ten-proofs does something AlphaProof did not: open problems chosen by their own communities, with the argument generated by the model rather than a proof of a supplied competition statement — and shipped as Lean certificates anyone can check. AlphaProof remains the better-documented system (a published paper, a named benchmark); ten-proofs is the larger claim on a model nobody outside OpenAI can run. Note the awkward pairing: llms-cant-jump cites AlphaProof as evidence the deduction arrow is being conquered while abduction stays out of reach, and ten-proofs pushes that arrow much further without settling the question.

Related

lean-theorem-prover · lean-for-programmers · ten-proofs · lean-certificate · llms-cant-jump

Sourced only from a passing mention in the Lean tutorial; no dedicated AlphaProof source ingested.