Prove2Me 用 Claude 智能体形式化 2000+ 运筹学论文，已完成 64%
ChrSzegedy · x · 2026-10-30
- Prove2Me 社区在过去一个月里为运筹学领域的 2012 篇论文与教材建立 Lean 4 形式化任务，拆成 4288 个 mission，含 4.4 万条定理/定义与 880 万行 Lean 代码，覆盖优化、MDP、排队论、库存、博弈论等方向，社区贡献者已解决 64%。
- 形式化统一存放在一张共享图谱中：每项结果可复用，新的形式化成本随图谱增长递减；过程中还发现了已发表结果的更简证明和自然推广。
- 此前该社区曾让 Claude 智能体形式化费马大定理。团队希望运筹学最终实现「投稿前先形式化」，并计划扩展到理论计算机科学、量子物理等领域，研究者只需让 agent「去 Prove2Me 形式化这篇论文」。
所属事件:社区用 Claude 智能体形式化 2012 篇运筹学论文，进度达 64%(2 条相关)→
「编程与Agent」频道最新
- Agent 身份安全创企 Mintive 融资 1100 万美元，日调用超 250 万次 — dunkhippo33 · 2026-10-30
- Cartesia 语音 Agent 实测：AI 牙科前台自然应对打断对话 — haider1 · 2026-10-30
- 开源 korea-data-mcp：修复 agent 读韩国公共数据的 47 个陷阱 — youngtipted · 2026-10-30
- 作者自述：一年前手写代码成了 FrontierCS 2 第三难任务 — wzenus · 2026-10-30
- 三个开源 LLM 投票筛文献：15034 条记录自动评审出 489 项研究 — maier_ak · 2026-10-30
- 资深从业者：把心思花在 eval 上，训练自然容易 — yunta_tsai · 2026-10-30