Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Summary (Overview)

• Theo: A multi-agent autoformalization framework powered by general-purpose coding LLMs (Claude Code) that translates natural-language research mathematics into machine-verifiable Lean 4 code.
• Type-first formalization paradigm: The system dynamically extends Mathlib by defining missing domain-specific types, validated via a novel Auxiliary Lemma technique (unit-test-style verification) before formalizing primary theorems.
• Empirical results: Achieved a lower-bound accuracy of 91.3% on PutnamBench (32/32 random sample solved) at ~$5/problem, outperforming specialized Lean provers; successfully formalized main theorems from seven research papers (five STOC, two OpenAI manuscripts), with two developments requiring no axioms beyond Lean's kernel.
• Key discovery: The pipeline uncovered a computer-verified gap in a published STOC proof (Pham [17]), demonstrating the system's value as a proof-checking tool.
• Cost efficiency: Runs on a standard $200/month subscription (~$1,200 total over six months) rather than metered API ($13,681 API-equivalent), requiring no local GPUs.

---

Introduction and Theoretical Foundation

Motivation

Large Language Models (LLMs) produce subtle logical errors that differ from human mistakes, making manual verification of AI-generated proofs impractical. Formal languages like Lean 4 offer mechanical proof checking, motivating autoformalization: the automatic translation of natural-language mathematics into verifiable code.

Key Insight

Recent trends show general-purpose LLMs (optimized for standard programming) now outperform smaller models explicitly fine-tuned for Lean. This shift enables a new approach: leveraging powerful coding agents for formal mathematics.

The Two-Task Split

Autoformalization divides into:

1. Statement formalization: Translating the theorem's statement into Lean. Challenge: No mechanical ground truth exists to verify semantic alignment with the source.
2. Proof formalization: Proving the formalized statement. Benefit: Direct compiler feedback guides the process.

Limitations of Prior Approaches

• Single-agent setups: Failed proof attempts and compilation errors saturate the context window, degrading long-horizon reasoning.
• Fixed pipelines: Process statements in rigid sequential order, cannot backtrack when an earlier step fails.

Core Principle: Faithful Leanification

"The Lean development should faithfully reflect what the paper proves, what it assumes, and the proof strategy used by its authors."

This boundary-aware approach mirrors mathematical peer review: results imported from prior work are declared as citation-linked axioms rather than reproved, isolating formalization effort to the paper's core contributions. Through paper chaining, verified theorems from one development can discharge axioms in another.

---

Methodology

System Architecture

Theo is built around an Orchestrator (the Claude Code session) managing two pipelines:

1. Statement Formalization Pipeline

1. Extractor: Identifies the main theorem from the paper's PDF and LaTeX source, capturing all required definitions and assumptions.
2. Type Planner: Determines which types beyond Mathlib are needed, generating a dependency-ordered type plan.
3. Type Formalizer (per type, k parallel attempts):
   • Type Leanifier: Translates the informal type into Lean, iterating with the Faithfulness Judge.
   • Lemma Formalizer: Translates associated auxiliary lemmas into Lean.
   • Lemma Prover: Attempts to prove the lemmas (with a Claim Check tool preventing statement alteration).
4. Auctioneer: Ranks candidates via best-of-k selection based on: proportion of proved lemmas, semantic alignment, and code length. Strictly gated—spawns more attempts if no candidate passes.
5. Theorem Formalizer: Translates the primary theorem statement, collaborating with the Faithfulness Judge.

2. Proof Formalization Pipeline

Treats proofs as a recursive tree of proof-nodes (root = main theorem):

1. Natural Language Prover: Proposes an informal proof, revising internally with the ProofCritic until clean.
2. ProofDetailer: Expands into tactic-sized steps and named sub-lemmas.
3. Lemma Breakdown: Decomposes into topologically ordered lemmas with stable identifiers.
4. Lemma Leanifier: Translates each into Lean statements (body left as sorry).

Key strategy: Prove parent nodes before children, using child statements as unproven premises—revealing whether child lemmas are actually usable.

Key Components

Faithfulness Judge

Runs four independent verifications (two blind, two direct) across different models:

• Blind: An Informalizer subagent back-translates Lean code to natural language for comparison.
• Direct: Compares comment-stripped Lean code against the intended statement.
• A judge agent dismisses false positives; a single confirmed error flags the formalization invalid.

ProofCritic

Audits informal proofs purely in natural language, emitting concrete questions about: unstated hypotheses, undefined terms, hidden case splits, swapped quantifier orders, and appeals to "standard arguments."

Auxiliary Lemma Technique

Before accepting a new type definition, the system generates and proves general lemmas about it. Unprovable lemmas indicate flawed formalizations, triggering retry—functioning like unit testing in software engineering.

Shared Tools

• Lean Search / Lean Lookup: Documentation retrieval.
• Lean REPL: Compiles code snippets, reports goals, errors, and compilation status.

Integrated Techniques

• Back-translation [15]: Verifies theorem statements.
• Lemma decomposition [16]: Streamlines proof generation.
• Axiom declaration for prior work [7]: Isolates formalization to core contributions.

---

Empirical Validation / Results

PutnamBench Evaluation

• Setup: 32 randomly sampled problems (seed = 0), internet disabled, no hand-prepared proofs.
• Result: All 32 solved → lower-bound accuracy of 91.3% at 95% confidence (Wilson bound).
• Cost: ~$5/problem (subscription), ~$29/problem API-equivalent.

Table 1: State-of-the-art comparison on PutnamBench Lean 4 (672 problems)

†Wilson lower bound at 95% confidence on a uniformly random sample of 32 problems (seed = 0).

Research-Level Mathematics

Seven papers formalized across combinatorics, communication complexity, mechanism design, learning theory, discrete geometry, number theory, and graph theory:

Table 2: The seven research papers formalized

Highlight: Pham [17] — Gap Discovery

The pipeline formalized the paper's headline theorem:

There exists a constant $c > 0$ such that the following holds. Let $t > 0$ be an integer. Assume that $H$ admits a fractional cover $w : 2^X \to [0, 1]$ such that $\sum_{W \in 2^X} w(W) p^{|W|} \le 1/2$ and $w$ is supported on sets of size at most $t$. Then $c_{\mathrm{int}}(\mathcal{H}; q) \leq 1/2$ for $q = cp/\log t$.

The Lean formalization (Figure 4 in paper) defines FractionalCover, IntegralCover, and IsPSmall structures. Critical finding: The system discovered the paper's Lemma 2.6 is false as stated (with an explicit computer-verified counterexample), invalidating the proof of the Lemma 2.9 bound. The pipeline admitted this bound as a single scoped axiom and proved everything else from scratch.

Axiom-Free Achievements

• Mackenzie and Saffidine [19] (refuting the Direct Sum Conjecture): Both qualitative and quantitative theorems proved with no axioms—even cited results (Chung's product theorem, Kushilevitz–Nisan log-rank bound) were reproved from scratch.
• Gravin and Jia [20] (median mechanism for facility location): Four theorems (upper bound, tightness, consistency, robustness) all axiom-free and sorry-free.

Scale of Formalizations

• OpenAI [23] (unit distances): 14,831 lines of Lean, 2 axioms—less than half the size of the independent Aleph Prover formalization (~33,000 lines).
• OpenAI [24] (cycle double cover): 5,713 lines of Lean, 3 citation-backed axioms.

Cost Analysis

Table 3: Cost and token usage for the seven research papers

Actual outlay: ~$1,200 over six months on the$200/month subscription (~95% of API-equivalent spend comes from prompt-cache traffic).

---

Theoretical and Practical Implications

Software Engineering Principles Applied to Mathematics

The paper introduces a methodological shift by directly applying:

• Object-oriented type decomposition: Breaking mathematical domains into structured types.
• Unit-test-style verification: Auxiliary lemmas validate type definitions before use.
• Dynamic backtracking: The orchestrator can revert to earlier pipeline states, unlike rigid fixed pipelines.

Faithful Leanification as a Standard

The principle that formalizations should preserve the epistemic boundary of source papers (proving what the paper proves, assuming what it assumes) provides a rigorous standard for autoformalization that mirrors mathematical peer review.

Proof Checking as a Scientific Tool

The discovery of a gap in a published STOC proof demonstrates that autoformalization systems can serve as automated proof auditors, providing concrete scientific value beyond formalization itself.

Democratization of Theorem Proving

By operating on a flat-rate subscription (~$5/problem on PutnamBench) rather than metered API or GPU clusters, Theo drastically lowers the barrier to entry for automated theorem proving, making it accessible to researchers without specialized hardware.

Limitations Acknowledged

• Algorithmic proofs: The system does not formalize algorithmic results (e.g., the algorithmic upper bound in Rivkin et al. [21], the polynomial-time learning algorithm in Kalai et al. [22]).
• Axiom dependence: Papers resting on heavy external machinery require citation-backed axioms, though this is framed as an honest readout of self-containedness rather than system weakness.

---

Conclusion

Theo demonstrates that general-purpose coding LLMs, orchestrated through a flexible multi-agent framework, can achieve state-of-the-art autoformalization performance at a fraction of the cost of specialized systems. Key takeaways:

1. Type-first formalization with auxiliary-lemma validation effectively bridges gaps in existing formal libraries like Mathlib.
2. Dynamic orchestration with structured-failure feedback outperforms both single agents and fixed pipelines.
3. Faithful Leanification provides a principled framework for handling prior-work citations and preserving epistemic boundaries.
4. The system's success on PutnamBench (≥91.3% lower bound) and seven research papers—including two axiom-free STOC formalizations—establishes it as a practical tool for research-level mathematics.

Future Directions

• Paper chaining: Discharging axioms in one development with verified theorems from another, creating a growing web of interconnected formalizations.
• Algorithmic proof formalization: Extending the framework to handle algorithmic results (currently a stated limitation).
• Human-in-the-loop refinement: The flexible design supports researchers injecting domain expertise mid-process without pipeline restarts.

All formalizations are publicly available at: https://beyondthelibrary.github.io/formal_arxiv/