悲伤，还是不悲伤？
AI 辅助定理证明的迅速进展，尤其是 Lean 和大型语言模型等工具，正在迫使数学家和软件工程师面对一个问题：当机器开始“解决”过去只属于人类专家的问题时，这意味着什么。评论者争论这究竟是哲学上的转变还是劳动危机，担心生计流失、权力与资本集中，以及以人为中心的创造性和智力工作被侵蚀。另一些人则认为，AI 终将只是另一种工具，改变数学与编程实践的性质，而不是消灭它们；社会如何回应——监管、资助优先级与劳动政策——将决定其影响是普遍有益，还是深度不平等。
AI 与数学
- 多条评论讨论 AI 加形式化证明助手（例如 Lean）如何成为数学中的变革力量：LLM 现在能够生成由机器验证的形式化证明。
- 这引出了存在性问题：如果“解决大问题”被自动化了，数学家的角色是什么？
- 有人认为真正的危机在于劳动，而不是哲学：证明曾是工作的“货币”；如果 AI 产出这些，招聘与资助信号就会失灵。
- 还有人认为，数学资助越来越来自对 AI 感兴趣的组织，这扭曲了激励，并边缘化了“真正的反对者”。
- 关于 AI 是否真的在解决“困难问题”仍有争论；有人担心相关说法被夸大。另一些顾虑包括：历史上曾促成新想法的人类探索性死胡同可能会消失。
悲伤、身份与意义
- “悲伤的五个阶段”这一类比被广泛用于描述数学家和程序员适应 AI 的过程；有些人明确自认处在“讨价还价”“抑郁”或“接受”阶段。
- 也有人完全拒绝这一模型，或嘲讽其被过度使用。
- 一个反复出现的主题是：如果发现与证明变得机械化，意义会随之丧失。有些人更看重做数学的人类过程与文化，而不是结果本身。
劳动、阶级与收益分配
- 许多评论强调 AI 是一个阶级/劳动问题：强大的技术出现在劳工力量削弱、资本集中和政治腐败的背景下。
- 担忧包括：自动化导致失业、压低工资，以及知识私有化。
- 有人主张禁止或延缓 AI 部署；也有人认为这不现实，而直接再分配（例如福利/UBI）更诚实，但在政治上更棘手。
能力、炒作与风险
- 对 AI 实际能力的看法分化：有人认为炒作过头、推理能力有限；也有人认为它显然强大到足以重塑劳动，必须按这个标准来对待。
- 关于“失控 AI”和意志的争论：有人说系统没有意志，只是任务驱动；另一些人指出，哪怕只是执行目标的优化器，也可能因冷漠而危险，尤其是在与人类行为者结合时。
- 环境成本和财富集中被视为反对 AI 的理由，哪怕“它是否真的有用”都无关紧要。
编程与人类创造力
- 程序员将 AI 描述为既令人不安又令人振奋：它能写出有用的代码，但常常又像低质量的“垃圾内容”。
- 有人预测会出现“人类编写代码”的细分市场，类似摄影之后的绘画；也有人认为，人类从来就没那么擅长管理复杂性，AI 工具最终会占主导。
- 人们担心对 AI 工具的广泛依赖会侵蚀技能，但也承认工具一直在改变实践方式。