Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

As AI systems become increasingly capable of generating mathematical proofs, the primary bottleneck has shifted from proof generation to proof verification. Large Language Models (LLMs) often produce subtle logical errors that are difficult for humans to detect. This paper addresses the need for autoformalization—the automatic translation of natural language mathematics into machine-verifiable code—to enable rigorous, scalable validation of research-level proofs.

The authors introduce Theo, an agentic autoformalization framework that manages two distinct pipelines: one for formalizing theorem statements and one for formalizing proofs. Unlike rigid, sequential pipelines, Theo uses a centralized orchestrator that treats formalization as a dynamic software engineering project.

Key innovations include:

• Type-First Formalization: Because research mathematics often relies on concepts absent from existing libraries like Mathlib, the system explicitly defines missing domain-specific concepts before attempting to formalize the primary theorem.
• Auxiliary Lemma Verification: To ensure the faithfulness of these new definitions, the system generates and proves auxiliary lemmas related to the new types. This acts as a unit-testing suite; if the prover cannot prove these lemmas, the system identifies the type definition as potentially flawed and iterates.
• Faithfulness Judge: The system employs a multi-model judge that performs both blind and direct verification to ensure the generated Lean code semantically aligns with the original natural language source.

Theo demonstrates high performance and reliability across two domains. On the PutnamBench benchmark, the system achieved a lower-bound accuracy of 91.3% on a random sample of 32 problems, significantly outperforming previous methods while maintaining a low operational cost of approximately $5 per problem.

For research-level mathematics, the authors formalized main theorems from seven papers spanning fields such as combinatorics, communication complexity, and graph theory. Notably, the system produced fully machine-checked proofs for two STOC papers using no axioms beyond Lean’s standard kernel. Furthermore, the system’s rigorous checking process surfaced a previously undetected gap in a published STOC proof, demonstrating its utility as a tool for peer review.