Freek Wiedijk 百大定理清单全部完成形式化证明
satnam6502 · x · 2026-09-06
有人宣布,Freek Wiedijk 的著名「百大数学定理」清单上最后一个定理也已被形式化,标志着这份清单的完成。Microsoft Research 的 satnam6502 回忆 2006 年面试时,George Gonthier 的电脑正在后台运行四色定理的 Rocq(原 Coq)证明——如今看来那正是形式化数学浪潮的开端。
「研究」频道最新
- NBER 研究:AI 投资自 2018 年后带来企业生产率增长 — TaniaBabina · 2026-09-06
- GNN 作者 Kipf:智能是缩小生成-验证差距的过程 — tkipf · 2026-09-06
- 模型爱乱改别人代码,CROCODIL 后训练框架可抑制过度编辑 — omarsar0 · 2026-09-06
- 阿德莱德大学 MIP:裸编码 agent 零样本导航,R2R-CE 成功率 78% — jiqizhixin · 2026-09-06
- 临床试验拖慢反馈回路，AI 制药能力被系统性削弱 — clarejtbirch · 2026-09-06
- GPT-6 上线即打满 RuneBench，基准作者转攻更难的群体协作任务 — SchoeneggerPhil · 2026-09-06