Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Research mathematics often introduces concepts and dependencies beyond the coverage of existing formal libraries. Autoformalizing such work requires constructing suitable definitions, checking their correspondence with the source, and developing proofs over them. We introduce Theo, an agentic framework powered by general coding LLMs that integrates these tasks in a definition-first workflow. To select among candidate formalizations of new definitions, Theo generates auxiliary lemmas and attempts to prove them under each candidate. It favors candidates that make these proofs easier, using proof difficulty as a proxy for formalization quality. An orchestrator then builds on the selected definitions through recursive proof development and semantic review, revising them when downstream issues arise. We evaluate proof generation on 32 randomly sampled PutnamBench problems and obtain checked proofs for all 32. We also formalize selected main results from nine research papers, including five STOC papers, Babai’s graph isomorphism result and the Strong Perfect Graph Theorem of Chudnovsky et al. The case studies expose a gap in a STOC proof, three incorrect intermediate statements in the Strong Perfect Graph Theorem proof, and three gaps in Babai’s graph isomorphism manuscript. For the latter two developments, we prove repaired statements and steps that preserve the main results. These findings demonstrate how formalization can complement mathematical proof review.