AxiomProver 完成素数间隔定理 BGP246 的 Lean 形式化

Zulfikar_Ramzan · x · 2026-08-18

Axiom（axiommathai）宣布：用 AxiomProver 完成了「BGP246 定理」的机器可检验形式化——即素数间小间隔的最佳已知界 246，这是数学界距离孪生素数猜想最近的结果。

成果不止验证一条定理：还交付了可复用组件与新的开源库 PrimeGapsLib，为社区提供了可检验、可继续构建的形式化基础设施。前MIT教授、Ripple CTO Zulfikar Ramzan 转发称赞，称这是 AI 辅助数学研究的 remarkable 时刻。