# Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

arXiv: https://arxiv.org/abs/2607.13292 · HTML: https://mlsanity.com/paper/2607.13292/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 89 references that are in the map.
- First posted on arXiv 14 Jul 2026.

## Builds on (most cited first, 30 of 37)

- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Tool Learning with Large Language Models: A Survey](https://mlsanity.com/paper/2405.17935/) (2024)
- [VeriGen: A Large Language Model for Verilog Code Generation](https://mlsanity.com/paper/2308.00708/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [CRAFT: Customizing LLMs by Creating and Retrieving from Specialized Toolsets](https://mlsanity.com/paper/2309.17428/) (2023)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks](https://mlsanity.com/paper/2401.12869/) (2024)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Generating Natural Language Proofs with Verifier-Guided Search](https://mlsanity.com/paper/2205.12443/) (2022)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)](https://mlsanity.com/paper/2403.04651/) (2024)
- [Text2Cypher: Bridging Natural Language and Graph Databases](https://mlsanity.com/paper/2412.10064/) (2024)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [A New Approach Towards Autoformalization](https://mlsanity.com/paper/2310.07957/) (2023)
- [Formalizing Chemical Physics using the Lean Theorem Prover](https://mlsanity.com/paper/2210.12150/) (2022)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)

## Built on by (most cited first, 3 of 3)

- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)

## Abstract (arXiv)

Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.