用 AI 推进 OpenAI 新数学发现：13 维最优证明已通过 Lean 验证
Moretheevu · reddit · 2026-10-08
一位开发者受 OpenAI 近期数学研究启发，用 AI 辅助完成了两个开源项目：
- 新数学结果：OpenAI 曾证明某种几何效应在 10 维形状上成立，作者借助 AI 进一步证明在该形状族中 13 维是最优维度。
- 实用科研工具：研究者常用「打乱网络」检验规律是否只是巧合，作者基于新数学构建了一个工具，可计算达到指定误差界所需的最少打乱次数，替代经验猜测。
两个项目都包含经 Lean 形式化证明系统逐步验证的证明（第二项软件未做端到端形式化验证）。作者强调：形式化验证不能证明结论的新颖性，但能大幅提升对数学正确性的信任。全部开源，并记录了 AI 参与过程。作者自述原本没期待有产出，结果意外收获。
所属事件:开发者用 AI 接力 OpenAI 数学发现，13 维最优结果经 Lean 验证并开源(2 条相关)→
「漫话AGI」频道最新
- NYU 数学教授:OpenAI 投入数百万美元算力攻坚千禧年大奖难题 — rohanpaul_ai · 2026-10-10
- AI 是不是偷走了开源社区感?Hacktoberfest 今年悄然无声 — _jaydeepkarale · 2026-10-10
- 该不该读博?研究者:不是没东西可发现,而是博士不是发现的正确场所 — tensorqt · 2026-10-10
- 为什么人们坚信意识只属于人类?连猫狗都被排除了 — RileyRalmuto · 2026-10-10
- 「软件像食物」:开发者谈 AI 时代如何让人爱上你的产品 — pixlpa · 2026-10-10
- Pedro Domingos 断言:超级智能将成寻常之物 — pmddomingos · 2026-10-10