OpenAI 发布 722 个 AI 生成的数学证明
精选理由
OpenAI 用 AI 生成了 722 个数学证明，还把矩阵乘法的复杂度纪录从 AlphaEvolve 的 n^2.37 压到 n^2.25，附带 Lean 验证，搞数学和算法的可以看看。
OpenAI 发布了 722 个由 AI 生成的数学证明。其中在矩阵乘法这一问题上，把已证最低复杂度从 AlphaEvolve 在 8 月创下的约 n^2.371177 降到约 n^2.25。结果附带 Lean 形式化验证，但属于理论上界，尚未转化为可用的更快的 GPU 实际计算例程。
原文 · rohanpaul_ai
OpenAI today released 722 AI generated math proofs.
This is one of the achievement, on the topics of Matrix multiplication
Here it lowers the proven cost of multiplying 2 n×n matrices from about n^2.371177, the record that AlphaEvolve set in August, to about n^2.25.
The result comes with a Lean formalization, but it is a theoretical bound and does not yet hand engineers a faster routine for real GPU workloads.
