aiqbench analysis
This study highlights a critical gap in current autoformalization capabilities: while agents can easily close proof gaps ("sorries"), they struggle significantly with high-level architectural decisions like defining reusable APIs and organizing code for expert review. The research argues that evaluating AI mathematical assistants solely on mechanical verification is insufficient, as true utility requires surviving rigorous human scrutiny of definitions and library structure.
Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
arXiv:2606.13925v1 Announce Type: new Abstract: Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We then ran a review-driven refactor and compression process and obtained a second expert review. The before-and-after comparison shows a sharp split: agents adapted well to local, mechanically checkable feedback, but remained weak at choosing definitions and designing APIs. We argue that autoformalization should be evaluated not only by closed sorries, but by whether the resulting formalization survives expert review.
Abstract:Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We then ran a review-driven refactor and compression process and obtained a second expert review. The before-and-after comparison shows a sharp split: agents adapted well to local, mechanically checkable feedback, but remained weak at choosing definitions and designing APIs. We argue that autoformalization should be evaluated not only by closed sorries, but by whether the resulting formalization survives expert review.
Artificial Intelligence (cs.AI); Algebraic Geometry (math.AG)
I.2.3; I.2.7; F.4.1
arXiv:2606.13925 [cs.AI]
(or arXiv:2606.13925v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2606.13925 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 225 words
