标签: 形式化验证

2026 年 7 月 20 日，世界杯决赛正踢得胶着。数学家 Levent Alpöge 发了一条推文——Claude Fable 找到了 Jacobian 猜想的一个反例。87 年的公开问题，反例只有一行多项式。

同一天，剑桥数学家 Kevin Buzzard 在博客上写了一篇长文，标题是 "Human mathematicians are being outcounterexampled"（人类数学家正在被反超）。他整理了两个月内发生的三件事：

• 5 月 20 日：ChatGPT 构造了 Erdős 单位距离猜