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

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/Awesom e-Autoformalization.

Introduction. We define Theory-Level Autoformalization as the task of automatically formalizing the entire theoretical context within a given scope, including axioms, definitions, notations, examples, lemmas, theorems, proofs, tactics, and all their inter-dependencies, as a coherent formal library. As depicted in the “Theory-Level Autoformalization Tower” (Figure 2), formalizing even a single target theorem like the Pythagorean theorem requires first constructing multiple layers of axiomatic primitives, derivative definitions, and proof infrastructure. This contrasts with statement-level autoformalization, which translates individual theorems in isolation and implicitly relies on formal theoretical contexts like Lean Mathlib (Mathlib Community, 2020). For do- The need for this shift is evident from real-world formalization efforts (Table 1). The Kepler conjecture is a single statement, yet its formalization required 11 years of constructing an entire web of definitions and supporting lemmas (Hales et al., 2015).

Discussion / Conclusion. We have argued that autoformalization must move beyond isolated statements to formalize entire theories as holistic formal knowledge bases. We identified open challenges and proposed paths forward, aiming to turn autoformalization from a per-statement demonstration into a scalable tool for real-world verification and theoretical discovery.