Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
For researchers in formal verification and AI, this position paper highlights a conceptual gap but offers no empirical evidence or new method.
The paper argues for shifting autoformalization from isolated statements to complete theories, identifying open challenges and proposing three research directions. No concrete results or numbers are provided.
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.