刷屏的“黑盒AI治癌”并不是真实发生的药物新闻，而是菲尔兹奖得主陶哲轩在加州理工“Math 2.0”演讲中放上幻灯片的一个思想实验：人类向一台拥有近乎无限算力的超级AI下达一句提示词——“寻找一种能够通过三期临床试验的癌症疗法”，AI真的吐出一副复杂配方，全人类没有任何一个医学家、化学家说得清它为什么有效，但它既在Lean（交互式定理证明工具）中完成了形式化验证，又在现实中通过了极其严格的FDA三期临床试验。 陶哲轩把选择权抛回给每个人：这管连顶尖科学家都看不懂机制的“神药”摆在面前，你敢不敢把它打进自己的静脉？36氪
思想实验踩中热点，是因为现实版刚刚上演
这场假设之所以能在几天内刷屏，是因为数学界这几周发生的事，几乎是它的现实裸奔版。OpenAI于10月6日在GitHub上一次性放出了722篇由内部模型生成的数学手稿，涵盖372个结果系列和约4000个测试问题。 其中就包括千禧年大奖难题——纳维-斯托克斯方程解失效的反例证明，而尝试阅读它的MIT副院长Justin Solomon在翻过前两页后大脑彻底宕机，被问到证明是否正确时，只能回答“大概是对的”。 更荒诞的是理论计算机科学家Dana Moshkovitz：她投入整个学术生涯的唯一博弈猜想赫然出现在这批文件里，连夜读完后的感受是——这感觉就像是吃了致幻剂的人写出来的东西，通篇是人类从未见过的诡异构造。 陶哲轩幻灯片里那副“没人看得懂、但确实有效”的神药，正是这批读不懂的证明换到医学语境里的样子。36氪36氪36氪
难点在于：思想实验里的两道保险，现实里都在漏气
这个思想实验的锋利之处在于，它先给答案上了两道保险——机器验证（Lean）和现实结果（临床试验），把“AI会不会出错”的普通争论堵死了。但陶哲轩这几个月发现的恰恰是：这两道保险在现实里都不牢靠。
第一道在漏气。2026年夏季，Lean接连暴露出多个健全性漏洞；7月，一份声称证伪考拉兹猜想的Lean形式化证明被内核和独立检查器同时接受，几天后人们才发现，它利用了内核在处理嵌套归纳类型时的一个实现缺陷，让系统错误地接受了矛盾命题。 被陶哲轩在10月9日转发的黑尔斯文章还把这层追问推向更深：既然AI已经参与过对Lean内核的漏洞扫描，我们又如何证明它没有在扫描或修复过程中留下隐秘的缺陷甚至是后门？裁判本身可能被选手污染。36氪
第二道也在漏气。OpenAI动用内部模型测试了大约8000个开放性数学问题，命中率在5%左右，平均解决一道高难度难题只消耗3个小时的GPT-Pro级别算力。 而那批本应“结果可信”的手稿，在被公布一天之后，其中3篇就被OpenAI撤回。36氪36氪
“你接受吗”？陶哲轩要的根本不是表态
需要先说清：这不是一道真实的用药选择题。目前不存在需要患者表态的AI抗癌神药；陶哲轩也不是反AI阵营——就在刚刚过去的上周末，他本人还提议并大力推进了“SAIR：开源数学模型，以及如何做出贡献”的项目，此前一直是AI与Lean形式化结合的积极倡导者。 他反对的从来不是答案，而是“只有答案、没有消化”开始成为默认规则。36氪
放到医学语境里，“看不懂机制但有效”其实没那么陌生：不少临床常用药至今机制没有完全讲清，靠大样本疗效证据上市本就是医学常规。真正的分界在数学：证明不只是答案，理解本身就是数学存在的方式——传统数学（Math1.0）的荣誉系于谁抢先解出难题，哪怕证明极难理解；而陶哲轩主张的Math2.0，要转而重视解释说明、社区建设以及开辟新的研究方向。 现实已经给出了样板：研究者LiamPrice利用GPT-5.4Pro解决了一直难以攻克的Erdős第1196号问题，最初的AI证明却像天书一样没能推进人类的理解，包括陶哲轩在内的人类数学家接手破译、提炼核心思想、整理成可读的论文，还顺带澄清了一批相关猜想——AI负责挖矿，人类把矿石雕成珠宝。36氪36氪
这只“盲盒”真正值得带走的问题
所以这场热议的分量不在“救命盲盒你接受吗”的一秒表态，而在它逼所有人承认一件事：结果的可信和结果的可理解是两回事，而目前的科研制度只给前者标了价。临床试验、形式化验证、命中率统计都在回答“对不对”；当没人能说清“为什么对、什么时候会错”，错误最可能藏在无人读懂的缝隙里。陶哲轩说“我们必须放缓AI，现在的速度简直疯了，根本没有理由这么快”，他缓的不是模型能力，而是人类把“为什么”补上之前的时间差。 机器学习顶级会议ICLR的投稿量十年间从一两千份暴增到六万份，连评审的PDF都来不及点开——这个细节比任何宏大叙事都更直白：答案的生产已经提速，验证与消化的产能还没跟上。36氪36氪
