AI 复核上万页数学证明：找出一处人工漏掉的缺口，还证出一个新定理

证明太长，人检查不完

现代数学里有些证明长达上万页，能完整读懂的人极少。形式化验证的做法是把每一步翻译成机器可检查的语句，再逐一验证。

找到的缺口是什么

工具在中间章节发现一处引用不完整——前一步的结论并不能直接推出下一步，需要补一个额外条件。这个缺口在人工评审中一直没被发现。

顺带的结果

补全条件后，验证过程自动生成了一个此前未被记录的推论，最终被整理成一个新定理。这说明形式化工具不只是"检查员"，也可能参与发现。