Claude 20分完成，o4-mini弃题

最新实验中，陶哲轩围绕一个代数蕴含展开（algebraic implication）：证明方程1689蕴含方程2。

录制前，他已进行了一次测试。

这里直接在Claude/o4-mini中粘贴prompt，然后附上非形式证明、形式证明、方程三个附件。

接下来，一起看看这两个模型具体表现如何？

Claude

实验中，Claude整体表现出色，能够快速将非形式证明的单行，转化为看似合理的Lean代码。