最近海外技术社区有一类帖子特别火：**AI 不再只是帮科学家打下手，而是自己提假设、自己写代码、自己跑实验、自己写论文**。这件事在 Hacker News 和 Reddit 上吵出了三层楼：一派觉得“科学发现要加速了”，一派觉得“这是灌水流水线”，还有一派在默默把这套流程搬进自己的日常工作。本文拆解三场正在进行的争论——AI 自动科研靠不靠谱、数学家为什么先拥抱了形式化验证、以及海外正在推动的“AI 亮明身份”标准——每场都给你可操作的结论。 --- ## 话题一：AI 科学家上岗，是加速还是灌水？ ### 事情从哪来 东京初创公司 Sakana AI（创始人包括 Transformer 论文作者之一 Llion Jones）在 2024 年开源了「The AI Scientist」项目：给它一个研究方向，它会自动做文献综述、提想法、写实验代码、跑实验、写论文，据其官方博客声称单篇论文成本约 15 美元。2025 年初，Sakana 又宣布 AI 生成的论文首次通过了 ICLR 2025 一个 workshop 的盲审——这条新闻在 Hacker News 上直接爆了。 几乎同一时间，Google 在官方研究博客上发布了「AI co-scientist」，一个基于 Gemini 的多 Agent 系统，定位是科学家的协作助手。据 BBC 报道，帝国理工学院的研究者用它筛选肝纤维化的老药新用方案，实验室验证了部分候选药物确实有活性。 ### 社区怎么吵 **支持派**的观点很直接：科学最大的瓶颈是“想法到验证”太慢，Agent 能把假设-实验循环从几个月压到几天。一位 Hacker News 高赞评论的说法代表了这派人：“人类一天只能跑 10 组实验，Agent 一晚上跑 1000 组，哪怕 90% 是废的，剩下来也比人快。” **反对派**火力更猛。Reddit 上 r/MachineLearning 和 HN 的主流声音是： - AI 写的论文里存在编造引用、数据和结论对不上的情况，审稿人发现“AI 味”论文直接拒稿； - 自动化跑通≠科学发现，**没有人工复现的“发现”不配叫发现**； - 伯克利「A-Lab」自主材料实验室 2023 年在 Nature 发表成果后，多位材料学者公开质疑其部分合成结果——这场争论至今没完全落幕。 **中间派**最实用，他们的立场是：把 AI 科学家当成“不知疲倦的博士后”，它可以穷举、可以试错、可以写好所有粗活，但**最后一步必须人来验证**。Sakana 自己也承认这一点——他们提醒用户：这个系统会自主执行生成的代码，必须在沙箱环境里跑。 ### 这套流程长什么样 把各家方案抽象一下，自动科研 Agent 的核心循环其实是一样的： ```mermaid flowchart TD A[人类科学家定题] --> B[文献综述Agent] B --> C[生成候选假设] C --> D[设计实验方案] D --> E[执行Agent跑代码] E --> F[评估Agent核数据] F --> G{结果显著吗} G -->|不显著| C G -->|显著| H[撰写论文初稿] H --> I[审稿Agent挑刺] I --> J{过审吗} J -->|不过| H J -->|通过| K[人类最终复核] K --> L[投稿或归档] ``` ### 对中国技术从业者的启示 你不需要发论文才能用这套东西。**「AI co-scientist」模式可以直接改造成技术调研流水线**：三个角色——文献综述 Agent（读论文/读源码）、假设 Agent（提出 3 种技术方案）、验证 Agent（写 benchmark 跑数据）——用任何主流 Agent 框架都能拼出来。选型、调参、做技术预研的人，这就是你的“自动实验室”。唯一的铁律：**结论必须自己复现一遍才能信**。 --- ## 话题二：数学家先投降了？Lean + AI 的暗流 如果说“AI 做科研”还有争议，那数学圈发生的事更值得玩味：**最讲究严格证明的群体，反而最先接受了 AI 工具链**。 ### 陶哲轩带头的工作流革命 菲尔兹奖得主陶哲轩这两年一直在公开推动 Lean——一个开源的形式化证明语言（官网 lean-lang.org，代码在 github.com/leanprover/lean4）。所谓形式化，就是把数学证明写成编译器能逐行检查的代码：**证明对不对，不再由审稿人投票，而是由编译器说了算**。 2024 年他牵头的「等式理论项目」是个标志性事件：把一个原本估计要多年才能解决的猜想，拆成上万个小任务放在 Lean 里众包，配合自动搜索工具和 AI 辅助，据其博客描述几个月内就完成了主体证明。他在公开演讲里形容 AI 工具像一个“不太靠谱但肯干的研究生”——水平有限，但能替你干脏活累活。 ### 三种立场的碰撞 **加速派**：DeepMind 的 AlphaProof、Harmonic（Robinhood 联合创始人 Vlad Tenev 创办，主打“数学超级智能”Aristotle）等团队都在押注“AI 先过形式化这一关，再谈真正的研究”。他们的逻辑是：自然语言证明可以糊弄审稿人，但糊弄不了 Lean 编译器——**形式化验证是 AI 数学能力的照妖镜**。 **传统派**的担忧则是数学的“美感”会消失：证明过程变成机器生成的几万行验证代码，人类再也无法“读懂”数学。r/math 上这类讨论不少，核心一句话：“如果没人能理解证明，数学还是数学吗？” **工程派**最值得中国程序员关注，他们的观点是：**Lean 这套东西真正的用武之地根本不是数学研究，而是关键代码的形式化验证**。协议实现、加密算法、分布式一致性逻辑——这些“错了会出大事”的代码，可以用 Lean 给它们上“数学保险”。Lean 配套的定理库 mathlib（github.com/leanprover-community/mathlib）已经积累了海量已验证定理，而且有一个开源项目 Lean Copilot 专门用 AI 辅助补证明步骤。 ### 程序员的入门路径 ```mermaid flowchart TD A[装Lean4工具链] --> B[玩自然数游戏入门] B --> C[熟悉mathlib套路] C --> D[让AI把命题译成Lean] D --> E[AI补证明草稿] E --> F[编译器当裁判] F -->|报错| D F -->|全绿| G[沉淀为项目资产] ``` 这个方向在国内中文社区的教程密度极低，属于典型的**时间差信息差**：海外已经把它当工程实践讨论，国内搜索相关关键词几乎只有零星翻译稿。 --- ## 话题三：AI 该不该在网上“亮明身份”？ 第三场争论更冷门，但和出海的人直接相关：**网站怎么区分“好 AI”和“坏 AI”**。 现状是：AI 爬虫泛滥，Cloudflare 在 2025 年先后推出了 AI Labyrinth（用诱导页面消耗恶意爬虫算力）和 AI Crawl Control（站长可一键放行或封禁各家 AI 爬虫）。但“按 User-Agent 封禁”太容易伪造，所以 Cloudflare 正在 IETF 推一个叫 Web Bot Auth 的草案：**让爬虫用密码学签名自报家门**——你是 OpenAI 的爬虫？拿出签名证书来。据 Cloudflare 官方博客，多家 AI 厂商已参与讨论。 社区观点分三边： - **开放网络派**：这是好事，机器人亮身份，站长才有谈判筹码（放行换流量或收费）； - **隐私派**：密码学身份会把爬虫变成“实名制”，独立小爬虫和学术项目会被逼死，最后只剩大厂； - **务实派**：反正拦不住，不如标准化，至少日志里知道谁来的。 **对你意味着什么**：如果你做出海产品，现在就该去 Cloudflare 后台看一下 AI Crawl Control——决定哪些 AI 爬虫可以抓你（这是免费的获客渠道）还是全部拒绝（保护带宽和内容）。如果你的服务是给 Agent 调用的 API，Web Bot Auth 这类标准值得关注，未来“Agent 实名访问”可能成为风控标配。 --- ## 信息差总结 | 你以为的 | 别人已经知道的 | |---|---| | AI 做科研 = 编造论文的笑话 | 开源项目已能全流程自动跑实验，15 美元一篇；但社区共识是：不人工复现 = 不算数 | | 形式化验证是数学家的玩具 | 陶哲轩们用它加速真研究，程序员可以用它给关键代码上“数学保险”，中文教程还是空白 | | 反爬虫就是封 User-Agent | 海外在推爬虫密码学亮身份（Web Bot Auth），好 bot 坏 bot 分开管，出海站长有新开关 | ## 行动指南 1. **本周花 2 小时**：安装 Lean4（VSCode 插件一键装），玩 Natural Number Game 入门游戏，感受“编译器判你对错”的体验； 2. **花 10 美元做实验**：克隆 github.com/SakanaAI/AI-Scientist，**务必在 Docker 沙箱里**跑一个最小模板，亲眼看看 AI 科学家的工作全过程； 3. **10 分钟检查**：登录 Cloudflare 后台，看 AI Crawl Control 里过去 30 天有哪些 AI 爬虫抓过你的站，决定放行名单； 4. **改造你的预研流程**：把“综述 Agent → 方案 Agent → 验证 Agent”三角色 prompt 用到下一次技术选型上，人工只做最后裁决。 **延伸思考**：这三场争论其实指向同一个问题——当“生成”变得几乎免费，“验证”就成了新的稀缺资源。Lean 是验证数学，复现是验证科学，签名身份是验证流量。未来两年最值钱的技能，可能不是让 AI 干活，而是**判断 AI 干的活哪些能信**。 ## 参考来源 1. Sakana AI「The AI Scientist」开源仓库：https://github.com/SakanaAI/AI-Scientist 2. Lean 官网与 Lean4 仓库：https://lean-lang.org / https://github.com/leanprover/lean4 3. Google Research 官方博客（AI co-scientist）：https://research.google/blog 4. Cloudflare 官方博客（AI Crawl Control / Web Bot Auth）：https://blog.cloudflare.com 5. Hacker News 与 Reddit r/MachineLearning 相关讨论：https://news.ycombinator.com --- > 本文由「51学通信」技术团队出品。51学通信由通信行业18年老兵**爱卫生**（微信ID: gprshome201101）维护。 > 聚焦5G/6G核心网、3GPP标准、AI工具实战。知识星球「51学通信」提供深度技术答疑和行业洞察。 > [!tip] 51学通信知识星球 > **星主：爱卫生**（微信：gprshome201101）——公众号「51学通信」创办者，19 年通信行业运维与讲师经验，著有《GPRS网络信令实例详解》《EPC原理与实践》《5G核心网原理与实践》三本纸质书（各大电商平台有售）。 > **星球定位**：深耕 5G 核心网、IMS、NFV/AI、云原生等 ICT 领域，主打运维岗位与信令分析。 > **当前规模**：5200 篇主题 / 990 个回答，198 元/年。 > **加入福利**：加入星球后请加爱卫生微信，拉您进知识星球年度陪伴与答疑群——不限量回复您的各种问题，另有群内分享。 > **AI 加持**：51学通信知识星球已作为 skill 接入 WorkBuddy，使用 deepseek-4-flash 在海量星球帖子中精准找贴、找视频、找 FAQ 和案例，做总结、找文档和 PPT 等场景全覆盖。