福建
我打赌你想不到，全球最顶尖的数学家之一，会用GitHub Copilot写代码。
不是偶尔用用。是每天用。是把AI当成研究搭档，天天一起干活的那种用法。
这个人叫陶哲轩（Terence Tao），菲尔兹奖得主——数学界的诺贝尔奖。2024年9月，他干了一件事，让整个数学界和AI圈同时炸了锅：他发起一个项目，要在48小时内解决2200万个数学难题。
结果呢？他做到了。
01 一个十几年前的预言，正在兑现 
AI负责写草稿，验证系统负责检查，人类负责突破——三层协作的未来图景
2012年左右，陶哲轩说过一句话（大意）：AI未来会成为数学研究的可信合作者。当时大多数人听了，礼貌性地点点头，心里想的是"等你真能证明一个定理再说"。
2024年7月，Google DeepMind的AlphaProof和AlphaGeometry 2在国际数学奥林匹克竞赛（IMO）上拿到了银牌水平——比预期提前了十几年。
两个月后，陶哲轩自己下场了。
他发起了"Equational Theories Project"（等式理论项目），目标听起来很学术：研究4694条代数等式之间的逻辑关系。但你把它翻译成人话就懂了——4694条等式，每两条之间都有可能互相推导，总共有超过2200万种可能的组合关系。
靠人力？算到退休也算不完。
02 48小时，2200万个问题
陶哲轩的设计精妙在哪儿？他把整个任务拆成了三个角色：
AI负责写证明草稿。你给它一个问题，它噼里啪啦给你写出一个"看起来像证明"的东西。
Lean形式化验证系统负责检查对错。AI写的证明到底对不对？不是靠人眼看，是靠一个严格的数学验证系统逐行检查。对就是对，错就是错，没有"差不多"。
全球志愿者社区负责攻克具体难题。有些问题AI搞不定，就发到社区里，让全世界的数学爱好者一起上。
结果呢？项目启动48小时后，陶哲轩在日志里写了一句话："这个项目的进展速度远远超出我的预期——才48小时，大部分问题就快要解决了。"
19天后，项目完成度达到了99.9963%。超过817万条关系被证明为"真"，超过1385万条被证明为"假"，只剩下826条还是未知的。GitHub仓库收到了1763次代码提交。
一个12年前的预言，用19天兑现了。
03 这不只是数学的故事
说实话，陶哲轩做这件事的意义，远远超出了数学本身。
他的核心洞察是：有一类项目，天然适合"AI+人类+验证系统"的三层协作模式。这类项目的特征是——由大量独立的小问题组成，每个问题不难理解，但加在一起人力根本做不完。
翻译一下：你公司里是不是也有这种活？
比如审核一万份合同里的风险条款。比如检查十万行代码里的安全漏洞。比如分析一千篇用户反馈里的情感倾向。
每个单独看都不难，但"多"本身就是一个不可能的任务。
陶哲轩的模式给出了一条路：让AI先干粗活，用一个严格的质量检查系统（不一定非得是Lean，可以是自动化测试、人工抽检）来兜底，然后把人的时间花在最有价值的判断上。
关键不是"AI能不能干"，是"你怎么设计这个系统"。
2025年11月，陶哲轩又跟Google DeepMind合作，用他们的AlphaEvolve工具（一个基于大语言模型的进化编码智能体）一口气解决了67个数学难题。他把这叫"大规模数学探索与发现"。
到2026年6月，他宣布了第三届SAIR竞赛——"反伽罗瓦挑战"。模式跟等式理论项目一模一样：大规模、众包、形式化验证。只不过这次用的是MAGMA而不是Lean。
模式已经变成模板了。
04 陶哲轩自己怎么用AI的？
这一点特别有意思。
陶哲轩在GitHub上公开了他的项目日志。他写了一句话："我发现GitHub Copilot在日常工作中非常有用——把新的Lean定理写进去，或者更新蓝图来纳入最新的结果。"
注意，他不是说"AI帮我证明了定理"。他说的是"AI帮我干了那些无聊但必须干的活"。
这是AI最被低估的用法。大多数人要么把AI当搜索引擎使（"帮我查个东西"），要么期待AI一步到位出完美结果（"帮我写个方案"）。但真正高效的人，是把AI放在"加速器"的位置上——我不需要你有多聪明，我需要你帮我把重复劳动的时间从3小时压到10分钟。
陶哲轩还特别提到了AI的一个致命弱点：它会"胡说八道"。AI生成的数学证明，看起来像那么回事，但逻辑可能完全是错的。这就是为什么Lean这样的验证系统是必不可少的——你不能信任AI的输出，但你可以信任一个形式化验证系统的判断。
换句话说：AI是笔，验证系统是尺，人是拿笔和尺的设计师。
05 给所有知识工作者的启示
你可能不是数学家。你可能一辈子都不会用Lean。但陶哲轩的项目给了一个信号：
真正的"AI替代焦虑"搞反了方向。问题不是"AI会不会取代我"，而是"我能不能设计出一个AI替我干活的系统"。
这两者之间的差距，是指数级的。
第一种人，坐在工位上等AI来抢饭碗。第二种人，主动把AI拉进自己的工作流里，让它处理那些消耗时间但不消耗脑力的部分。
陶哲轩是第二种人。他12年前就看明白了这件事，然后用了12年时间一步步走到今天。
2024年的等式理论项目证明了一件事：当人类、AI和质量验证系统各司其职的时候，产出可以快到连发起者自己都觉得"疯狂"。
所以，下次你花3个小时整理数据的时候，问自己一个问题：这个任务里，哪些步骤可以交给AI，哪些步骤必须我自己把关，哪些步骤需要一个自动化的质量检查？
把这三个问题想清楚，你就已经走上了陶哲轩的路。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
