人类数学家正被反例超越

摘要

在形式化与AI工具的交汇处，反例成为焦点。2026年5月20日，ChatGPT反驳了离散几何中的Erdős单位距离猜想，人类数学家虽经核查但未在Lean中形式化。五天后，Logical Intelligence（由Turing奖得主Yann LeCun共同创立）将其自动形式化于Lean中。该证明依赖Golod-Shafarevich定理，该定理的证明需100多页且涉及全局类域论，目前全局情形尚未形式化。Buzzard的学生Edison Xie正在完成局部情形的PhD项目。