Human mathematicians are being outcounterexampled

Kevin Buzzard 描述了一种新研究循环：模型先寻找反例，再把结论形式化到 Lean，由人检查陈述是否忠实、依赖是否可信、证明是否编译。文中 Sol 三周生成约 120 万行 Lean，而 mathlib 九年约 230 万行；一个 60 年问题的反例最终是 1076 行 Lean，本地验证不到五分钟。速度令人震动，但作者也记录了模型先写出错误非正式论证、另一模型再找出反例的情况，说明形式验证解决“对不对”，尚未解决“为什么”和人类如何吸收海量证明。