「理解」本就是弱概念:Lean 证明才算精确理解,机器正在其上发现

sytelus · x · 2026-09-19

作者主张「understanding」是个很弱的描述:人类所谓的理解不过是公理加程序,机械地套用就能持续奏效,最根本层面上没有人真正「理解」什么。他认为任何 Lean 形式化证明才提供了对命题为何成立的精确且完整的理解,而机器会基于它们不断构建、做出新发现——因为机器确实「理解」了它们。如果人类消化不了,那是人类自己的问题,正如公众无法消化菲尔兹奖得主的工作也从不妨碍后者。