Kevin Buzzard｜What is the point of formalisation?

观看 Rutgers 讨论班录像（YouTube，1:17:33） (opens in a new tab)

活动时间　美国新泽西州当地时间 2026-02-04 10:00–11:00。北京时间 2026-02-04 23:00 至 2026-02-05 00:00。

把数学写成机器可核查的形式，究竟是为了什么？Buzzard 回顾自己对这个问题的看法如何变化，再从 AI 工具已能自动完成部分形式化工作的现状，解释为什么仍然值得投入精力组织、维护和复用形式化数学。

Rutgers 数学系公告 (opens in a new tab)