在交互式定理证明器中，大型语言模型常常能够弥补证明中的空白，但经过验证的定理与可重用的库贡献并不相同。本文通过详细案例研究探讨这一区别：对Grothendieck消失定理的半自主形式化。初始版本在没有任何错误的情况下编译，但专家评审发现定义、定理的一般性、文件组织和API存在严重问题。
随后，我们进行了基于评审的重构和压缩过程，并获得了第二次专家评审。前后对比显示出明显的差异：智能体适应了局部、机械可检查的反馈，但在选择定义和设计API方面依然薄弱。我们认为，自动形式化的评估不仅应关注关闭错误的数量，还应关注所产生的形式化结果是否能够通过专家评审。
博主点评： 本文揭示了自动形式化过程中的技术挑战，尤其是在定义和API设计方面。专家评审的反馈是提高形式化质量的关键，强调了人机协作的重要性。