大家好，欢迎收听每日一分钟AI。

数学界有个困扰人类一百多年的"千年难题"，最近 AI 干了一件史无前例的事——第一次自动验算了一份人类最难的数学证明。

先说说这个难题有多出名。你知道"孪生素数"吗？就是像 3 和 5、5 和 7、11 和 13 这样，相差正好 2 的一对素数。数学家猜想：这样的素数对，是不是有无穷多对？一百多年了，没人能证明。

但人类一直在逼近。2013 年，华人数学家张益唐石破天惊，证明存在无穷多对素数、相差不超过 7000 万——这是几百年来的第一次突破。后来英国数学家梅纳德把它压到 600，再后来陶哲轩带着一个协作组，硬是压到了 246。离那个终极目标"2"，只差 244。

而这次 AI 干的，不是把 246 再往下压，而是干了一件更基础的事——把这个"246 定理"的证明，用机器逐行验算了一遍。

具体怎么做的？一家叫 Axiom Math 的公司，用一套叫 AxiomProver 的 AI 系统，把这几十页、极其复杂的证明，翻译成了机器能检查的数学语言，再由计算机一行一行地确认："没错，每一步都站得住脚。"光署名贡献的数学家就有 41 位。

为什么要费这么大劲？这家公司的创始数学家小野健（Ken Ono）说了句很扎心的话：这个世界，很快就要运行在"没人读过的代码"上了。如果 AI 写代码，谁来检查它写得对不对？而这次验算数学证明，就是一次预演——学会让机器检查机器。

当然也得说清楚：这并没有证明孪生素数猜想，246 也没变小。但让最难的数学证明第一次被机器"盖章"，这一步本身，可能比结论更重要。

明天见！

---
📌 本期关键词：246定理 孪生素数 AxiomProver AI验证 陶哲轩 张益唐人在什么情况下才能大彻大悟AI编造
📌 参考来源：IEEE Spectrum、澎湃新闻、Unite.AI、至顶网、AOL