Goedel-Scribe: Toward Faithful Statement Autoformalization via Adversarial Mutation

AI systems now possess the capability to produce Annals-level mathematical content autonomously. This capability introduces an asymmetry in the review process wherein the pace of generation of mathematical content far exceeds the (human) review capacity of the field. One way forward for the community is to more heavily rely on *formalized* proofs in languages like Lean. A pivot to formalization also has benefits for autonomous AI generation as models can iteratively improve proof candidates without the need for human intervention until a final compiling proof is produced. However, this shifts the importance of verifying proofs to verifying *faithfulness of statements* in Lean. A compiling proof matters only insofar as it corresponds precisely to a natural language mathematical statement. Complicating this matter is the reality that most human mathematicians are not currently fluent in Lean, meaning reliable AI assistance in formalizing statements, or whole papers, is necessary. In this work, we outline reasons for shifting focus to (auto)formalization of mathematical statements, we describe several desiderata of a formalization process, and we present a lightweight and flexible pipeline for AI driven autoformalization of mathematical statements. Our pipeline outperforms competing AI autoformalization approaches by relying on kernel certified repairs to mis-formalizations, and, when tested, autonomously finds several mis-formalizations in existing Lean code, including code used in benchmarks, and code certified by human mathematicians.