Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

Computer Science > Artificial Intelligence [Submitted on 11 Jun 2026] Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization Vasily Ilin, Brian Nugent 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. Subjects: Artificial Intelligence (cs.AI); Algebraic Geometry (math.AG) MSC classes: 68V20, 68V15, 68V35, 68T07, 55N30 ACM classes: I.2.3; I.2.7; F.4.1 Cite as: 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 Submission history From: Vasily Ilin [view email] [v1] Thu, 11 Jun 2026 21:33:50 UTC (658 KB) Access Paper: HTML (experimental) view license Current browse context: cs.AI < prev   |   next > new | recent | 2026-06 Change to browse by: cs math math.AG References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)