继费马大定理后，社区用 Lean 4 形式化 2012 篇运筹学论文，已完成 64%
ChrSzegedy · x · 2026-10-30
Prove2Me 团队在用 Claude agent 完成《费马大定理》的完整 Lean 形式化之后，尝试把同一方法扩展到整个研究领域，首选运筹学（OR）。
- 过去一个月，社区已开始用 Lean 4 形式化 2012 篇 OR 论文与教材，组织为 4288 个「任务」（mission），共包含 4.4 万条定理陈述与定义、880 万行 Lean 代码，覆盖优化、MDP、排队论、库存、博弈论等方向，社区贡献者已解决 64% 的任务。
- 增长来自复用：60% 的任务复用了早期任务中证明过的定理或定义，目标是构建一个共享的公共库，而非数千个孤立的 Lean 文件。
- 配图是 Formalpedia 的 OR 形式化图谱（2026-10-24）：33353 条定理、11146 条定义，按线性规划、凸优化、随机规划、排队与网络、博弈与机制设计等主题可视化为森林状结构。
- 背景补充：Anthropic 此前公布，研究者 Tianyi Peng 让 Claude 在 11 天内基本自主写出首个费马大定理的端到端机器验证证明，写了 1300 万行 Lean、证明 2.95 万个中间命题。
「研究」频道最新
- arXiv 论文：Self-Directed Repair 让 Agent 从错误中持续学习 — rohanpaul_ai · 2026-10-30
- 把纠错存成 LoRA：Self-Direction 让 Agent GAIA 成功率 38.8%→55.8% — rohanpaul_ai · 2026-10-30
- UCSF 论文：AlphaGenome 系统性低估因果变异效应，细定位表现不及线性基线 — anshulkundaje · 2026-10-30
- NeurIPS 2026 论文数排行：一人挂名 22 篇引作者署名之争 — qberthet · 2026-10-30
- 斯坦福 I3L 让全身机器人部署成功率平均提升 68.3 个百分点 — jiajunwu_cs · 2026-10-30
- 三个模型互相辩论投票找答案，作者踩坑后改用外部裁判判收敛 — lluisantoni · 2026-10-30