Axiom Math团队用AI系统AxiomProver首次自动验证素数相关定理「246定理」，标志AI辅助数学形式化验证取得重要里程碑。

OpenAI即将发布的推理模型Astra以约2000美元算力成本，成功破解10个数学与理论计算机科学领域长期悬而未决的难题，包括首个非SoFIC群的显式构造及对Connes刚性猜想的否定。所有证明均通过Lean 4...