多伦多大学数学教授 Daniel Litt 最近写了篇文章，直指一个正在象牙塔深处蔓延的隐秘危机：定理证明的自动化正在摧毁学术界两百年来的度量衡。三年前的大模型甚至做不好加法，如今却在奥数金牌与前沿难题边缘频频叩门；但如果一台机器能吐出几百万行无懈可击的代码，却没有任何人类看得懂其中的几何或代数洞察，这到底算不算数学的进步？
证明可以由算力批量制造，但人类的理解不能被外包。
战报与现实：千禧难题的真水准
围绕 AI 解题的公关喧嚣，学界与科技巨头之间其实隔着一层很厚的认知温差。
2024 年，Google DeepMind 旗下的 AlphaProof 与 AlphaGeometry 2 拿到国际数学奥林匹克竞赛（IMO）银牌水平（28/42分），但当时部分题目需要耗费多达 2 至 3 天算力，且赛题必须由人类专家手工翻译成 Lean 形式化语言。到了 2025 年，DeepMind 的 Gemini Deep Think 经协调员官方评分拿下 35/42分，解出 6 题中的 5 题，跨过了金牌线；OpenAI 同样公布其内部模型摸到了 35/42分。作为对照，2026 年官方 IMO 的人类金牌线为 29/42分。
但在真正的科研战场上，两家机构的路线与态度开始分道扬镳。
2026 年 2 月 11 日，DeepMind 宣布其数学智能体 Aletheia 测试了约 700 个 Erdős 猜想，成功解决其中 4 个，但团队极为克制，公开发文强调这些成果仅属于 Level 0–2 级别，并未触及重大进展。
反观 OpenAI，步子迈得极为激进。2026 年 2 月 20 日，其针对 10 个未发表问题发布 First Proof 成果，旋即承认第 2 题被证实错误，仅声称至少 5 个解答具有较高正确率；5 月 20 日，OpenAI 宣布推翻 Erdős 单位距离猜想；9 月 8 日更声称攻克了千禧年大奖难题之一的 Navier–Stokes 方程光滑性问题，并提交了形式化验证代码。克雷数学研究所（CMI）虽然承认该问题“显然已被处理”，但至今仍把课题保持在 Active 状态，强调必须经过严格漫长的同行评议程序。
商业机构急于树立通用人工智能的旗帜，学界看到的却是提示词脆弱性与庞大算力的堆叠。
形式化有效性与人类理解的断裂
数学家焦虑的根源，不在于 AI 会不会解题，而在于逻辑的有效性与人类的理解正在分道扬镳。
以往数学界默认产出文本就等于掌握了思想。一个学者能证明定理，意味着他参透了背后的结构。但在交互式定理证明器 Lean 介入后，这层对应关系被切断了。机器可以从公理出发暴力展开数亿步符号推演，生成一段完全正确却长达数万行的代码。
这在逻辑上毫无破绽，但对人类认知几乎是噪音。如果一段证明无法提供可复用的概念工具，不能解释为什么这种构造有效，那它在智识层面的价值极其有限。数学史从来不是定理清单的简单累加，而是概念网络的逐步织造。从微积分到代数几何，人类前行的每一步都在追求简化与顿悟，而非纯粹的穷举。
一旦只要充值算力就能砸出答案，数学就从最便宜的纯粹智力活动，变成了资本密集型的工业推演。
象牙塔度量衡瘫痪后的重塑
当生成一篇符合顶级期刊要求的推演文本只需几百美元算力时，现行的高校评价体制首当其冲。
长期以来，数学博士毕业、教职评聘、期刊同行评议，全部锚定在论文和证明主定理上。现在这一基石正在松动：一个甚至没通读全文的研究生，借由辅助模型也能攒出一篇技术指标达标的博士论文。纸面文本正在丧失作为学者学术水准的信噪比。
与其固守日渐失效的审稿流程，不如直面制度演进的必然。Daniel Litt 提出的自救方案很纯粹：放弃把论文数量作为唯一硬通货，转而考核口头答辩与即时研讨。
- 建议.毕业与招聘重心转向深度的现场考核，要求候选人脱离模型直接阐明概念机制，应对未知算例的临场迁移。
- 风险.若任由闭源大模型垄断未决猜想的算力解释权，公立学术机构将逐步丧失对数学前沿审美与问题定义权的掌控。
学术评价被迫回归黑板前的对话。古希腊学园里的论辩、导师办公室里的推导敲打、以及研讨课上持续追问直到所有人扫清疑惑，这些曾被量化发表挤压的社交与认知过程，反倒成了抵御机器泡沫的最后防线。
AI 可以不知疲倦地证明定理，但挑选哪些问题值得研究、为哪种理论赋予美感，决定权依旧在人。机器越是擅长提供现成答案，人类就越要退回到最本质的那个动作：坐下来，把事情真正想明白。