Theory-Level Autoformalization: AI That Formalizes Entire Theories, Not Just Isolated Statements

A team of researchers has introduced the concept of theory-level autoformalization in a new position paper on arXiv. Unlike current approaches that focus on translating individual natural-language statements into formal, machine-verifiable languages, this method aims to formalize entire theories—including all their inter-dependent axioms, definitions, and lemmas—as structured, unified libraries.

Autoformalization is the process of converting informal natural language into a format that machines can understand and verify. Most existing AI systems can only handle single statements in isolation, which limits their ability to capture the full context and dependencies required for complex reasoning. The researchers argue that real formalization efforts are inherently theory-level: you need a complete web of foundational knowledge before target theorems can even be stated.

This shift could have significant implications for fields like mathematics, law, and science. For example, a legal document or a scientific theory could be input into an AI system that breaks it down into a structured, verifiable format—helping lawyers, scientists, and students understand and validate complex information more easily.

The paper, titled "Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases," is available on arXiv. It examines the significance of this shift, addresses alternative views, and identifies key challenges and opportunities for future research.