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

The paper presents a case study on the semi-autonomous formalization of Grothendieck's vanishing theorem using large language models in interactive theorem provers. It highlights the challenges faced during expert review, including issues with definitions, theorem generality, file organization, and API design, despite the initial version compiling without errors. The findings emphasize the need for autoformalization to be assessed not just on technical correctness but also on its robustness in expert evaluations, which is critical for practitioners aiming to ensure the reliability of automated formalization processes.