Lean

Lean是一种把数学证明转写成计算机可以核验的形式的语言。就像我们在学校做数学题时,必须把中间的每一步计算都写出来,批改的人才能确认对错一样,用Lean写证明时,必须把每一个极其细小的逻辑步骤都完整写出来,不能有任何省略。作为回报,计算机可以机械地逐行核对每一步是否正确,不用担心人工阅读时会看漏错误。

数学家平时写的证明通常只有几页文字,中间常常省略'这是显然的''方法与前面相同'之类的步骤。人类读者可以自行补全这些省略的部分,但计算机不能,所以要把证明转写成Lean,就必须把所有省略的步骤都完整展开。因此,原本只有几页的证明,一旦转写成Lean,往往会变成数百万行代码。

这种毫无遗漏的重写工作被称为形式化。如果由人工来做,可能需要花上数年之久,极其繁琐且工作量巨大;但一旦用Lean完成,这份证明是否真的正确,就不再需要依赖人的判断了。

文章中提到,"Claude用一种叫Lean的证明语言写出了多达1300万行代码。"这里的Lean并不是Anthropic开发的工具,而是数学界早已在使用的证明验证语言。Claude是按照这种语言的语法写出了证明,并不是它自己创造了Lean,这一点不应混淆。