Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics¶

🕒 Published (v1): 2026-06-30 05:05 UTC · Source: Arxiv · link

Why this paper was selected

Agentic autoformalization pipeline with Lean 4 verification; novel harness for correctness guarantees

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

This paper presents a multi-agent agentic framework that automates the translation of research-level mathematics into machine-verified Lean 4 proofs. The system introduces a "type-first" paradigm with auxiliary-lemma validation and a recursive proof-decomposition pipeline, all orchestrated through Claude Code as the session manager. It achieves a 91.3% lower-bound accuracy on PutnamBench at ~$5/problem and successfully formalizes main theorems from five STOC 2025 papers.

Problem¶

LLMs generating mathematical proofs make subtle errors that are difficult for humans to detect at scale. Existing autoformalization approaches fail at research-level mathematics because: (1) single-agent setups saturate context windows with compilation errors; (2) fixed pipelines cannot backtrack when an upstream step fails; and (3) formal libraries like Mathlib lack coverage for many research domains, causing direct translation to fail for theorems that depend on undefined types.

Method¶

The orchestrator (a Claude Code session) manages two sequential pipelines:

Statement formalization pipeline: An Extractor identifies the main theorem; a Type Planner enumerates types missing from Mathlib; for each type (in dependency order), a Lemma Planner generates auxiliary lemmas to serve as unit tests, then $k$ Type Formalizer agents independently attempt to translate the type into Lean and prove the auxiliary lemmas. An Auctioneer applies best-of-$k$ selection scoring by: fraction of auxiliary lemmas proved, Faithfulness Judge semantic alignment, and code length. If no candidate passes, the orchestrator spawns additional formalizers until one does. A Theorem Formalizer finally translates the main statement, verified by the Faithfulness Judge via four independent checks (two blind via back-translation, two direct; each pair uses different models; discrepancies adjudicated by a final judge agent).

Proof formalization pipeline: Treats a proof as a recursive tree. At each node: a Natural Language Prover drafts an informal proof, internally revised in a loop with a Proof Critic (which emits concrete questions about logical gaps rather than a pass/fail verdict). A Proof Detailer expands the accepted proof into tactic-sized steps; a Lemma Breakdown agent decomposes these into topologically ordered sub-lemmas. The orchestrator scores each node (depth, statement length, quantifier nesting, source-paper cues) to decide leaf vs. recurse. Parent nodes are proved before their children using sorry stubs, ensuring child lemma statements are validated by their use before being proved. A Claim Check tool enforces that no attempt silently weakens a statement. Structured failure diagnostics route back to re-breakdown, child reformalization, or node promotion. Prior-work citations become explicitly labeled Lean axioms verified by the Faithfulness Judge; on benchmarks this path is disabled to keep proofs self-contained.

Key Contributions¶

Type-first formalization paradigm: defines domain-specific types missing from Mathlib before addressing the primary theorem, analogous to declaring data structures before algorithms.
Auxiliary lemma technique: validates type definitions by attempting to prove associated well-known properties, functioning as unit tests for formal mathematical vocabulary.
Dynamic orchestrator with backtracking: the Claude Code session can reorder stages, open feedback bridges between pipeline stages, and roll back to prior states on failure—overcoming rigidity of fixed pipelines.
Recursive proof-formalization pipeline: parent-before-child proving strategy with structured failure feedback and escalation budgets ensures termination while enabling fine-grained repair.
Cost-effective deployment: research-level theorem proving using only a standard $200 software subscription, averaging ~$5/problem, with no local GPUs required.
Discovery of a proof gap: the system identified a computer-verified gap in a published STOC proof during formalization.

Results¶

PutnamBench: 32 randomly sampled problems (seed=0, no internet access, no manual proof preparation), all 32 solved; statistical lower bound of 91.3% accuracy over the full benchmark at 95% confidence.
STOC 2025 papers: 5 papers formalized (combinatorics, communication complexity, mechanism design, learning theory); main theorem statements confirmed accurate by human expert review; all 5 proofs machine-checked by Lean compiler.
2 of 5 papers proved with no axioms beyond Lean's kernel (cited prior results reproved from scratch).
3 of 5 required explicit admission of well-known external theorems as axioms.
1 published STOC proof had a gap uncovered by the formalization process.
Cost: ~$5 per PutnamBench problem; backing models Claude Opus 4.7 (Putnam) and Claude Opus 4.8 (STOC).

Limitations¶

PutnamBench evaluation used only 32 of the full problem set; the 91.3% lower bound is statistical, not exhaustive.
Statement faithfulness cannot be mechanically verified—the Faithfulness Judge may miss semantic mismatches that human experts would catch.
Relies on the orchestrator's heuristic leaf-vs-recurse scoring; poor calibration could waste budget on trivial nodes or under-decompose complex ones.
Prior-work results admitted as axioms mean full kernel-level provability is not always achieved; human judgment determines what counts as "prior work."
Computational cost and latency scale with recursion depth and $k$ parallel formalizer attempts; no ablation on $k$ or budget sensitivity is reported in the excerpt.
Internet access was disabled for PutnamBench to prevent data contamination, but this also precludes Lean Search for relevant existing library lemmas during those runs.

Relevance to Harnesses / Meta-Harnesses¶

This paper is a direct instantiation of the meta-harness pattern: Claude Code acts as the top-level orchestrator that spawns, monitors, and coordinates specialized subagents (Extractor, Type Planner, Lemma Planner, Type Formalizer pool, Auctioneer, Faithfulness Judge, Proof Critic, etc.), each with access to MCP tools (Lean REPL, Lean Search). The dynamic backtracking mechanism—where the orchestrator rolls back pipeline state and injects feedback to upstream agents—demonstrates how a meta-harness can implement non-linear control flow beyond a fixed DAG. The best-of-$k$ selection with gated quality thresholds and automatic escalation (spawning additional agents until a candidate passes) exemplifies adaptive resource allocation within a harness. The separation of orchestrator context (high-level strategy) from subagent context (compilation details) is a concrete solution to the context-saturation problem that any long-horizon agentic harness must address.