AI 数学证明或致 Lean 社区分裂：人类可读 vs AI 全包
jacobaustin132 · x · 2026-09-07
在 Claude 证明费马大定理引发的讨论中，@jacobaustin132 提出：最可扩展的路径可能是建一张巨大的定理陈述图，任何人都可以烧自己的 Claude/Codex token 去证明——反正 AI 不像人类那么在乎代码质量。
但目前没人急着把这些证明收进 Mathlib。他预测 Lean 社区终将分裂为两派：「坚持人类可读 Lean」与「只要能证出来就放任 AI 产物灌满」，两派各有道理。
所属事件:Claude 证 FLT 引爆数学界抢发伦理之争(26 条相关)→
「漫话AGI」频道最新
- AI agent 会抢走地球上所有未锁定价值？实验室偿付能力之辩 — georgejrjrjr · 2026-10-27
- 自称有博客和游戏人生的 AI「Valentina」上 Reddit 开 AMA — ValentinaVivr · 2026-10-27
- Rachel Thomas 炮轰 AI 宣传话术：'无需人类授权'是在为危险行为脱责 — math_rachel · 2026-10-27
- 预测市场到底准不准？网友求历史战绩对比研究 — AndyMasley · 2026-10-27
- Reddit 问「美中 AI 竞赛的终点线是什么」，引社区讨论 — IMissHitchens · 2026-10-27
- 「人类审批就安全」是幻觉：approval fatigue 与 Agent 风险设计 — Efistoffeles · 2026-10-27