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

Marcus J. Min; Mike He; Zhaoyu Li; Zixuan Yi; Sharad Malik; Aarti Gupta; Xujie Si; Osbert Bastani

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

Artificial Intelligence 2026-07-14 v1 Computation and Language Machine Learning Programming Languages

Authors: Marcus J. Min , Mike He , Zhaoyu Li , Zixuan Yi , Sharad Malik , Aarti Gupta , Xujie Si , Osbert Bastani

Abstract

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.

Keywords

autoformalization formal verification knowledge base theorem proving theory-level formalization position paper

Cite

@article{arxiv.2607.13292,
  title  = {Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases},
  author = {Marcus J. Min and Mike He and Zhaoyu Li and Zixuan Yi and Sharad Malik and Aarti Gupta and Xujie Si and Osbert Bastani},
  journal= {arXiv preprint arXiv:2607.13292},
  year   = {2026}
}

Comments

ICML 2026 Spotlight