29.3 Formal Mathematical Reasoning

"The type checker rejected my proof at step 47. It turns out 'obviously true' is not a valid tactic in Lean 4. I have filed a feature request."

A Proof Assistant With No Patience for Hand-Waving

1. Why Formal Verification Matters for Science

Episodes like the following illustrate the stakes. In one well-documented case, a team of physicists announced a proof connecting two pillars of quantum field theory. Eighty-six pages of dense algebra survived peer review at a top journal. Years later, a graduate student found a sign error: a minus where a plus belonged. That single character invalidated the central result and every downstream experiment that relied on it. The history of science is littered with such episodes: a boundary condition on the wrong domain, an integral over the wrong limits, a tensor contraction that "obviously" commutes until it does not. Peer review catches many such errors, but it is a statistical filter, not a guarantee.

Formal verification uses a software tool (a proof assistant) to confirm mechanically that every logical step in a derivation follows from the axioms and previously proven results. It leaves zero room for human error or ambiguity. It replaces social trust (peer review, reputation, "this looks right") with a mathematical guarantee: a checked proof is either correct, or the checker itself has a bug. Modern checkers have trusted kernels (the minimal core code that all verification reduces to) small enough to audit exhaustively. The mechanism is type checking: each proof step must produce a term whose type matches the goal type, and the kernel rejects any term that does not fit. Use formal verification instead of informal argument whenever the cost of an undetected error is high (drug design, safety-critical systems, novel theoretical claims) and the reasoning fits a supported logic. Use informal reasoning for exploratory work, rough estimates, or domains where formalization infrastructure does not yet exist.

From Statistical Filters to Constructive Guarantees

When a pharmaceutical company submits a new drug whose safety proof rests on a 200-step statistical derivation, a single algebraic slip can mean years of wasted trials and, worse, patient harm. Formal verification exists precisely to make such slips structurally impossible.

Formal verification offers a different contract: if a derivation type-checks, every step follows logically from the axioms. The Lean 4 proof assistant implements a constructive type theory (the Calculus of Inductive Constructions, where "constructive" means every proof of existence must exhibit an explicit witness rather than merely ruling out non-existence) that has been formally verified down to a small trusted kernel of approximately 6,000 lines of C. That tiny kernel is the sole root of trust for Mathlib's 170,000+ verified declarations, meaning every theorem in analysis, algebra, and topology ultimately reduces to fewer lines of code than a single web-page stylesheet. Everything built on top of this kernel, from natural number arithmetic to abstract algebra to measure theory, is verified by reduction to the kernel.

The practical relevance for discovery AI is that formal verification provides a perfect reward signal for reinforcement learning. In Section 29.2, we approximated process rewards through Monte Carlo rollouts, an expensive and noisy estimate. Lean 4 gives an exact, instant, binary signal: does this proof step type-check? This perfect signal is what makes systems like AlphaProof possible. In short: a proof assistant turns "I believe this derivation is correct" into "this derivation is correct, and the machine checked every step."

2. Lean 4: A Crash Course

Lean 4 is both a programming language and a proof assistant. In Lean, a theorem is a type, and a proof is a value of that type. Proving a theorem is literally writing a program that has the theorem as its type. This is the Curry-Howard correspondence: proofs are programs, propositions are types.

Here is a minimal example. We prove that for any natural number \(n\), \(n + 0 = n\):

-- Lean 4: a simple proof by induction
theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl           -- base case: 0 + 0 = 0 is true by definition
  | succ k ih =>          -- inductive case: assume k + 0 = k
    simp [Nat.add_succ]   -- simplify using the definition of addition
    exact ih              -- apply the induction hypothesis

The key concepts for our purposes are:

• Tactics: commands that transform proof goals. Common tactics include rfl (prove by reflexivity), simp (simplification), ring (ring arithmetic), linarith (linear arithmetic), omega (Presburger arithmetic, where the decision procedure handles integer formulas with addition and ordering but not multiplication) , and norm_num (numerical normalization).
• Mathlib: a community-maintained library of over 170,000 formalized declarations (circa 2024) covering analysis, algebra, topology, number theory, and combinatorics. Mathlib provides the building blocks that LLM-based provers reference.
• Goals and hypotheses: at each point in a proof, Lean maintains a goal (what remains to be proved) and a set of hypotheses (what is known). Tactics transform goals and hypotheses until no goals remain.

For scientific applications, the most relevant Lean capabilities are formalized real analysis (for continuous optimization, differential equations), linear algebra (for matrix derivations), and measure theory (for probability arguments). The connection to the knowledge representation formalisms in Chapter 3 is direct: Lean's type system is a strictly more expressive knowledge representation than the description logics and first-order theories discussed there.

Running Lean from Python

To integrate Lean verification into a Python-based discovery pipeline, we interact with Lean through a subprocess. The following utility sends Lean code to the Lean server and checks whether it type-checks:

import subprocess
import tempfile
import os
from pathlib import Path
from dataclasses import dataclass

@dataclass
class LeanResult:
    """Result of checking a Lean 4 proof."""
    success: bool
    errors: list[str]
    warnings: list[str]
    lean_code: str

def check_lean_proof(
    lean_code: str,
    lean_path: str = "lean",  # path to lean executable
    timeout: int = 60
) -> LeanResult:
    """Submit Lean 4 code to the type checker and return the result.

    Args:
        lean_code: Lean 4 source code to check
        lean_path: Path to the lean executable
        timeout: Maximum seconds to wait for verification

    Returns:
        LeanResult with success status and any errors/warnings
    """
    # Write code to a temporary file
    with tempfile.NamedTemporaryFile(
        mode='w', suffix='.lean', delete=False
    ) as f:
        # Add minimal imports
        full_code = "import Mathlib.Tactic\n\n" + lean_code
        f.write(full_code)
        tmp_path = f.name

    try:
        result = subprocess.run(
            [lean_path, tmp_path],
            capture_output=True,
            text=True,
            timeout=timeout
        )

        errors = []
        warnings = []
        for line in result.stderr.split('\n'):
            if 'error' in line.lower():
                errors.append(line.strip())
            elif 'warning' in line.lower():
                warnings.append(line.strip())

        return LeanResult(
            success=len(errors) == 0,
            errors=errors,
            warnings=warnings,
            lean_code=lean_code
        )
    except subprocess.TimeoutExpired:
        return LeanResult(
            success=False,
            errors=[f"Lean timed out after {timeout}s"],
            warnings=[],
            lean_code=lean_code
        )
    finally:
        os.unlink(tmp_path)

# Example: verify a simple theorem
result = check_lean_proof("""
theorem square_nonneg (x : Real) : x ^ 2 >= 0 := by
  exact sq_nonneg x
""")
print(f"Proof valid: {result.success}")
if result.errors:
    print(f"Errors: {result.errors}")

3. DeepSeek-Prover: LLMs That Generate Lean Proofs

DeepSeek-Prover (Xin et al., 2024) demonstrates that language models can be trained to generate Lean 4 proofs directly. The approach uses a bootstrapping strategy:

1. Seed data: start with a small corpus of human-written Lean proofs from Mathlib.
2. Synthetic generation: use a language model to generate new theorem statements and proof attempts.
3. Verification filter: keep only the (statement, proof) pairs where Lean's type checker confirms the proof.
4. Fine-tuning: train the language model on the verified pairs, then repeat from step 2.

This loop mirrors AlphaZero's self-play: the model generates its own training data, and the formal verifier acts as judge. Each iteration yields a stronger prover that produces harder verified proofs, fueling the next iteration.

On the miniF2F benchmark (a collection of 488 competition-level math problems formalized in multiple proof assistants, used as the standard evaluation suite for automated theorem provers), DeepSeek-Prover-V1.5 solves approximately 60% of problems, compared to ~30% for earlier LLM-based provers. The key innovation is the integration of Monte Carlo Tree Search (MCTS)-style proof search: rather than generating a complete proof in one pass, the model generates one tactic at a time, checks it with Lean, and uses the result to guide the next tactic choice. (As of 2025, DeepSeek-Prover-V2 further improved on these results by combining chain-of-thought reasoning with formal proof generation, surpassing 80% on miniF2F and closing many previously open Lean formalization challenges.)

import anthropic

client = anthropic.Anthropic()

def autoformalize_and_prove(
    informal_statement: str,
    max_attempts: int = 5
) -> dict:
    """Translate an informal mathematical statement to Lean 4 and attempt a proof.

    Pipeline:
    1. Autoformalize: translate natural language to a Lean theorem statement
    2. Proof search: generate candidate proofs
    3. Verify: check each candidate with the Lean type checker

    Args:
        informal_statement: A mathematical claim in natural language
        max_attempts: Maximum proof attempts per formalization

    Returns:
        Dict with formalization, proof (if found), and verification status
    """
    # Step 1: Autoformalize
    formalize_response = client.messages.create(
        model="claude-sonnet-4-20250514",
        max_tokens=512,
        temperature=0.0,
        messages=[{
            "role": "user",
            "content": f"""Translate the following mathematical statement into a Lean 4
theorem declaration. Use Mathlib conventions and imports.
Output ONLY the Lean 4 code, no explanation.

Statement: {informal_statement}"""
        }]
    )
    lean_statement = formalize_response.content[0].text.strip()

    # Clean up: extract just the theorem line if wrapped in markdown
    if "```" in lean_statement:
        lines = lean_statement.split("```")
        for block in lines:
            if "theorem" in block:
                lean_statement = block.replace("lean", "").strip()
                break

    # Step 2: Generate proof candidates
    proofs_tried = []
    for attempt in range(max_attempts):
        proof_response = client.messages.create(
            model="claude-sonnet-4-20250514",
            max_tokens=1024,
            temperature=0.6 + 0.1 * attempt,  # increase diversity
            messages=[{
                "role": "user",
                "content": f"""Complete this Lean 4 proof. Use standard Mathlib tactics.
Output ONLY the complete theorem with proof, no explanation.

{lean_statement} := by
  sorry  -- replace this with actual proof tactics"""
            }]
        )
        candidate = proof_response.content[0].text.strip()
        if "```" in candidate:
            lines = candidate.split("```")
            for block in lines:
                if "theorem" in block or "by" in block:
                    candidate = block.replace("lean", "").strip()
                    break

        proofs_tried.append(candidate)

        # Step 3: Verify with Lean
        result = check_lean_proof(candidate)
        if result.success:
            return {
                "informal": informal_statement,
                "lean_statement": lean_statement,
                "proof": candidate,
                "verified": True,
                "attempts": attempt + 1
            }

    return {
        "informal": informal_statement,
        "lean_statement": lean_statement,
        "proof": None,
        "verified": False,
        "attempts": max_attempts,
        "candidates": proofs_tried
    }

# Example: formalize and prove a simple statement
result = autoformalize_and_prove(
    "For all natural numbers n, if n is even then n squared is even."
)
print(f"Statement: {result['informal']}")
print(f"Formalized: {result['lean_statement']}")
print(f"Verified: {result['verified']}")
if result['proof']:
    print(f"Proof (found in {result['attempts']} attempts):")
    print(result['proof'])

4. FunSearch: Discovering Functions with LLMs

While DeepSeek-Prover uses LLMs to prove existing theorems, FunSearch (Romera-Paredes et al., 2024) uses LLMs to discover new mathematical objects. The key insight is that many mathematical discovery problems can be framed as program search: find a function (program) that satisfies a given property, as verified by an automated evaluator.

FunSearch made headlines by discovering new constructions for the cap set problem (finding the largest subset of points in a finite geometry such that no three points are collinear, a central question in additive combinatorics), finding sets larger than any previously known by human mathematicians. The architecture is deceptively simple:

1. Specification: define an evaluate function that scores candidate programs (higher is better).
2. Population: maintain a population of programs, initially seeded with simple baselines.
3. Evolution: prompt an LLM with the best programs from the population and ask it to generate an improved version.
4. Selection: evaluate each candidate; keep those that score higher than their parents.

The evaluator provides the correctness guarantee: unlike informal reasoning, the evaluator's verdict is exact. If a candidate program achieves a higher score, that improvement is real, not a hallucination.

import anthropic
import random
from dataclasses import dataclass

client = anthropic.Anthropic()

@dataclass
class Program:
    """A candidate program in the FunSearch population."""
    code: str
    score: float
    generation: int

def funsearch(
    task_description: str,
    evaluate_fn: callable,  # function(code_str) -> float
    seed_programs: list[str],
    n_generations: int = 10,
    population_size: int = 10,
    children_per_gen: int = 5
) -> Program:
    """Simplified FunSearch: evolve programs using an LLM and an evaluator.

    Args:
        task_description: Natural-language description of what the function should do
        evaluate_fn: Scoring function that takes program code and returns a score
        seed_programs: Initial population of programs
        n_generations: Number of evolutionary generations
        population_size: Maximum population size (best are retained)
        children_per_gen: Number of new candidates per generation

    Returns:
        The highest-scoring Program found
    """
    # Initialize population
    population = []
    for code in seed_programs:
        try:
            score = evaluate_fn(code)
        except Exception:
            score = 0.0
        population.append(Program(code=code, score=score, generation=0))

    for gen in range(1, n_generations + 1):
        # Select top programs as parents
        population.sort(key=lambda p: p.score, reverse=True)
        parents = population[:3]

        parent_code = "\n\n---\n\n".join(
            f"# Score: {p.score:.4f}\n{p.code}" for p in parents
        )

        # Generate children via LLM
        for _ in range(children_per_gen):
            response = client.messages.create(
                model="claude-sonnet-4-20250514",
                max_tokens=1024,
                temperature=0.9,
                messages=[{
                    "role": "user",
                    "content": f"""Task: {task_description}

Here are the best programs found so far, with their scores:

{parent_code}

Generate an IMPROVED version of the function. Try a different strategy.
Output ONLY the Python function, no explanation."""
                }]
            )

            child_code = response.content[0].text.strip()
            # Strip markdown fences if present
            if "```" in child_code:
                lines = child_code.split('\n')
                child_code = '\n'.join(
                    l for l in lines
                    if not l.strip().startswith('```')
                )

            try:
                score = evaluate_fn(child_code)
            except Exception:
                score = 0.0

            population.append(Program(
                code=child_code, score=score, generation=gen
            ))

        # Prune to population size
        population.sort(key=lambda p: p.score, reverse=True)
        population = population[:population_size]

        best = population[0]
        print(f"Generation {gen}: best score = {best.score:.4f}")

    return population[0]

# Example: discover a function that packs numbers into bins efficiently
def evaluate_packing(code: str) -> float:
    """Evaluate a bin-packing heuristic on a test instance."""
    namespace = {}
    exec(code, namespace)
    if 'pack' not in namespace:
        return 0.0

    # Test instance: pack items of sizes [0.7, 0.3, 0.5, 0.4, 0.2, 0.8, 0.1, 0.6]
    # into unit-capacity bins, minimizing bin count
    items = [0.7, 0.3, 0.5, 0.4, 0.2, 0.8, 0.1, 0.6]
    try:
        bins = namespace['pack'](items)
        # Verify: each bin sum must be <= 1.0
        if not all(sum(b) <= 1.0 + 1e-9 for b in bins):
            return 0.0
        # Score: fewer bins is better; also reward tighter packing
        n_bins = len(bins)
        utilization = sum(sum(b) for b in bins) / n_bins if n_bins > 0 else 0
        return 10.0 / n_bins + utilization  # lower bin count dominates
    except Exception:
        return 0.0

seed = ["""def pack(items):
    bins = []
    for item in sorted(items, reverse=True):
        placed = False
        for b in bins:
            if sum(b) + item <= 1.0:
                b.append(item)
                placed = True
                break
        if not placed:
            bins.append([item])
    return bins"""]

# best = funsearch(
#     "Write a Python function pack(items) that packs float items into "
#     "unit-capacity bins, minimizing the number of bins used.",
#     evaluate_packing,
#     seed,
#     n_generations=5
# )

5. AlphaGeometry 2 and AlphaProof at IMO 2024

FunSearch demonstrates that LLMs paired with exact evaluators discover novel mathematical objects. The natural extension applies the same pairing to problems demanding multi-step formal proofs rather than single-function optimization.

In July 2024, DeepMind demonstrated two systems at the International Mathematical Olympiad that represent the state of the art in AI mathematical reasoning:

AlphaGeometry 2 extends the original AlphaGeometry (Trinh et al., 2024) with a Gemini-based language model and an expanded symbolic deduction engine. The original AlphaGeometry solved 25 of 30 historical IMO geometry problems; AlphaGeometry 2 solves the geometry problems from the 2024 competition. The architecture pairs a neural language model (which proposes auxiliary constructions: "draw line through point A parallel to BC") with a symbolic deduction engine (which derives consequences using standard geometric theorems). The neural component handles the creative, abductive step; the symbolic component handles the deductive verification.

AlphaProof tackles algebra and number theory, the IMO problem types that require multi-step algebraic manipulation and clever inequality arguments. AlphaProof's architecture combines:

• A Gemini model fine-tuned to generate Lean 4 proof tactics
• Lean 4 as a verification backend (providing the perfect reward signal)
• MCTS-style search over proof states, guided by a learned value function
• Reinforcement learning from verified proofs (unlike AlphaZero's self-play where two agents compete, here the "opponent" is the Lean type checker: the model proposes proof steps and the checker either accepts or rejects them, providing the training signal)

Together, AlphaProof and AlphaGeometry 2 solved 4 of 6 problems at IMO 2024, scoring 28 out of 42 points, equivalent to a silver medal. This is the first time an AI system has achieved medal-level performance at the IMO. The two problems it did not solve (Problems 3 and 5) are combinatorics problems, a domain where current formal verification infrastructure is less developed.

6. The Autoformalization Pipeline

Competition results mark the frontier, but most scientific teams need a practical workflow for their own derivations.

The practical workflow for connecting LLM reasoning to formal verification follows a three-stage pipeline, illustrated in Figure 29.3:

1. Informal reasoning: the LLM solves the problem using chain-of-thought, producing a natural-language derivation with mathematical notation.
2. Autoformalization: a second LLM call translates the informal derivation into a Lean 4 proof sketch, with sorry placeholders for steps that are hard to formalize.
3. Proof completion: a prover (LLM-based or tactic-based) fills in the sorry gaps. Each completed gap is verified by Lean's type checker.

The resulting proof has a partial verification status: some steps are formally verified, others remain as sorry placeholders that represent trusted but unverified claims. This partial verification is still valuable: it localizes the burden of trust to specific steps, rather than requiring trust in the entire derivation. Figure 29.3.1 illustrates autoformalization pipeline from informal reasoning through Lean 4 verification.

@dataclass
class VerificationReport:
    """Report from the autoformalization pipeline."""
    informal_solution: str
    lean_sketch: str
    verified_steps: list[str]
    unverified_steps: list[str]  # steps that remain as 'sorry'
    fully_verified: bool
    confidence: float  # fraction of steps verified

def autoformalization_pipeline(
    client: anthropic.Anthropic,
    problem: str,
    domain: str = "real analysis"
) -> VerificationReport:
    """Three-stage autoformalization pipeline.

    Stage 1: Solve informally with CoT
    Stage 2: Translate to Lean 4 sketch
    Stage 3: Attempt to fill sorry gaps
    """
    # Stage 1: Informal solution
    informal_response = client.messages.create(
        model="claude-sonnet-4-20250514",
        max_tokens=2048,
        thinking={"type": "enabled", "budget_tokens": 8000},
        messages=[{
            "role": "user",
            "content": f"Solve this {domain} problem step by step, "
                       f"showing all mathematical details:\n{problem}"
        }]
    )
    informal = ""
    for block in informal_response.content:
        if block.type == "text":
            informal = block.text

    # Stage 2: Autoformalize to Lean sketch
    lean_response = client.messages.create(
        model="claude-sonnet-4-20250514",
        max_tokens=2048,
        messages=[{
            "role": "user",
            "content": f"""Translate this mathematical solution into a Lean 4 proof.
Use Mathlib tactics. Where a step is difficult to formalize, use 'sorry'.
Output ONLY the Lean 4 code.

Solution:
{informal}"""
        }]
    )
    lean_sketch = lean_response.content[0].text.strip()
    if "```" in lean_sketch:
        parts = lean_sketch.split("```")
        for part in parts:
            if "theorem" in part or "lemma" in part:
                lean_sketch = part.replace("lean", "").strip()
                break

    # Stage 3: Count and attempt to fill sorry gaps
    sorry_count = lean_sketch.count("sorry")
    verified_steps = []
    unverified_steps = []

    if sorry_count == 0:
        # No sorries: check the entire proof
        result = check_lean_proof(lean_sketch)
        if result.success:
            verified_steps = ["entire proof"]
        else:
            unverified_steps = ["entire proof (type check failed)"]
    else:
        # Try to fill each sorry one at a time
        sorry_positions = []
        lines = lean_sketch.split('\n')
        for i, line in enumerate(lines):
            if 'sorry' in line:
                sorry_positions.append(i)
                unverified_steps.append(f"line {i+1}: {line.strip()}")

        # Attempt to replace each sorry with a proof
        for pos in sorry_positions:
            context_before = '\n'.join(lines[max(0, pos-5):pos])
            context_after = '\n'.join(lines[pos+1:min(len(lines), pos+3)])

            fill_response = client.messages.create(
                model="claude-sonnet-4-20250514",
                max_tokens=256,
                temperature=0.3,
                messages=[{
                    "role": "user",
                    "content": f"""Replace 'sorry' with actual Lean 4 tactics.
Context before:
{context_before}

Line to replace: {lines[pos]}

Context after:
{context_after}

Output ONLY the replacement tactic(s), one per line."""
                }]
            )

            replacement = fill_response.content[0].text.strip()
            test_code = lean_sketch.replace(
                lines[pos], replacement, 1
            )

            result = check_lean_proof(test_code)
            if result.success:
                lean_sketch = test_code
                verified_steps.append(f"line {pos+1}: {replacement}")
                # Remove from unverified
                unverified_steps = [
                    s for s in unverified_steps
                    if not s.startswith(f"line {pos+1}")
                ]

    total = len(verified_steps) + len(unverified_steps)
    confidence = len(verified_steps) / max(total, 1)

    return VerificationReport(
        informal_solution=informal,
        lean_sketch=lean_sketch,
        verified_steps=verified_steps,
        unverified_steps=unverified_steps,
        fully_verified=len(unverified_steps) == 0,
        confidence=confidence
    )

# Example usage
report = autoformalization_pipeline(
    client,
    "Prove that the arithmetic mean of two positive reals is at least "
    "their geometric mean (AM-GM inequality for n=2).",
    domain="real analysis"
)
print(f"Fully verified: {report.fully_verified}")
print(f"Confidence: {report.confidence:.0%}")
print(f"Verified steps: {report.verified_steps}")
print(f"Remaining sorry gaps: {report.unverified_steps}")

Exercises

1. (Conceptual) FunSearch uses LLMs to generate candidate programs and an evaluator to score them. Compare this to genetic programming (which uses random mutation and crossover instead of LLM generation). What advantages does the LLM provide over random search? What limitations does it inherit from its training distribution?
2. (Coding) Install Lean 4 (via elan, the Lean version manager) and Mathlib. Write a Lean proof of the statement: "For all natural numbers \(n \geq 1\), \(n^2 \geq n\)." Then modify the autoformalize_and_prove function to solve this problem automatically. How many attempts does the LLM need?
3. (Analysis) The combined AlphaProof and AlphaGeometry 2 system solved 4 of 6 IMO 2024 problems but failed on the two combinatorics problems. Research the specific problems it failed on (Problems 3 and 5). What makes combinatorics harder to formalize than algebra or geometry? Propose a research direction that might address this gap.