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

> Theo, an agentic framework using general-purpose coding LLMs, autoformalizes research mathematics into Lean 4, proving 32/32 sampled Putnam problems and catching a false lemma in a published STOC paper.

- **Source:** [arXiv](https://arxiv.org/abs/2606.31134)
- **Published:** 2026-08-17
- **Permalink:** https://picx.dev/p/UsUzlm
- **Whiteboard:** https://picx.dev/p/UsUzlm/image

## Summary

# 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)**

| Method | Backbone / Setting | Solved/672 | Accuracy | Cost/Q. |
|---|---|---|---|---|
| *Specialised Lean Provers* | | | | |
| Kimina-Prover-7B-Distill | 7B, Pass@192 | 10 | 1.5% | <$1* |
| Bourbaki | 7B, Pass@512 | 26 | 3.8% | <$1* |
| DeepSeek-Prover-V2 | 671B MoE, Pass@1024 | 47 | 7.0% | ~$18* |
| Goedel-Prover-V2 | 32B, Pass@184 | 86 | 12.8% | <$1* |
| *General LLM, single short pass* | | | | |
| GPT-5 (ReAct, 10 turns) | GPT-5, Pass@1 | 28 | 4.2% | <$1* |
| *Agentic / Hybrid Systems* | | | | |
| Seed-Prover | RL-tuned, "medium" | 329 | 49.0% | — |
| AxProverBase | Claude Opus 4.5 | 365 | 54.3% | $12.60 |
| Hilbert | Gemini 2.5 Pro + Goedel-V2 | 462 | 68.8% | ~$39* |
| Aleph ($100 cap) | GPT-5.2 agentic | 500 | 74.4% | $23 |
| Seed-Prover 1.5 | 10 H20-GPU-day budget | 581 | 86.5% | ~$168* |
| Aleph ($400 cap) | GPT-5.2 agentic, Pass@2 | 637 | 94.8% | $54 |
| Aleph ($1400 cap) | GPT-5.2 agentic, Pass@3 | 668 | 99.4% | $68 |
| **Ours** | **Claude Opus 4.7, single attempt** | **32/32** | **≥91.3%†** | **~$5** |

†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**

| Paper | Area | Axioms beyond kernel |
|---|---|---|
| Mackenzie and Saffidine [19] | Communication complexity | **None** |
| Gravin and Jia [20] | Mechanism design | **None** |
| Pham [17] | Combinatorics | 1: paper's Lemma 2.9 bound |
| Rivkin et al. [21] | Information-theoretic LB | 2: [32, 33] |
| Kalai et al. [22] | Learning theory | 3: [34, 35, 36] |
| OpenAI [23] | Discrete geometry | 2: [37, 38] |
| OpenAI [24] | Graph theory | 3: [39, 40, 41] |

#### 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**

| Paper | Cost ($) | Input | Output | Cached input |
|---|---|---|---|---|
| Pham [17] | 688.42 | 0.61M | 3.41M | 0.60B |
| Mackenzie and Saffidine [19] | 1,697.28 | 1.77M | 9.23M | 1.85B |
| Gravin and Jia [20] | 1,240.12 | 1.39M | 5.26M | 1.35B |
| Rivkin et al. [21] | 2,608.86 | 4.71M | 11.30M | 2.76B |
| Kalai et al. [22] | 4,527.42 | 2.35M | 16.11M | 5.02B |
| OpenAI [23] | 2,480.64 | 0.13M | 3.20M | 2.63B |
| OpenAI [24] | 438.31 | 0.05M | 1.20M | 0.49B |
| **Total** | **13,681.05** | **11.01M** | **49.71M** | **14.70B** |

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/

---

_Markdown view of https://picx.dev/p/UsUzlm, served by PicX — AI-generated visual whiteboard summaries of research papers._