AI 找到了新的矩阵乘法方法。
AlphaTensor 用强化学习寻找矩阵乘法算法。作者在研究所覆盖的设定中检查了这些构造是否成立。
它说明了什么
计算机搜索系统可以帮助发现特定数学任务中有效的新算法。
它没有说明什么
这不表示 AI 能解决所有算法问题、证明普遍下界，或者取代人的数学判断。
为什么重要：这是一个具体例子：AI 不只是在预测文字，也能帮助构造数学对象。
阅读原始来源 · Nature，2022已核实例子 · 最后检查于 2026 年 10 月 31 日
AI 在理论计算机科学里，真正做到了什么
这里收录的是一些经过核对的例子，它们改变了 AI 能在数学研究流程中承担哪一部分工作。 这不是实时新闻流，也不是这个领域的完整历史。
怎么读：
先看“它说明了什么”，再看“它没有说明什么”。一项结果可能是真的，但仍然比新闻标题窄得多。
证据时间线
三个已核实例子，三种不同的工作。
每一项都附上我们核对过的原始来源。证据标签沿用全站统一的四类标准。
AI 在 Lean 中搜索形式化证明。
AlphaProof 在 Lean 证明助手中学习，并为部分奥赛级问题找到了形式化证明。论文同时报告了大量算力消耗和任务范围有限的限制。
它说明了什么
AI 可以参与这样的流程：由证明助手检查一份形式化证明是否有效。
它没有说明什么
一道竞赛题的形式化证明，不等于研究级数学的普遍理论；搜索还需要大量算力。
为什么重要：它说明了证明检查为什么重要：验证的是证明本身，不是 AI 有多自信。
阅读原始来源 · Nature，2025AI 在人类证明框架中提供了有限结构。
AlphaEvolve 找到有限组合结构。经过计算机检查后，研究者把这些结构放入已有证明框架，改进了复杂度理论中的界。
它说明了什么
AI 可以帮助证明流程中的一个具体环节：寻找一个可以被检查的有限对象。
它没有说明什么
更完整的证明仍依赖人类设计的数学框架；不能把它泛化为 AI 已经解决了复杂度理论。
为什么重要：它把有用的一小步和完整定理分开：找到一个有限对象，不等于证明一个普遍命题。
阅读原始来源 · Google Research，2025接下来看什么