LLM-Assisted Formal Proofs: What They Can Do and Where They Stop

Formal proof means writing a mathematical argument as code that a proof assistant (Lean, Coq/Rocq, Isabelle) checks step by step. The assistant accepts only proofs that obey typing and logic rules, so the result can be independently verified.

Models are increasingly used to generate proof steps, and reports of “finishing a proof in tens of hours” often omit verifier version, task scope, and reproduction conditions. This article covers workflow, capability limits, and engineering practice: what models actually do in these tasks and what to watch for.

What is formal proof?

Mathematicians usually write proofs in natural language and rely on peer review. Formal proof encodes every step as machine-checkable commands. The assistant checks that each lemma holds and each inference follows the rules. After a successful check, correctness depends on the kernel and the chosen axioms; human review load drops.

The cost is labor. Formalizing a theorem often requires many supporting definitions and lemmas. Fermat’s Last Theorem was proved by Andrew Wiles in 1994 (paper in Annals of Mathematics, 1995) and depends on modularity of semistable elliptic curves. A Lean community FLT formalization led by Kevin Buzzard is still in progress; status should be taken from the official repository and announcements.

How models typically work in proofs

A common closed loop has three steps.

1. Decompose. Split the goal into sublemmas and record dependencies.
2. Guess. Generate proof code from trained mathematical knowledge and the assistant’s standard library.
3. Verify. Compile with the proof assistant. On failure, feed error messages back so the model revises tactics and retries.

The verifier is the final judge. Model output is not a reliable conclusion until it type-checks. Three caveats:

• Confirm the statement is right. A proof can check while wrong definitions prove something else (misformalization); humans must audit definitions.
• Check extra assumptions. In Lean, #print axioms lists axioms used. sorry means the proof is unfinished.
• Avoid eval contamination. If test problems or solutions were in training data, success rates do not reflect real ability.

Confirmed progress

In 2024, Google DeepMind published AlphaProof and AlphaGeometry 2, reaching silver-medal level on IMO problems, with some proofs in Lean. That is a checkable public result; see the original blog and papers for problem set, scoring, and baselines.

Many other reports lack comparable materials—no paper, code, or independent review. Treat those as leads, not decision inputs, until sources can be verified.

Common failure modes

• Lemma-name hallucination. Invented theorems or wrong argument order. The compiler errors, but retries waste time.
• Misformalized definitions. Natural-language concepts become inequivalent code; the proof passes but the meaning drifts.
• Lost context. Long proofs have many intermediate states; multi-turn edits forget earlier conventions.
• Useless retry loops. The model repeats the same error. Cap retries and hand off to a human.
• Over-reliance on automation. Teams that do not understand the proof structure cannot maintain or extend it.

What models can do in software migration

Legacy migration is hard because business meaning is incomplete in code, and rule-based transforms cover only fixed patterns.

Dimension	Rule-based transform	LLM semantic migration
Predictability	High; same input, same output	Lower; needs sampled review
Coverage of business meaning	Known patterns only	Some implicit logic
Call cost	Lower	Grows with code volume
Main risk	Misses nonstandard writing	Plausible but wrong code
Fit	Regular patterns, fixed language versions	Strong tests plus human review

In practice the two combine: rules for syntax and format, LLMs for semantics, tests and review as gates.

A workable flow: extract AST and dependencies with static analysis; let the model infer module intent; generate target-language code plus unit and integration tests; compare old vs. new outputs in a test environment and widen rollout gradually.

Preconditions: work on a dedicated version-control branch for rollback; migration tools read-only on production databases, write only in test; original system must have enough test coverage to judge behavioral equivalence.

Illustrative (not production) agent loop:

# Illustrative only, not production-ready
MAX_STEPS = 20
ALLOWED_TOOLS = {"search_docs", "run_tests"}   # whitelist; no undeclared tools
def agent_loop(task, env, audit_log):
    history = []
    for step in range(MAX_STEPS):
        obs = env.get_state()                      # read-only current state
        plan = llm.plan(task, history, obs, tools=ALLOWED_TOOLS)
        audit_log.write(step, plan)                # audit every step
        if plan.is_finished():
            return "done"
        if plan.is_destructive():                  # delete/deploy need human OK
            if not env.request_human_approval(plan):
                return "human rejected"
        try:
            result = env.execute(plan, timeout=30) # timeout, sandboxed
        except Exception as err:
            audit_log.write(step, f"exec failed: {err}")
            if step >= 3 and history[-3:] are all failures:
                return "consecutive failures, hand off"
            continue
        history.append((obs, plan, result))
    return "max steps, hand off"

Real systems still need auth, timeouts, and logging.

Designing the agent runtime

Agents call tools, so permissions matter more than for chatbots.

• Least privilege: only files, APIs, and tables required for the task.
• Isolated execution: containers or VMs, restricted egress.
• Tool whitelist; undeclared tools forbidden. Irreversible actions (delete, deploy, permission change) need human confirmation.
• Audit logs for every step: inputs, outputs, parameters, timestamps, with access control (logs may hold secrets).
• Retry caps and rollback. Model changes stay pending until review, then merge.

Protecting data in enterprise deployments

Watch data flow. Prompts and context sent to external models may include source, customer data, or internal docs.

• RBAC so each role gets only matching model capabilities and data sources.
• Filter inputs (keys, IDs, phones) and outputs (blocked content).
• Check vendor retention: whether prompts are used for training, log lifetime, data region—per contract and official docs.
• Full audit trail for later investigation.

Cloud platforms can supply network isolation, key management, and access audit. Choose a provider or self-hosted setup that meets your compliance needs.

Cost of “fast” modes

Some platforms offer faster generation via speculative decoding or quantization, usually at a higher unit price.

Useful when latency is user-visible: voice assistants, interactive coding, real-time control.

Poor fit for offline batch jobs, archival, or long cost-sensitive work with no human waiting.

Do not compare only price per million tokens. A better metric:

task cost ≈ cost per call × average calls + retry cost + human review cost

Track end-to-end latency, success rate, and retries together. Use the vendor’s current pricing page and your own measurements.

Summary

In formal proof, value comes from pairing candidate generation with machine verification. The verifier decides trust; the model speeds search. In migration and agents, the same idea applies: put model capability inside tests, permissions, and audit.

To judge a claim, ask: is there reproducible material, is verification described, and are failures and cost considered? Only then is further investment warranted.

Sources (verify latest versions before citing): Andrew Wiles, “Modular elliptic curves and Fermat’s Last Theorem,” Annals of Mathematics, 1995; Lean community Mathlib and FLT formalization repositories; Google DeepMind AlphaProof / AlphaGeometry 2 IMO 2024 materials; Lean 4 docs on #print axioms and sorry.