数学的黑夜
AI 在定理证明和形式化验证方面的快速进展让许多数学家感到不安，因为他们认为自己这门学科的核心部分——为证明而挣扎、发现反例、以及靠原创成果谋生——正在被自动化。评论者争论这究竟是人类“精神性前沿”的损失，还是又一次把苦差事卸给机器的技术进步，并将其类比到编程、航空和其他被自动化重塑的手艺之中。其背后是更广泛的焦虑：在一个知识工作本身可能被彻底改变的未来里，社会究竟应该多么重视以人为中心的创造，而不是单纯的实用价值。
情绪反应与身份危机
- 许多评论者对这种失落感深有共鸣：AI 似乎抹去了发现的“英雄式”体验，把数学家变成了旁观者或评论员。
- 另一些人认为作者确实处于强烈痛苦之中，并呼吁同情；也有人觉得这种语气过于戏剧化，甚至“过于情绪化”。
- 还有人报告自己在编程中也有类似感受：他们热爱的是亲手做这门手艺，而不是监督一个模型，并且觉得某些非常有意义的东西正在被剥夺。
过程 vs 产出：AI 是否偷走了乐趣？
- 一派观点认为：乐趣在于挣扎、洞见与创造；如果 AI 做了最有趣的部分，人类的参与就会变得空洞，像是在用“无敌作弊码”。
- 反对一派则说：工具一直在自动化那些枯燥的部分；AI 让人跳过苦差事，专注于自己真正喜欢的内容。你仍然可以把数学当作爱好来“手算”。
- 几位评论者指出，享受感往往取决于社会认可和经济支持，而不只是个人口味。
经济、价值与数学的资助
- 有一条很强的观点线认为：你不是为了开心而被付钱；你是因为创造价值而被付钱（通常是教学、争取资助，或下游应用）。如果 AI 在这些方面做得更好，资金就会转移。
- 反驳意见是：社会应当资助美、好奇心和“无用”的研究；许多基础数学在当初并没有明确的“客户价值”。
- 也有人强调，许多数学家主要是因教学而获得报酬，而不是因为每一个新定理本身。
民主化、可及性与新能力
- 乐观者看到的是数学的“黎明”：AI 助手帮助形式化证明、探索庞大空间、连接不同领域，并让非专家也能提出深刻问题。
- 另一些人指出，AI بالفعل 已经能够生成反例以及 Lean/Isabelle 证明，但人类仍然需要选择问题、解释结果并赋予意义。
- 人们担心封闭的专有系统，并呼吁类似 FOSS 的“自由且开源的数学”：记录 AI 辅助的证明路径，而不只是最终定理。
与其他领域及历史先例的比较
- 常见类比包括：程序员、战斗机飞行员、外科医生、棋手、工匠与工业机器、僧侣与印刷术。
- 有些人认为每一门手艺都经历过这一过程；也有人说 AI 在性质上不同，因为它自动化的是洞见，而不只是体力劳动。
存在性与社会性担忧
- 一些人进一步扩大了担忧：所有知识工作者都面临过时；基于能力和工作的身份认同可能崩塌。
- 观点分裂在乌托邦式的“富足世界，拥有更多时间做数学”和反乌托邦式的“少数精英 + 在经济上无用的大多数”之间。
- 少数人淡化了影响，认为当前 AI 研究成果仍然有限且被过度炒作；也有人援引目标快速变化，认为这正是应当认真对待这种冲击的理由。