Search papers, labs, and topics across Lattice.
This paper advocates for a shift from isolated statement autoformalization to a comprehensive approach that encompasses entire theories, including their axioms, definitions, and interdependencies. By framing formalization as a structured library of knowledge, the authors highlight the limitations of current methods that focus solely on individual statements. The key result is a proposed framework for theory-level autoformalization that addresses existing challenges and outlines three potential avenues for future research.
Transitioning from isolated statements to a unified theory-level autoformalization could revolutionize how we build 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/Awesome-Autoformalization.
