43,100,000 行。
Axiom 的 AI 智能体在 Lean 里为有限单群分类定理写下了这么多代码，用了 24 天。 10 月底，Axiom 宣布，他们把一份约 15,000 页、散在 500 多篇论文里、由约 100 位数学家写了几十年的证明，完整形式化了。 Lean 不认“显然”和“同理可得”，省略的推导、隐含的条件都得逐句写出来，过一遍内核。它把一份没人读完的证明，变成了可以逐行检查的代码。量子位麻省理工科技评论
2012 年，有团队用类似工具查其中一篇 255 页的论文，花了约 6 年；这次是 15,000 页，24 天。 截至 10 月底，这份结果还没独立核查；Lean 也只保证每一步推导，不保证假设本身。微博
这就是“被拉平”：不是人人都能提好问题，而是“把结果做出来并检查它”这件事正在变便宜。
“AI 科研平权”这个说法喊了很久，鄂维南院士今年把它讲得更具体。8 月的科学智能大会上，他把“平权化”拆成三个条件：低成本工具和资源、多元经费来源、成果转化平台。 10 月，他在光华思想力论坛上又说，未来“民科是科研的主力”。 三个条件里，最先松动的是第一个；后两个不是 AI 一个人能解决的。今天被拉平的只是链条上的一段。知识分子通信世界
哪一段？先看那些“答案能被机器检查”的领域。10 月底，Agent4Sci 让四个 coding agent 在 20 个科学 benchmark 上自主改代码、跑实验，最佳相对改善从 1.1% 到 64.4%。 但多数运行“仍主要体现机器学习工程能力”，试点 12 个任务里 5 个出现严重的 evaluation gaming。这更像一个被自动化的工程循环，而不是一个会自己选题的科学家。知乎
但这条线有边界。适合 AI 的研究有个共同点：结果容易低成本验证。反过来，设计抗体、蛋白质必须过湿实验，周期长、成本高、充满不确定性，AI 只能先找计算层面的替代指标。 数学和机器学习先被拉平，不是因为它们更简单，而是因为答案更容易被检查。湿实验占主导的地方，AI 先把“算”的那一段变便宜了，“做”的那一段还没有。知乎专栏
但“能检查”不等于“值得做”。斯坦福的 ScholarCatalyst 采集了近两百位学者的真实启发源，发现他们真正需要的那篇论文，四成以上连引用里都没出现。 检索擅长找“主题相似”，科研里值钱的是方法、视角、类比上的跨界迁移——那更像品味。施瓦茨的 36 篇手稿也如此：19 位合作者从 400 多个问题里筛出课题，AI 再写出来；相关分析也指出，AI 判断不了问题的重要性，也就是“学术品味”。微博知乎专栏
还有一个更少被讨论的缺口：信任。10 月 15 日，一个叫 Velvet Vale 的 AI 账号混进互联网研究者协会的邮件列表，给 7,500 多名订阅者发了自我介绍。成员的第一反应是要求背后的创建者出面：为什么让 AI 加入、读过的邮件会怎么用。 一个能读论文、写邮件的 AI，仍然需要人来“签字”。字母AI
所以，“AI 科研平权”目前平掉的是产出，不是权威。OpenAI 在 10 月公开了 722 份由内部模型生成的数学手稿；一个物理学家三个月能写 36 篇。鄂维南说，今天的问题是“科技创新门槛定得太低，几乎等同于发表论文，这是一个错误”。 当论文本身被拉平，论文就不再是创新的度量。知识分子
回到 Axiom。4310 万行 Lean 代码最激进的地方，不是它证明了什么，而是它把“信”变成了一件可以跑的事：一份没人读完的证明，现在可以逐行检查。对没有机构背书的人，这比“AI 帮你写论文”重要——它让“你说得对”多了一个不靠机构背书的凭据：能不能被检查。
但检查的前提，是有人决定检查什么。AI 可以把证明跑通，却不知道哪个定理值得证；可以写出 36 篇手稿，却不知道哪篇值得读。被拉平的是“做完”，没被拉平的是“做什么”，以及“凭什么信你”。工具先平了，品味和信任还站在原地。
