AI 助力证明森多夫猜想，陶哲轩验证代码
机器之心 · wechat · 2026-08-16
初创公司 CEO Lech Mazur 借助 GPT-5.6 Pro 和约 9 万行 Lean4 代码，成功证明了困扰数学界约 70 年的森多夫猜想。陶哲轩随后用 AI 辅助消化并简化了该证明，将代码缩减至 1.5 万行，并发现论证实际上解决了更强的 Phelps-Rodriguez 猜想。这一事件标志着 AI 在数学证明和形式化验证中扮演了核心角色，改变了传统数学研究的人机协作模式。
「漫话AGI」频道最新
- 机场叫车被困两小时:为什么简单规则比 AI 更该先做好 — shashib · 2026-10-16
- 博导给每个博士生配 Codex Pro：执行力变廉价，选题能力才是 PhD 的价值 — DJiafei · 2026-10-16
- ASI 能否在人类消失后靠现有机器人供应链自续?引发热议 — NathanpmYoung · 2026-10-16
- 「万物基建化」论:AI 时代最终只剩算力、存储、推理等基础设施消费可卖 — AccBalanced · 2026-10-16
- Dwarkesh 在纽约时报发文：2030 年 AI 将完成经济中全部工作 — Traditional-Chip8339 · 2026-10-16
- 「奇点期间的每一周都疯狂」：开发者感叹 AI 进展节奏 — tszzl · 2026-10-16