数学家：AI 可代写引理证明，但投 arXiv 必须附完整 Lean 形式化
LucaAmb · x · 2026-11-05
数学家 Scott Armstrong 提出对当前 AI 数学工具的实践观点与出版规范主张：
- AI 的合理用途：在 PDE 等存在超长技术证明的领域，让 AI 把「有说服力的证明提纲」扩写成完整（但可能是 slop 的）证明是很好的用法。逐条打磨引理是艰苦工作，2026 年还让人类手工做这些「计算器式」工作很愚蠢。
- 但前提是形式化：如果要在 arXiv 上传 100+ 页的半 slop vibe-tex 证明，必须附带完整的 Lean 形式化——现在做到这点太容易了，不做就是偷懒。
- 编辑立场：他担任编委的期刊若收到无 Lean 形式化的此类论文，可能直接退回并要求补交完整形式化后再投。
「研究」频道最新
- 开源人形机器人 BRIDGE：88cm 高 12.5kg 成本约 1500 美元 — philfung · 2026-11-05
- 生产环境 Agent 的第一套评测集：用失败工单还是真实对话抽样？ — rahulladumor · 2026-11-05
- Ninada 开源：21.7MB 浏览器内 TTS，覆盖梵语与 10 种印度语言 — init0 · 2026-11-05
- 牛津团队发布 TestBED：贝叶斯实验设计首个通用开源工具包 — tom_rainforth · 2026-11-05
- NVIDIA 研究发布 TAMPAgent：因子图让机器人零样本完成移动操作 — danfei_xu · 2026-11-05
- Harmonic 的 Aristotle 模型一键合成电路并附完整 Lean 证明 — satnam6502 · 2026-11-05