Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
06:00 · July 16, 2026 · arXiv cs.AI RSS
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.
Summary
Autoformalization converts informal mathematical or scientific arguments into machine-checkable formal languages. Current systems largely operate at the statement level, translating individual theorems while assuming that an underlying library of axioms, definitions, and lemmas already exists. The position paper argues that this assumption breaks down for most substantive targets: even a single result such as the Pythagorean theorem or the Kepler conjecture presupposes an entire tower of primitive sorts, derived notions, notations, and proof infrastructure that must be assembled first.
Real formalization projects illustrate the gap. The Kepler conjecture required eleven years of constructing supporting definitions and lemmas before the central statement could be expressed; the Liquid Tensor Experiment similarly demanded substantial portions of condensed mathematics. These efforts show that the dominant cost lies not in rendering one sentence but in building coherent formal theories whose components depend on one another. Statement-level tools therefore succeed mainly when they ride on mature libraries such as Lean’s Mathlib; outside those domains the missing context must be created explicitly.
The authors identify several technical obstacles to scaling theory-level work. Evaluation must move beyond isolated statement accuracy to measures of library coherence, including equivalence checking across alternative formalizations. Low-resource domain-specific languages lack the parallel corpora that current models rely on, and multimodal inputs—diagrams, notation, and prose—remain poorly supported. They also note that new theoretical advances often depend on fresh abstractions that reorganize existing knowledge, an operation that isolated translation cannot perform.
To address these issues the paper outlines three directions: construction of benchmarks that reward complete library synthesis rather than single-statement fidelity; development of a common intermediate representation that decouples informal input from any particular proof assistant; and systematic study of how neural models can propose, verify, and refactor the layered components of a formal theory. Together these steps aim to shift autoformalization from a translation aid into a practical engine for building and extending unified formal knowledge bases.
Why it matters
The paper is highly relevant for Dutch AI researchers and high-tech enterprises that rely heavily on formal verification for hardware and software. It provides a strategic roadmap for using AI to automate the creation of formal knowledge bases, aligning with the EU's push for trustworthy and verifiable AI systems.
