Owain Evans：人类用几百年把数学形式化，AI 接棒走完剩余路程

brianryhuang · x · 2026-09-11

Owain Evans 长文梳理数学的「形式化栈」：人类用演化的神经网络历经数百年发展数学，Dedekind 等人把越来越多概念形式化以支持严格证明；Frege、Russell、Turing 进一步把「证明」本身形式化，发明了可验证和搜索证明的机械过程（算法），并证明简单机械系统的通用性。人类随后造出通用计算机，花数十年扩展算力与算法（Turing、Von Neumann、Knuth），但计算机搜索证明长期低效无用。直到人类为神经网络建立简单数学模型并用通用计算机模拟——如今 AI 正在接管数学。引用评论 Peligrietzer 的说法：人类把数学做得足够好，数学已能自己走完剩下的路。