AI 形式化能力突飞猛进，Lean 却开始撞墙
davidad · x · 2026-09-04
研究员 davidad 转引 @AcerFur 的实践观察：AI 形式化数学的能力看不到上限，但作为载体的 Lean 证明助手可能开始成为瓶颈。具体案例中，将数值计算部分形式化会在 Lean 里产生 100+ GB 的数值数据，把作者的笔记本塞满，最后只能选择将其作为公理绕过。这提示 AI 自动形式化的产出规模正在超出现有证明基础设施的承载能力。
「研究」频道最新
- 开源项目 Marin 启动 535B/A23B MoE 训练,一年内从 1 人扩到 10 人 — wandb · 2026-09-04
- 研究称让 AI 造 App 的环境成本可达快速提问的 1 万倍 — shiringhaffary · 2026-09-04
- SpeedrunBench：首个测 AI 智能体速通游戏能力的基准，最优模型距人类纪录差 4 倍 — mariyaivasileva · 2026-09-04
- Foresight 推出新 RFP:最高 10 万美元资助开源 AI 科学与安全项目 — niloofar_mire · 2026-09-04
- 研究者用 Lean4 机器验证解决 Chrisnata et al 开放问题 — _xjdr · 2026-09-04
- NeurIPS 悉尼几秒内门票售罄,距录用放榜还有三周 — alrojo · 2026-09-04