Axiom Math 用 AI 形式化验证 246 定理，素数间距证明通过机器检查
AI 完成 246 定理形式化验证，人类素数间距最前沿结论首次获机器确认。
AxiomProver 将“246 定理”的人类证明形式化为 Lean 4 代码，确认逻辑无误。该定理是孪生素数猜想的最接近成果，由 Maynard 与陶哲轩等推进至 246。AI 验证了 50 维优化及关键常数，全部证明仅依赖两个外部定理。
正文摘录
 新智元报道  人类证出来的最难素数定理，AI 刚刚从头到尾验了一遍。 结论是： 证明成立，逻辑无误。 8 月 17 日，由一位 25 岁广州女孩创立的 AI 公司 Axiom Math 宣布，自家系统 AxiomProver 完成了「246 定理」的形式化验证。  论文地址： https://primegaps.axiommath.ai/paper/ 所谓 246 定理，指的是无论数字多大，你总能找到两个素数，它们之间的间距不超过 246。 虽然离终极目标「差距为 2」还差着不少，但它已经是目前最接近「孪生素数猜想」的结果了。  根据 Axiom Math 创始数学家 Ken Ono 的解释：「这个定理，就是人类目前对素数理解的天花板。」 那么，这次的验证到底是怎么做的呢？  246 这个数字怎么来的 故事要从孪生素数猜想说起。 这是 19 世纪提出的老问题，猜的是存在无穷多对相差为 2 的素数。