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

arXiv: https://arxiv.org/abs/2606.13925 · HTML: https://mlsanity.com/paper/2606.13925/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 17 references that are in the map.
- First posted on arXiv 11 Jun 2026.

## Builds on (most cited first, 9 of 9)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature](https://mlsanity.com/paper/2603.08139/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [Evaluation of LLMs for Mathematical Formalization in Lean](https://mlsanity.com/paper/2606.05632/) (2026)

## Built on by (most cited first, 4 of 4)

- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [Definition Grounding in Theory-Level Auto-formalization](https://mlsanity.com/paper/2610.19223/) (2026)

## Abstract (arXiv)

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.