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.

翻译：大型语言模型通常能够填补交互式定理证明器中的证明漏洞，但已验证的定理不等同于可复用的库贡献。我们通过一个详细案例研究这一区别：格罗滕迪克消没定理的半自主形式化。初始版本编译通过且无任何未解决证明缺口，但专家评审发现其定义、定理泛化性、文件组织及API存在严重问题。随后我们执行了评审驱动的重构与压缩过程，并获得了第二次专家评审。前后对比显示出显著分歧：代理能良好适应局部、可机械检查的反馈，但在定义选择与API设计方面仍显薄弱。我们认为自动形式化的评估不应仅以关闭未解决缺口为依据，而应取决于生成的形式化内容能否经受专家评审。