加载失败
这篇讨论来自 Timothy Gowers（Fields medal 获奖数学家）在个人博客上的长文，起因是他用 ChatGPT 5.5 Pro（OpenAI 的高推理订阅模型）做数学研究后，觉得模型已经能产出接近可发表的结果。原文一边肯定 LLM 能快速扫文献、拼接已有证明技巧，一边强调它们会在概念层面犯错，因此需要专家反复校验。评论把焦点扩展到 Gemini（Google 的 LLM）、Claude Opus（Anthropic 的高端模型）、Lean（交互式定理证明器）、RAG（检索增强生成）和 CritPt benchmark（面向研究级 physics problems 的评测）等工具。讨论进一步延伸到 PhD 训练、学术预算、地区定价，以及谁有资格使用这些高端工具。
很多评论把当前 LLM 描述成“高效学生”或“强力实习生”：它们能在大段文本里抓出漏掉的符号错误，也能提醒人忽略的概念连接。可一旦进入概念层面，它们就会沿着错误模型继续跑，比如把 3D Clifford algebra 里的 bivector 和 pseudoscalar 搞混，或者在代码里抱着错误假设继续堆东西。大家普遍认为，模型最有价值的用法不是盲信，而是由懂行的人先设定预期，再用测试、反例和追问把它逼回正轨。换句话说，LLM 更像极速但不稳的助手，不像能独立负责的研究者。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6] [来源7] [来源8] [来源9] [来源10]
原文里最让人不安的一点，是“温和题目”可能不再适合作为 PhD 训练起点，因为 LLM 已经能把这些低门槛研究题先做掉。评论认为这会抬高真正进入研究的门槛：学生不能只会读现成证明，而必须自己经历推导、犯错、修正，才能理解问题本身。有人强调，亲自解题和只是看别人或机器的证明是两回事，后者往往只会把人变成转发器，前者才会积累可迁移的研究能力。围绕“人和 AI 共同完成的成果算不算人的重大成就”，意见也分裂：有人只看结果价值，有人坚持学术文化仍然看重人的主导性。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6] [来源7] [来源8] [来源9] [来源10] [来源11] [来源12]
评论区大量讨论模型订阅费和 API 费用对学术界的实际可达性。有人指出，$200/月 的 Pro 套餐对东欧助理教授、很多公共大学，甚至不少美国普通家庭都不是小数目；再叠加软件采购红带、Copilot 绑定和 grant 规则，获取研究级模型就更难。也有人反驳说，如果 AI 真能显著提升产出，它的成本应该和薪资、办公室空间这些大开销一起算，而不是只盯着月费。可这场争论本身就暴露了不均等：真正能稳定用上高端模型的人，本来就不是同一个阶层，学校的“有 AI”公告也未必等于真的有能力。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6] [来源7] [来源8] [来源9] [来源10] [来源11] [来源12] [来源13] [来源14] [来源15] [来源16] [来源17] [来源18] [来源19] [来源20]
不少人反对把 LLM 使用过程称为“mentoring”，因为这会让人误以为模型真的会成长。评论更倾向于把它看成一种短期联想更新：模型能在当前上下文里形成新关联，但这种“学习”很脆弱，像 anterograde amnesia 一样不耐久。于是实务上就出现了 RAG、skills.md、手工提示词和“工程师笔记本”这种外部记忆层，把知识放在模型外而不是幻想模型自己长记性。这个方向的共识是：真正可用的系统，靠的不是模型内化了多少知识，而是外部工作流把它约束成什么样子。
另一条线是把这件事上升到 AGI / ASI 的层面，觉得模型已经展现出一种“jagged intelligence”：能解 frontier math，却又会在很简单的问题上出错。也有人说，这更像是强自动化，而不是持续扩张人类知识边界的系统。更感伤的评论担心，如果论文、突破和名声都能被 AI 参与甚至主导，人类做研究的“永恒价值”会变淡，读博的意义也会被重写。与此同时，也有人用体育、赛车和机器人类比，认为社会未必只奖励最底层的技术贡献，仍会继续为人类选手和人类操作者喝彩。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6] [来源7] [来源8] [来源9] [来源10]
有一支更技术化的讨论聚焦在 formal proof 上。有人提到，过去 LLM 在 Lean 里不太可靠，但现在像 Codex 这样的工具已经能在 write/compile/fix-first-error 的循环里，很快把模块 formalize 出来。这个方向的意义不只是“会写自然语言证明”，而是能把数学变成机器可检查的对象，因此在可验证性上更接近真正可落地的研究工作。它也说明，模型在不同任务上的能力差异很大：写文章、写 proof、形式化证明，结果并不一样。
Lean: 一种交互式 theorem prover，用于把数学证明形式化并由机器检查。
CritPt benchmark: 面向未公开、研究级 physics problems 的评测基准，用来观察 frontier models 在高难科研题上的进展。
regional pricing: 按地区定价的策略，会根据不同国家或地区的购买力调整订阅价格。
RAG: Retrieval-Augmented Generation，先检索外部资料再生成回答的架构，常用于补充最新知识或外部记忆。