OpenAI、分割原理与数学

对数学家与“AI 垃圾”的负担

• 许多人把几百个部分难以理解的 AI 生成证明的堆积，视为对专家的拒绝服务攻击：少数具备相应技能的人被淹没在这些产物中，而社会与职业上又被迫去评估它们。
• 也有人认为“没人被强迫”去读这些内容；批评者则回应说，资助、宣传，以及来自同事/学生的持续询问，使得在实践中不参与的代价很高。

有效性与 Lean 形式化

• 一方主张，与目标问题形式陈述相匹配、且经 Lean 验证的证明，属于最可靠的数学成果之一。
• 反方指出了具体失败：一个利用 Lean 内核漏洞的 Collatz“反证”，以及带有符号错误而被撤回的结果。形式化验证、规格和代码都可能出错或不匹配。
• 有几位认为阅读 Lean 的命题是可行的，但证明对象非常庞大，实际上不可读。

可读性、表述与数学的本质

• 一个核心抱怨是：这些论文不清楚、结构怪异、引用也很差；如果是人写的，很多会直接被编辑部拒稿。
• 数学家强调，数学不只是“真理加证书”；阐述、新方法，以及与既有理论的整合，都是科学工作的核心。
• 也有人回应说，许多人类论文同样糟糕，而一个真实但难看的证明仍然有价值，只是没有一个可理解的证明那么有价值。

OpenAI 的动机与发布策略

• 支持者把这次发布描述为科学开放性和评估工具；任何感兴趣的人都可以在这些结果上继续推进。
• 批评者主要把它看作公关噱头：用开放问题来营销能力，忽视建议委员会的意见（例如关于署名、失败率以及改进表述）。
• 有人称这一过程带有剥削性：需要社区劳动来解读和清理这些结果，而主要受益的是公司本身。另一些人也担心，AI 输出会与用户提交但未公开的工作高度相似。

对职业与激励机制的影响

• 研究者强调机会成本和残酷的就业市场：花在解读 AI 产物上的时间，未必有助于职业发展，尤其对学生和无终身教职学者而言。
• 也有人把这些新结果和引理看作“自助餐”，认为雄心勃勃的数学家可以借此提炼、扩展并改进。

AI 时代数学的未来

• 爱好者感到兴奋：他们指出，已有社区项目在改进 AI 生成的界限，设想自动化的形式证明仓库，并期待未来模型能生成“令人愉快的证明”。
• 怀疑者担心“意义的丧失”：人类被降格为调试或翻译外星式证明，学科重心转向验证黑箱结果，而不是发展共享理解。