数学照妖镜：AI 能发现新的数学定理吗？

snowboat 2026-05-07 60.9 KB 11.4K 16 𝕏 文章列表

文章回顾了人工智能与数学证明的深厚渊源，从1950年代的Logic Theorist到哥德尔不完备性定理，探讨了形式化数学的演进。重点介绍了现代AI数学的基础设施LEAN（包括其核心人物Leonardo de Moura、从v3到v4的演进及mathlib库），以及DeepMind、Harmonic、Axiom Math等科技巨头和初创公司在AI自动定理证明领域的布局。文章指出，AI正在通过神经网络与形式化验证的结合，重新回归逻辑推理的起点。

AI 数学证明 LEAN DeepMind 逻辑推理形式化验证 Axiom Math mathlib 科技史自动定理证明

# 数学照妖镜：AI 能发现新的数学定理吗？ **作者**: snowboat **日期**: 2026-05-06T23:49:51.000Z **来源**: [https://x.com/snowboat84/status/2052174034041995572](https://x.com/snowboat84/status/2052174034041995572) --- ![Image](/doc/1737/image/img_6877eb9ef978.jpg) 2025年底，数学圈出了一个很有传播性的故事。数论学家Ken Ono离开弗吉尼亚大学，加入硅谷AI初创公司Axiom Math。Ono做过美国数学会副主席，长期研究拉马努金和数论。按传统路径，他本来应该继续待在大学、研究所和讲台上。 Axiom Math由Carina Hong创办。Hong当时24岁，MIT数学和物理本科出身，后来进入斯坦福读博，又离开学校创业。她想做一个AI数学家：能解决数学难题，能生成证明，也能检查自己的推理是否正确。 ![Image](/doc/1737/image/img_d34f8ef46e68.jpg) 这也是这个故事最抓人的地方：一位资深数学家，加入了一位年轻创业者刚刚成立的AI数学公司。放在几年前，这样的组合很难想象。 Axiom的大目标，已经越过了让模型算题、写答案这一步。它要让AI学会做可靠的数学证明，把证明写进形式化系统里，让机器能检查每一步到底成立不成立。几个月后，资本市场也投了票。2026年3月，Axiom拿到2亿美元A轮融资，估值约16亿美元。一个刚成立不久的AI数学公司，靠“数学证明”讲出了独角兽故事。最近几年，AI在语言和图像、视频上都有了重大的突破。但是在数学上，AI的表现如何呢？数学不像写文案、画图、做视频。一个证明要么对，要么错。错一步，后面再漂亮也没用。数学给AI提供了一把很硬的尺子。如果AI只能写出“看起来像证明”的文字，那它离真正的数学还很远。只有当它能在这把尺子下面站住，我们才有资格继续追问更大的问题。所以问题来了：AI能不能发现新的数学定理？它是在做更快的计算器，还是已经开始碰到人类创造知识的边界？ # 一、AI 一开始就是从数学证明里长出来的 ## 1.1 第一个 AI 程序就在证明定理很多人以为AI是最近几年才开始碰数学，其实刚好反过来。AI这个学科最早的代表作品之一，干的就是数学证明。故事要从1950年代的RAND公司讲起。那时候还没有“人工智能”这个正式学科。有三个学者在RAND凑到了一起：Allen Newell研究组织和决策，Herbert Simon研究人怎样在有限信息下做选择，Cliff Shaw负责把这些想法写成真正能跑的程序。 ![Image](/doc/1737/image/img_e0ca128c0eba.jpg) Aritificial Intelligence pioneers Allen Newell (right) and Herbert Simon Newell和Simon关心的问题很直接：人类解决问题的时候，到底在做什么？如果一个人能一步步推理、排除、搜索、试错，那么机器能不能也这么做？他们挑的第一个靶子，是罗素和怀特海的《数学原理》。三卷本的《数学原理》是20世纪数学基础研究里最有名的著作之一，试图把数学建立在形式逻辑之上。书里的命题写得非常严格，对机器来说正好合适：规则清楚，目标明确，每一步能不能走下去都可以检查。 1955年底到1956年初，Logic Theorist的雏形做出来了。最有意思的是，最早的版本并不是直接在电脑上跑出来的。Simon后来回忆，他们把程序步骤写在卡片上，让家人和研究生分别扮演程序里的不同部件，像一台“人肉计算机”一样模拟程序运行。这听起来很原始，但它抓住了AI最早的核心想法：智能可以被拆成符号、规则和搜索。等Shaw把程序真正搬到RAND的计算机上之后，Logic Theorist开始证明《数学原理》第二章里的定理。它最后证明了前52个定理中的38个。一个亮点是，有些证明比原书还短。 ![Image](/doc/1737/image/img_f9d74419a889.jpg) 1956年夏天，Dartmouth会议召开，“Artificial Intelligence”这个词在那里被正式推上台面。Newell和Simon带着Logic Theorist去参会。别人还在讨论机器智能应该是什么样子，他们已经拿出了一个会证明定理的程序。所以AI从诞生第一天起，目标就不只是模仿人类输出。它一开始想做的，就是逻辑推理，就是数学证明，就是让机器进入人类最硬的智力活动之一。 ## 1.2 希尔伯特的梦被打碎，但工具留下了再往上追，故事会回到希尔伯特。 20世纪初，数学家已经拥有了微积分、集合论、非欧几何、抽象代数，工具越来越强，地基却越来越让人不安。集合论里出现了悖论，几何不再只有欧几里得一种，分析学也刚刚经历严格化。数学家突然意识到：我们每天都在证明定理，但“证明”本身到底有多可靠？希尔伯特的回答很硬。他希望把整个数学变成一套可以机械检查的符号系统。所有概念先清楚定义，所有推理都按规则展开，只要给出一个命题，原则上就能判断它是真的、假的，还是能不能从公理里推出来。这就是后来所谓的希尔伯特纲领。它有两个核心愿望：第一，数学不能自相矛盾；第二，数学证明应该能被有限、明确、可检查的规则管住。换句话说，数学不应该只靠大师的直觉和读者的信任，它应该像一台严密的机器。这个梦想非常诱人。它等于给数学找一张最终安全证书：只要公理系统是安全的，所有在里面推出的定理就都是安全的。罗素和怀特海写《数学原理》，也可以放在这条大线里理解。 ![Image](/doc/1737/image/img_2ad5410dcf28.jpg) 希尔伯特和哥德尔然后，1931年，哥德尔来了。哥德尔不完备定理把希尔伯特最乐观的部分打碎了。他证明，在任何足够强、足够一致的形式系统里，总会存在一些真命题，无法在这个系统内部被证明。更麻烦的是，这个系统也无法用自己的力量证明自己的一致性。这句话听起来抽象，意思却很重：数学不可能被完全压成一台万能判定机。你不能指望有一套终极规则，把所有数学命题都自动判定完。但希尔伯特的计划并没有完全白费。哥德尔打碎的是“全自动解决一切”的终极幻想，不是形式化本身。恰恰相反，形式逻辑、证明论、可计算性理论、类型论、自动定理证明，后来都从这条线长出来。它们承认数学不可能被彻底机械化，但仍然努力把能机械化的部分尽量机械化。 AI的早期几十年，尤其是所谓GOFAI，也就是Good Old-Fashioned AI，本质上大量依赖符号、规则、搜索和逻辑。Logic Theorist能出现，背后就有这条形式化传统。今天的工具LEAN、Coq、Isabelle，也是在这条路上继续往前走。 ## 1.3 从神经网络绕了一圈回到原点按照1950年代那批人的想法，AI本来应该沿着逻辑和证明一路往前走。机器会推理，会搜索，会证明定理，再往前一步，也许就能理解自然语言、规划行动、解决科学问题。现实没有这么顺。符号AI很快撞到墙。手写规则太脆，真实世界太乱，常识太多，例外也太多。一个小小的场景变化，就可能让精心写好的规则失效。到后来，符号AI给人的感觉越来越像一座漂亮但难维护的宫殿：逻辑上很干净，走出实验室就漏风。然后神经网络起来了。它走的是另一条路：少写规则，多喂数据。图像识别、语音识别、机器翻译、自然语言生成，都是这条路上打出来的胜仗。以前AI研究者想教机器“猫是什么”，现在直接给它看几千万张图。以前想手写语言规则，现在让模型从海量文本里自己学。这条路线太成功了，以至于很多人开始相信：智能不需要显式规则，只要模型够大、数据够多、训练够狠，它就能自己长出来。符号、逻辑、证明这些老词，突然显得又慢又土。但数学证明没有那么容易被绕开。你可以用神经网络写一段“很像证明”的文字，但数学不会因为它像就放行。证明需要每一步都成立，需要变量、定义、定理、前提条件全部对上。这里的麻烦，恰好是符号系统最擅长处理的东西。所以现在剧情又绕回来了，而且不是一个实验室在自嗨。 Google DeepMind在做AlphaProof，把AlphaGo、AlphaZero那套神经网络加搜索的思路，搬进形式化数学证明。Harmonic在做Aristotle，目标是让模型直接产出能被LEAN检查的证明。Axiom Math押的是另一条更商业化的线：如果未来AI会写大量代码和科学推理，那么数学证明就可以变成验证这些输出是否可靠的工具。这些项目的技术细节各不相同，但底层结构很像：用神经网络猜路，用强化学习和搜索扩大尝试范围，再用形式化系统验算。机器先提出可能的证明路径，LEAN这类系统负责一行行检查。猜错了就退回去，猜对了才算真正往前走。绕了70年，AI又回到Logic Theorist的出发点。区别在于，这一次它手里多了算力、数据、强化学习，还有LEAN这样的形式化地基。 ![Image](/doc/1737/image/img_9c131b3d8967.jpg) Credit: https://www.walfsun.com/post/gofai-the-origins-of-artificial-intelligence # 二、LEAN: 这场游戏的地基 ## 2.1 LEAN 是检查证明的机器要理解AI证明数学，先要理解LEAN。 LEAN本身是一个定理证明器，也可以理解成一种极其严格的数学编程语言。它不负责和你聊天，也不负责替你“发挥”。你在LEAN里写的是定义、命题和证明。普通数学证明写在纸上，靠同行阅读、审稿和学术共同体来判断对错。人类写证明时，经常会说“显然”“由标准结论可知”“不难推出”。这些话在论文里可以成立，因为读者默认作者和审稿人知道中间省略了什么。 LEAN不接受这种省略。你在LEAN里写一步，它就检查一步。变量类型对不对，前提条件有没有给齐，调用的定理能不能用，目标有没有真的被证明完，它都会检查。只要LEAN接受，这个证明就在它的公理系统和库依赖下成立。它不看文风，不看气势，也不看作者名气。所以你可以把LEAN想成数学世界里的编译器。写程序时，编译器不关心你觉得代码“应该能跑”。它只看语法、类型和规则。LEAN也是这样。你说“显然可得”没有用，除非你把“显然”的每一步都写清楚，或者调用库里已经证明过的定理。这就是LEAN和ChatGPT式数学输出的根本差别。ChatGPT可以写出一段很像证明的文字，读起来顺，但中间可能有坑。LEAN里的证明要么通过检查，要么报错。它把“像不像证明”变成了“是不是证明”。 ![Image](/doc/1737/image/img_8081b14734d7.jpg) ## 2.2 Leonardo de Moura 为什么要做 LEAN LEAN的核心人物是Leonardo de Moura。他是微软研究院的研究员，长期做自动推理和形式化验证。 ![Image](/doc/1737/image/img_7ae1e34def7d.jpg) Leonardo de Moura 他更早的代表作之一是Z3，微软研究院开发的SMT求解器。SMT求解器可以理解成一种自动逻辑工具，擅长在很多约束条件里判断是否存在解，广泛用在程序验证、硬件验证和软件工程里。但自动工具有一个问题：它们很强，也很黑箱。你把问题丢进去，它给你答案；可是一旦问题变得非常抽象、非常数学化，人还是需要参与构造证明。传统交互式证明器正好相反，人可以一步步写证明，但自动化又经常不够顺手。 LEAN想把这两边接起来。 2013年，de Moura在微软研究院启动LEAN项目。官方Reference里写得很清楚：LEAN的目标，是把一个很小、可以独立实现的可信逻辑内核，和SMT求解器这类自动化工具的便利性结合起来，同时能扩展到大问题。这句话翻成白话就是：底层要足够小，才能让人相信；上层要足够好用，数学家和程序员才愿意真的写东西。 2015年，de Moura、Soonho Kong、Jeremy Avigad、Floris van Doorn和Jakob von Raumer在CADE会议上发表了LEAN的系统论文。那篇论文把LEAN定义为一个开源定理证明器，使用基于依赖类型论的小型可信内核，目标是连接交互式证明和自动证明。 ![Image](/doc/1737/image/img_0d6d6e2a31a2.jpg) 这也是LEAN后来能长大的关键。它一开始就没有只想做一个学术玩具，而是想做一个平台：可以写数学，可以做软件验证，可以做教育，也可以让自动化工具嵌进来。 ## 2.3 从 LEAN 3 到 LEAN 4：从证明器变成语言 LEAN最早的版本更像研究原型。官方历史里写到，LEAN 0.1在2014年6月发布。早期版本主要以C++库的形式存在，让其他程序可以调用它来构造可检查的证明。后来，LEAN逐渐往传统交互式证明器演化，先有Lua写的tactic，再有专门的前端语法。 2017年1月，LEAN 3发布。对数学社区来说，这是一个关键节点。LEAN 3足够稳定，也足够可扩展，数学家开始认真拿它干活。更重要的是，它支持很强的自扩展能力：tactic、记号、顶层命令，都可以用LEAN自己定义。这听起来像语言设计细节，其实影响很大。数学不是一套固定格式。代数有代数的写法，拓扑有拓扑的写法，范畴论有范畴论的写法。如果一个证明器不能让社区自己扩展语言和工具，它很难承载现代数学的复杂表达。 LEAN 3的成功也带来一个问题：系统本身主要还是C++实现，扩展起来有成本。于是LEAN 4开始重写。 2018年，LEAN 4开发启动。2023年9月，LEAN 4.0正式发布。它是新版证明器，也是一门更完整的函数式编程语言。官方Reference里说，到了LEAN 4，大约90%的LEAN实现代码本身用LEAN写成，也就是所谓self-hosted。这里很容易误解。LEAN 4不是一个“把人类证明自动翻译成机器语言”的转换器。它更像一个数学证明的编程环境：你在里面定义对象，写下命题，再把证明写成一行行代码。LEAN 4负责检查这些证明代码是否真的成立。把自然语言证明翻译成LEAN代码，是另一个问题，叫autoformalization。比如论文里写“显然，由紧性可知存在有限子覆盖”，翻成LEAN时，你要说明空间类型、紧性的定义、开覆盖怎么表示、调用哪个已有定理。翻译完以后，LEAN 4还要继续检查它。这一步很重要。它意味着LEAN不再只是“检查数学证明的工具”，也变成了“写工具的工具”。用户可以更方便地做自定义语法、自动化tactic、领域专用工具。对AI证明数学来说，这一点尤其关键，因为AI不只需要一个判卷老师，还需要一个可以嵌入搜索、生成、反馈和自动化的环境。 ![Image](/doc/1737/image/img_5ed2d4b2443b.jpg) ## 2.4 mathlib 是 AI 数学的工具箱真正让LEAN变成AI数学基础设施的，是mathlib。 mathlib是LEAN社区维护的数学库。它的目标很朴素，也很疯狂：把尽可能多的现代数学，翻译成机器可检查的定义、定理和证明。一个证明器本身再漂亮，如果没有库，也很难做事。就像你写程序，不会每次都从零实现数组、哈希表、网络协议和文件系统。数学也是一样。你要证明一个数论命题，可能要用群、环、域、拓扑、分析、组合、序理论、范畴论里的很多旧结论。没有库，每一步都要从公理开始，根本走不远。 mathlib解决的就是这个问题。 ![Image](/doc/1737/image/img_afcfacb5997d.jpg) 它把代数、分析、拓扑、数论、组合、范畴论等大量数学内容，一条条翻译成LEAN可以检查的形式。这个工作非常慢，也非常苦。很多时候，一个人类论文里一句“由标准结论可知”，在LEAN里可能要展开成几十行甚至几百行代码。 LEAN 3时代，mathlib已经积累到超过100万行形式化数学。2023年，社区又把mathlib迁移到LEAN 4。官方Reference提到，迁移完成后，mathlib继续增长到超过150万行，而且LEAN 4检查更大的库，速度反而比LEAN 3检查较小的库更快。这不是一个小工程。它更像把数学世界一块块搬进机器能读的城市里。每搬进去一个定义、一个引理、一个定理，后面的人和AI就少走一步路。所以AI数学这轮变化，底层并不只是“模型突然变聪明”。它是两件事叠在一起：形式化社区先花多年修路，神经网络再用搜索和训练把这条路跑得更快。 ## 2.5 为什么 AI 最终会盯上 LEAN 现在再回头看，AI盯上LEAN并不奇怪。大语言模型擅长生成候选答案，但它最大的问题是不可验证。它可以写出一段语气很像数学家的证明，也可以一本正经写错。自然语言证明里有太多省略，普通读者甚至很难看出错在哪里。 LEAN给AI提供了一个罕见的训练环境。模型每写一步证明，LEAN都能给出干净反馈：通过，或者不通过。这个反馈非常适合搜索和强化学习。模型可以先猜一个证明步骤，LEAN检查；失败就换路，成功就继续。成功路径还能变成新的训练数据。这就是为什么DeepMind、Harmonic、Axiom这些玩家都绕不开LEAN和mathlib。DeepMind需要一个可验证的竞赛数学环境，Harmonic需要证明文件真正通过检查，Axiom需要把数学证明变成代码和科学推理的可信底座。换句话说，LEAN不是AI数学故事里的配角。它更像这场游戏的地基。没有它，模型只能生成“看起来像证明”的文字；有了它，AI才有机会把猜想、搜索和验证连成一个闭环。 # 三、现在的玩家已经不只是实验室 ## 3.1 DeepMind 把 IMO 变成公开靶场 2024年7月，Google DeepMind把这个方向推到大众视野里。它没有先去宣布“AI要解决黎曼猜想”，而是选了一个所有人都看得懂的靶场：国际数学奥林匹克竞赛，IMO。 ![Image](/doc/1737/image/img_38e5b05a634c.jpg) IMO有两个好处。第一，题目足够难，全世界最强中学生都在这里竞争。第二，规则很清楚，满分42分，6道题，每道7分，最后可以直接和人类选手比较。对AI来说，这是一个天然的公开benchmark。 DeepMind发布的系统叫AlphaProof和AlphaGeometry 2。前者主攻代数、数论这类可以走形式化证明路线的问题；后者主攻几何。两个系统合起来，在2024年IMO上解出6道题中的4道，总分28分，达到银牌上沿。那一年金牌线是29分，它离金牌只差1分。这件事真正刺激人的地方，不只是“AI会做奥数题”。更关键的是，AlphaProof走的是形式化证明路线。它把自然语言问题转成形式化表达，再用强化学习和搜索去找证明，最后让证明系统检查。DeepMind等于把AlphaGo、AlphaZero那套“神经网络加搜索加强化学习”的结构，搬到了数学证明里。这和普通模型写一段漂亮证明完全不同。普通模型可以胡说，AlphaProof要让机器验算。它做出来的东西，至少要在形式系统里站得住。但这里也要泼一盆冷水。IMO金牌级不等于研究级数学家。竞赛题是人为设计的封闭问题，条件清楚，目标明确，答案一定存在。研究级数学经常连正确问题是什么都不清楚，更不用说把它翻译成LEAN里的精确定义。真正的数学研究还需要选题、定义、品味、背景判断和长期的理论积累。 ## 3.2 Harmonic 和 Axiom 把数学证明做成公司 DeepMind的意义，是证明这条路能打公开比赛。Harmonic和Axiom的意义，是把这条路做成公司。先看Harmonic。 Harmonic由Tudor Achim和Robinhood联合创始人Vlad Tenev创办。它对外讲的词很大，叫Mathematical Superintelligence，数学超级智能。这个词当然有营销成分，但它背后的问题很具体：如果AI经常幻觉，能不能用数学证明把它按住？ ![Image](/doc/1737/image/img_4072db2fad84.jpg) Harmonic的核心产品叫Aristotle。到了2025年，Aristotle在IMO方向又往前走了一步。Harmonic官方披露，Aristotle在2025年IMO上达到金牌级表现，形式化解决了6道题中的5道，并开源了部分LEAN证明文件。它的技术报告里也明确说，只有系统产出完整的LEAN 4证明，而且没有sorryAx这类不可靠占位，才算真正解决。这个标准很硬。很多系统做数学题，是写出一个看起来合理的解答。Aristotle要交的是可以被LEAN检查的证明文件。一个占位符、一个没有补完的证明洞，都不能算数。资本也迅速跟上。Harmonic 2025年11月宣布完成1.2亿美元Series C，估值14.5亿美元。它已经是一家围绕“可验证数学推理”融资、招人、做API的AI公司。另一个明星公司是Axiom Math。Axiom由Carina Hong创办，2026年3月，Menlo Ventures宣布领投它2亿美元A轮，投后估值16亿美元。 Axiom的招人故事也很有传播性。Ken Ono，这位数论领域的知名数学家，离开弗吉尼亚大学的学术岗位加入Axiom，担任founding mathematician。一位资深数学家加入年轻创业者创办的AI数学公司，本身就足够抓眼球。 ![Image](/doc/1737/image/img_9c7cf2d6563c.jpg) 那Axiom到底做什么？它的目标不是做一个“会聊天的数学模型”，也不只是帮数学家证明几个漂亮定理。Axiom押的是Verified AI，也就是可验证的AI。它要让模型生成的东西，最后能被形式化证明检查。最直接的场景是代码。未来AI会写大量代码，但“能跑”“通过测试”“看起来没问题”都不等于安全。金融交易、加密协议、自动驾驶、医疗系统、AI基础设施里的代码，错一次代价可能很高。Axiom想做的，是让AI写出来的关键代码和关键推理，能够被数学证明验证：这个函数对所有输入都返回正确结果，这段逻辑不会破坏数据，这个系统不会引入某类安全漏洞。所以Axiom的商业叙事不是“数学家失业”。它更像是在给AI生成代码和AI推理加一层可信度。AI负责生产，Axiom负责证明这些输出真的符合规格。 Axiom自己也在做工具层。它公开的AXLE，也就是Axiom LEAN Engine，提供的是探索、验证、操作数学证明的交互式工具。你可以把它理解成Axiom内部训练和验证系统的一部分：模型生成证明，AXLE/LEAN这类工具负责检查、提取定理、操作证明对象。所以Harmonic和Axiom看起来都在做AI数学，侧重点并不一样。Harmonic更像从数学推理模型往外扩，Axiom更像从可信AI和代码验证往里打。它们共同说明一件事：数学证明已经从学术实验，变成了AI创业公司的核心叙事。 ## 3.3 钱开始流向基础设施，但研究级数学还很远与此同时，钱也开始进入基础设施层。这一点很重要。真正推动AI数学的，不会只有几家闭源公司。它还需要数据集、形式化库、autoformalization工具、LEAN教学、现代定理形式化项目。换句话说，它需要一整套公共基础设施。 XTX Markets和Renaissance Philanthropy就是这一层的代表。AI for Math Fund最初由XTX Markets支持，后来扩大到1800万美元，资助29个项目。2026年3月，Renaissance Philanthropy和XTX又宣布追加1350万美元，把总承诺提高到3150万美元。这些钱投向的东西很具体：形式化数学数据集，autoformalization工具，LEAN教学，把现代数学定理搬进形式化库。比如有项目要把顶级数学期刊里的现代定理形式化出来，有项目要做本科生证明的自动形式化和反馈工具。这里还必须提一个开源项目：LeanDojo。 ![Image](/doc/1737/image/img_091310f4df13.jpg) LeanDojo LeanDojo由Caltech、NVIDIA、MIT等机构的研究者在2023年推出，论文发表在NeurIPS 2023。它解决的是一个很工程、但很关键的问题：机器学习模型怎么和LEAN交互？如果每个团队都自己写一套抽取数据、运行证明、记录状态、评测结果的工具，这个领域很难复现，也很难积累。 LeanDojo做了两件底层工作。第一，它从LEAN和mathlib里抽取证明数据、proof state、tactic和premise信息，做成可以训练模型的数据。第二，它把LEAN变成一个类似gym的交互环境：模型可以看到当前证明状态，提交下一步tactic，LEAN返回成功、失败或新的子目标。它还提出了ReProver，一个带检索的证明模型。这个思路很自然：证明一个定理时，模型不能只靠自己背下来的参数，它还要从庞大的数学库里找可能用得上的旧定理。LeanDojo论文里构造了接近10万个来自mathlib的定理和证明，用来训练和评测这种检索增强的证明器。所以LeanDojo的意义，不在于它自己是不是最强的数学AI。它更像一个开放训练场，把“模型如何读LEAN、如何和LEAN互动、如何从mathlib里找工具”这件事标准化。后来的很多AI证明工作，都离不开这种基础设施。陶哲轩（Terence Tao）也在这个基金的顾问名单里，并多次公开谈到AI和LEAN对数学协作的潜力。他的态度很有代表性：AI短期内不是按一下按钮就吐出深定理的神机，更像一个能帮数学家查库、补引理、找边界、整理证明的协作工具。这说明AI数学已经过了“几个研究员做benchmark”的阶段。大厂、创业公司、VC、交易公司、慈善基金、数学家，都开始把它当成一条可能改变科研和软件工业的基础路线。 # 四、AI 到底怎么证明一个定理 ![Image](/doc/1737/image/img_c7c84b08e1b6.jpg) ## 4.1 AI 负责猜，LEAN 负责判 AI证明数学的核心结构，可以压成一句话：AI猜，LEAN判。想象你给系统一个命题：证明某个数论结论，或者证明某段代码满足某个规格。第一步是把目标放进LEAN这样的形式化环境里，而不是先写一段漂亮解释。系统要知道对象是什么，变量是什么，前提是什么，最后要证明的目标是什么。然后模型开始猜路。它读过大量数学材料和LEAN代码，学过命题怎么写、定义怎么展开、证明套路怎么走、tactic怎么用。面对一个新目标，它可能先生成一个证明步骤，也可能先拆出几个中间引理。比如先证明一个更小的等式，再把这个等式接回原目标。 LEAN做另一件事。它不负责灵感，不负责猜路，只负责验算。模型写出一行LEAN证明，LEAN检查这行是否成立。通过就进入下一个状态，不通过就报错。这就像一个人负责想下一步棋，另一个裁判负责判断这步棋合不合法。AI的价值在于提出候选路径，LEAN的价值在于保证每一步没有偷渡。 ## 4.2 它和 ChatGPT 写证明不是一回事这和普通ChatGPT写数学证明差别很大。 ChatGPT可以写出一段非常像人类论文的证明。它会说“由紧性可知”“显然存在”“不难推出”，读起来很顺。但只要中间某个“显然”其实不成立，整段文字就塌了。更麻烦的是，很多读者看不出来它塌在哪里。 LEAN不吃这一套。你不能用语气骗过它。一个变量类型不对，一个条件没传进去，一个定理适用范围不满足，它都会报错。AI在LEAN里写证明，等于每一步都要过安检。举一个很小的例子。人类论文里写“由紧性可知存在有限子覆盖”，读者大概能懂。但在LEAN里，这句话要变成一串明确操作：当前空间是什么类型，紧性定义调用哪一个，开覆盖如何表示，有限子覆盖是哪个对象，用哪个已有定理把它拿出来。如果其中一个对象类型不对，LEAN就不会让你往下走。它不会因为这句话“数学味很足”就放行。所以普通模型写证明，是在生成一段像证明的文本。AI加LEAN写证明，是在生成一段会被机器逐步检查的证明代码。这两件事差别很大。 ## 4.3 检索旧定理，生成下一步 tactic 真正的证明很少从零开始。数学家做证明，也会先想：这个问题像不像某个已知定理？有没有可以调用的引理？这个结构是不是应该用紧性、完备性、归纳法、同构、范畴论里的某个标准工具？ AI也要做类似的事。它不能只靠参数里“记住”的数学知识。mathlib太大了，定理太多了，很多时候关键不在于模型会不会写下一行，而在于它能不能找到该用哪一个旧定理。这就是LeanDojo和ReProver那类工作的意义。模型看到当前proof state以后，先从mathlib里检索可能有用的premise，再把这些候选定理和当前目标一起喂给模型，让它生成下一步tactic。 Tactic可以理解成LEAN里的证明动作。它可能是“用这个定理改写目标”，可能是“把目标拆成两个子目标”，可能是“对自然数做归纳”，也可能是“把某个条件交给自动化工具处理”。每走一步，LEAN都会返回新的proof state。于是证明过程变成一棵搜索树。一个目标可以往很多方向走，有些方向马上报错，有些方向走几步才死，有些方向能把目标拆小，最后一路走到所有子目标都被解决。 ## 4.4 强化学习吃到了干净反馈这个结构特别适合强化学习。因为LEAN给出的反馈非常干净：通过，或者不通过。没有“看起来还行”，没有“老师给你5分辛苦分”。模型可以在LEAN环境里反复尝试，把成功路径当成训练数据，把失败路径丢掉或修正。这也是为什么DeepMind那批做过AlphaGo、AlphaZero的人会扑向数学证明。围棋有一个规则明确的棋盘，走法对错和胜负可以被系统判定。形式化数学也有一个规则明确的符号世界，证明是否成立可以被LEAN判定。但数学比围棋麻烦得多。围棋棋盘有限，规则固定，目标就是赢。数学里的“下一步该引入什么定义”“该证明哪个引理”“这个问题应该放进哪个理论框架”，没有那么清楚。证明空间大得离谱，很多时候连搜索方向都需要人类数学直觉。所以现在的系统通常不会只靠模型一次生成完整证明。它更像是在一个形式化环境里反复试：生成若干候选tactic，LEAN检查，保留能推进的路径，失败的路径回退。搜索算法负责在许多候选路径之间分配计算资源，模型负责提出更可能有用的下一步。一旦某条路径最终通过，系统就得到一个干净样本：这条证明是真的。这个样本可以继续拿来训练模型。失败路径也有用，因为它告诉模型哪些操作不该在类似状态下使用。这就是AI证明数学吸引人的地方。它不像写文章那样很难判分，也不像很多科学实验那样反馈慢。形式化证明给了模型一个快速、明确、可重复的训练信号。 ## 4.5 Autoformalization 是最硬的瓶颈所以现在最难的瓶颈之一，是autoformalization。这个词指的是把人类自然语言写的数学，自动翻译成LEAN里的形式化表达。它包括两层：把命题翻译成LEAN里的精确定义，也把证明翻译成LEAN可以检查的步骤。 ![Image](/doc/1737/image/img_6dba5d5b5c6f.jpg) 它难在好几层。第一层是省略。比如论文里写“令X为紧Hausdorff空间”，LEAN需要知道你调用的是哪个拓扑结构、哪些实例、哪些已有定理。论文里写“由标准结论可知”，LEAN要知道这个标准结论到底是哪一个定理，前提条件是否满足，变量如何对应。人类数学家默认共享的大量背景，在机器眼里都要显式写出来。第二层是概念选择。同一个数学对象，可以用不同方式形式化。一个群作用、一个拓扑空间、一个范畴里的对象，放进LEAN时要选哪套定义？选错了，后面可能每一步都很难走。人类数学家会凭经验选择最顺的语言，机器现在还不稳定。第三层是库映射。自然语言里一句“用Hahn-Banach定理”，到了LEAN里不一定刚好有一个同名定理可以调用。库里的定理可能叫另一个名字，前提写法可能不同，结论形式也可能差一点。模型要找到能用的版本，还要补齐中间转换。第四层是证明重构。人类证明经常只写主线，把大量计算、边界条件和小引理留给读者。LEAN不会替你脑补。很多时候，原论文的一段证明，形式化时要拆成一串新的lemma，证明顺序也要重排。最难的一层是上下文。论文里的一个符号，可能依赖前面几十页的约定；一个“显然”，可能依赖作者所在领域的默认技巧；一个“标准构造”，可能根本没有写出来。autoformalization真正要处理的，是整篇论文背后的数学语境。如果autoformalization做通，AI数学会发生质变。过去一百年的论文、教材、讲义和证明，都可以更快进入机器可验证的世界。AI不再只是在mathlib里玩，它可以真正读懂数学文献的骨架。但这一步现在还远远没完全解决。自然语言数学太省略，库里的形式化表达又太精确。把它翻成LEAN，需要做的远超语言转换，更像是把一篇论文重新拆成定义、引理、依赖关系和可检查步骤。 # 五、VC 砸钱赌的不是黎曼猜想 ## 5.1 数学定理本身很难卖钱很多人看到Axiom、Harmonic的估值，会本能地问：证明数学定理怎么赚钱？答案很直接：很难靠数学定理本身赚钱。如果某家公司明天证明了黎曼猜想，数学界会震动，媒体会刷屏，公司会收获巨大声誉。但这不是一个清晰的商业模式。没有哪个客户会因为你证明了黎曼猜想，每年给你付几千万美元订阅费。数学定理的价值很奇怪。它一旦被证明，就属于全人类知识。你可以因为这个成果拿奖、拿名声、拿学术地位，也可能因此吸引人才和资本。但它不像SaaS账号，也不像API调用，很难按次收费、按席位收费、按年续费。这也是为什么Axiom和Harmonic虽然讲数学，但资本真正看的不会是“证明多少个漂亮定理”。漂亮定理是展示能力的舞台，商业化要落到另一个问题：这些证明能力能不能变成别人愿意长期付费的可靠性服务？换句话说，数学本身是招牌，验证才是产品。 ## 5.2 真正的市场在形式化代码验证 VC真正看上的，是形式化验证。 AI写代码已经变成巨大市场。Cursor、Claude Code、GitHub Copilot、OpenAI Codex这类工具正在把代码生产速度拉上去。问题是，AI写的代码经常有bug。有些bug只是页面错位，有些bug会变成安全漏洞、金融损失、自动驾驶事故或医疗系统错误。传统软件工程靠测试。测试可以覆盖很多情况，但它本质上是抽样。你测了1000个输入，也不能证明第1001个输入不会出事。形式化验证要解决的是另一类问题：在数学意义上证明这段程序满足某个规格。这里要把“测试”和“证明”的差别说清楚。测试是在问：我试过这些情况，它们都没坏。形式化验证是在问：在某个精确定义的范围内，这段程序对所有情况都满足规格。前者是经验保证，后者是数学保证。举个很小的例子。一个转账函数，测试可以检查100美元、0美元、负数输入、余额不足等很多case。形式化验证想证明的是：不管输入怎么变化，只要满足前提条件，总金额不会凭空增加，账户余额不会变成非法状态，权限条件不会被绕过。这就是Menlo Ventures投Axiom时讲的逻辑。Menlo的文章标题很直白：AI会写所有代码，数学会证明它能工作。它们押注的是一个未来：代码越来越多由AI生成，真正稀缺的东西变成“可信”。 Menlo文章里有一句判断很关键：AI生成代码看起来对，能编译，经常能跑，但这离“可证明正确”还很远。它们认为这类问题来自统计模型本身，很难靠下一个模型版本自动消失。Axiom要做的，就是把AI代码生成从“概率上靠谱”推进到“关键部分可以被数学证明”。金融系统、加密协议、航空航天、自动驾驶、医疗设备、基础设施软件，这些地方错一次代价很高。如果AI能把形式化验证成本降下来，真正的市场会来自所有需要高可靠软件的公司，数学家只是早期用户。 Harmonic也在往这个方向走。它2025年12月发布Aristotle在VERINA Code Verification Benchmark上的结果，声称解决了189个形式化规格中的183个，完成率96.8%。这类benchmark的目标已经从数学竞赛题转向了代码和规格的一致性验证。这说明数学证明能力正在外溢。先在IMO、Putnam、mathlib里证明自己能推理，再把同一套能力迁移到代码验证。真正的客户不一定关心群论、数论和拓扑，但他们关心一件事：AI写出来的关键代码，能不能放心上线。 ## 5.3 形式化验证过去为什么没火问题是，形式化验证不是新东西。它已经存在几十年，也确实有很多硬核成果。seL4微内核就是经典例子。它用形式化方法证明了操作系统内核的关键正确性和安全性质，被高安全系统反复引用。DARPA这些年也一直资助形式化方法，用在安全文档解析、系统建模、高保证软件等场景。如果这东西这么好，为什么过去没有大规模普及？原因也很直接：太贵、太慢、太难用。过去做形式化验证，往往需要懂软件工程、懂数学、懂逻辑、懂证明工具的人。这样的人本来就少，还贵。很多时候，写规格、写证明、维护证明的成本，甚至比写代码本身还高。Menlo那篇文章提到传统形式化验证市场很小，一个原因就是它常常需要博士级专家，甚至可能出现“每一行代码配很多行证明”的成本结构。工程团队也不喜欢这种工作方式。产品要上线，需求在变，代码在改。只要代码一改，证明可能也要跟着改。对大多数互联网业务来说，测试、监控、灰度、回滚已经够用了。它们宁愿承受一点线上bug，也不愿为数学意义上的正确付出巨大成本。所以形式化验证过去一直停留在高价值、高风险、强监管的地方。航空航天、军工、加密、操作系统内核、金融基础设施，这些地方值得做；普通业务系统大多不会做。 AI带来的变量，是成本结构可能变了。如果模型能自动写规格、自动补证明、自动修复证明失败的地方，形式化验证的门槛就会下降。过去需要顶级专家做几周的事，未来可能变成工程师点几次、模型跑一会儿、系统给出证明和反例。这正是Axiom、Harmonic这类公司最想讲的故事：形式化验证过去是少数专家手里的奢侈品，它们试图把它变成AI时代的软件基础设施。 ## 5.4 Agent 的信任层和估值泡沫还有一层更大的想象空间，是AI agent的信任层。未来如果agent能替你转账、下单、改数据库、部署代码、签合同，那么它每次行动前都需要某种可验证约束。它不能只是“我觉得这样没问题”，它要能证明这一步不违反规则。这就是数学证明技术可能商业化的地方。客户不在数学系，而在软件、金融、安全、机器人和AI平台。比如一个代码agent要改支付系统，它最好能证明自己没有改变金额守恒；一个数据库agent要批量迁移数据，它最好能证明关键字段不会丢；一个交易agent要执行策略，它最好能证明不会突破风控限制；一个机器人agent要操作物理设备，它最好能证明某些安全边界不会被越过。这时候，证明技术就不只是“检查代码对不对”。它变成agent行动前的护栏。agent越能做事，验证层越值钱。但我对这里的估值仍然保持怀疑。形式化验证过去几十年一直是好东西，但始终没有大规模普及。大家知道它严谨，真正卡住普及的是贵、慢、难用，以及对工程团队要求太高。AI可以降低门槛，但能不能降低到普通公司愿意买单，还没有答案。很多公司可能会选择另一条便宜路线：更强的模型，加更多测试，加灰度发布，加监控回滚。它们不一定愿意为了“数学意义上的正确”多付几十倍成本。只有当事故代价足够高，或者监管要求足够硬，形式化验证才会从高级玩具变成预算项。所以VC赌的不是“AI证明黎曼猜想后卖门票”。他们赌的是两件事。第一，AI生成代码和agent行动会变得越来越多，风险也会越来越大。第二，AI本身能把形式化验证的成本打下来。前者创造需求，后者降低供给成本。两件事同时成立，这个市场才会打开。如果只有前者，没有后者，形式化验证还是太贵。如果只有后者，没有足够高风险的应用，客户也不急着买单。这就是这条赛道最核心的商业不确定性。 ![Image](/doc/1737/image/img_d942a8f2642f.jpg) # 六、三年内能看到什么，别期待什么 ## 6.1 几乎确定：库会变大，工具会进日常未来三年，最确定的变化是mathlib会继续长大。这件事听起来不刺激，但它最稳。AI for Math Fund、LEAN FRO、Harmonic的捐赠和赞助、大学里的形式化项目，都会把更多现代数学搬进LEAN。代数、分析、数论、拓扑、范畴论里还会有更多定义、定理和证明被写成机器能检查的形式。这个过程很慢，但很扎实。每搬进去一块，AI能使用的工具箱就大一圈。今天模型卡住，可能只是因为某个旧定理还没进库，或者进库了但名字、形式、依赖关系很难找。三年后，这类低级摩擦会少很多。第二个确定变化，是autoformalization会明显进步。它未必能一键把论文变成LEAN证明，但会先在更窄的场景里变好。比如把教材里的标准定理形式化，把本科生证明题翻成LEAN，把论文里的局部lemma翻成机器可检查版本。这些小场景一旦跑顺，就会慢慢扩大到更复杂的论文片段。数学家也会越来越多地把AI当成日常工具。它不一定替你想出核心思想，但可以帮你查库、补lemma、验证边界条件、找反例、把一个证明草稿改成更严谨的形式。陶哲轩谈AI时更偏向这个方向：AI像一个能协作的初级助手，而不是按一下按钮就给出深theorem的神机。这种工具进入日常以后，数学家的工作方式会变。以前你要花一天查一个库里有没有某个lemma，以后可能几分钟就能问出来。以前一个证明草稿有一堆边界条件，AI可以先帮你试着形式化，告诉你哪里少了前提。它像一个不知疲倦的研究助理，水平未必最高，但能不断试错。高端软件验证也大概率会起量。金融、加密、航空、自动驾驶、医疗设备和AI基础设施里，会有一批客户愿意为更强保证付费。Axiom、Harmonic这类公司如果能先在这里落地，估值故事就不只是故事。但这里的落地不会是全行业铺开。更可能先从小模块开始，比如关键函数、加密协议、智能合约、风控规则、数据库迁移脚本、agent行动约束。先证明最危险的局部，再慢慢扩大。 ## 6.2 可能发生：中等难度开放问题被 AI 补上比较可能发生的标志性事件，是AI在某个具体子领域里解决一个有学术分量的开放问题。这个问题大概率不会是黎曼猜想那种全人类盯了一百多年的超级难题，而是某个边界清晰、可以形式化、已有大量工具可用的中等难度问题。这类问题有几个特征。背景已经比较成熟，相关定义和定理大多能形式化；问题本身边界清楚，不需要发明全新的语言；证明可能需要大量搜索、拆case、组合已有工具。人类数学家能看出方向，但细节太多，或者某个关键连接长期没人撞上。 Axiom声称已经在类似方向上拿到过结果，Harmonic也在宣传它解决过未解Erdos问题的形式化版本。哪怕对这些宣传保持谨慎，也能看出方向：AI最先可能补上的，是那些“理论框架已有、证明空间巨大、需要大量试错”的问题。这类事件一旦发生，媒体标题一定会写成“AI击败数学家”。真实情况会复杂得多。很可能是人类提出问题、整理背景、搭好LEAN环境，AI在其中补上关键证明或大规模搜索。它仍然值得重视，但不等于数学家失业。更准确的说法，可能是“AI参与解决了一个开放问题”。人类负责选题、建模、解释结果、检查数学意义；AI负责在形式化空间里跑大量搜索，找到人类没有及时发现的连接。 ## 6.3 别期待：黎曼猜想级别还没到时候三年内基本别期待AI解决黎曼猜想、P vs NP、Navier-Stokes这种级别的问题。这些问题难在需要新的概念、新的语言、新的理论框架，单纯加算力和数据很难解决。人类数学史上真正的大突破，往往不靠把旧工具用得更快，而靠发明新的看法。AI现在更像一个极强的证明搜索和形式化工具，还不像一个能独立发明新数学语言的研究者。超级难题还有一个现实问题：它们周围的形式化基础不一定够。你要让AI解决黎曼猜想，不只是把一句“证明黎曼猜想”丢给模型。你需要把相关的解析数论、复分析、谱理论、代数几何或者其他可能路线，尽量放进可用的形式化环境里。这个地基本身就是巨大工程。而且超级难题通常需要新的结构，单纯长计算不够。人类历史上的大定理，很多时候靠的是换一张地图，旧路加速只能解决一部分问题。AI能不能发明这种地图，现在还没有证据。所以三年内更现实的边界是：AI在已有理论框架里变得很强，在形式化证明搜索里变得很强，在局部引理和中等问题上越来越有用。但“独立发明新数学语言、解决最顶级难题”，还不是当前最该下注的预期。 ## 6.4 公司结局：大厂收购会比数学突破更早公司层面倒是很可能出现大额并购。OpenAI、Google、Anthropic、微软、Meta这类公司都需要更强推理和验证能力。对它们来说，几十亿美元收购一个顶级形式化推理团队，不是离谱剧本。原因很简单。大模型公司都在往agent、coding、科研、企业自动化走。模型越能行动，越需要验证。谁能把“模型输出”变成“可检查输出”，谁就能在高价值场景里多卖一层信任。所以Axiom、Harmonic这类公司，未必一定要先证明世界级数学难题，才有商业价值。只要它们证明自己能稳定生成可验证代码、可验证推理、可验证agent约束，就已经足够让大厂动心。但并购不是技术成功的证明。它只说明大厂相信这条能力不能缺席。另一个可能发生的局面，是生态分化。闭源公司做大模型和高端客户，开源社区继续建设LEAN、mathlib、LeanDojo、autoformalization工具。最后真正推动行业的，可能会是闭源模型、开源库、数学家社区和企业验证需求一起往前推。所以未来三年，我会把预期放在三个层级：基础设施一定会变厚，数学家日常工具会变好，高风险软件验证会开始试水。至于AI独立成为研究级数学家，时间表还要往后放。 ![Image](/doc/1737/image/img_6f8e5154f22b.jpg) # 七、数学是 AI 的照妖镜 ## 7.1 数学的规则比艺术硬得多回到开头的Axiom故事，一个资深数论学家离开大学，加入一家年轻AI数学公司。这件事真正有意思的地方，不只是“老教授去了创业公司”，也不只是“2亿美元融资”。它说明AI终于走到一个很难糊弄的场景里。过去几年，AI在艺术、写作、图片、视频上给人的冲击很大。但这些领域有一个共同特点：标准比较软。你说这张图好，我可以说它不够高级；你说一段文案普通，我可以说它适合转化；你说一段视频怪，我可以说这是风格。数学不吃这一套。一个证明要么成立，要么不成立。一个LEAN证明通过了，就是通过了。没通过，再像论文也没有用。数学不给模型留“语气很自信”“看起来很合理”“大概差不多”的空间。这就是AI证明数学最迷人的地方。它不靠情绪，不靠风格，不靠“像不像”。它逼AI面对一个硬问题：你到底会不会推理？ ## 7.2 数学家不会被一键替代所以我不认为AI三年内会变成高斯、欧拉，也不认为数学家会被一键替代。数学家的工作并不只是把一段证明从A推到B。真正难的地方，经常在证明之前：提出好问题，选择好定义，判断一个方向有没有价值，决定该在哪个理论框架里看这个问题。很多时候，一个定义选错了，后面证明再努力也会很难走。 AI现在更像一个很强的加速器。它可以帮你查mathlib，补lemma，验证边界条件，找反例，把一个证明草稿改成更严谨的形式。它尤其擅长吃掉那些枯燥、细碎、可验证、需要大量试错的部分。这已经足够大了。如果过去一个数学家要花几周把一个证明形式化，以后可能只需要几小时或几天。如果过去一个研究生要反复查库、试tactic、补小引理，以后AI可以承担大部分机械劳动。数学家的时间会更多地花在上游：问题、结构、定义、路线和解释。换句话说，数学家不会立刻消失，但数学家的工作流会变。越靠近“机械化证明劳动”的部分，越容易被AI吃掉；越靠近“提出什么问题、为什么值得做、用什么语言看它”的部分，越仍然需要人。 ## 7.3 AI 终于遇到不能糊弄的考试从Logic Theorist到AlphaProof，从希尔伯特的形式化梦想，到今天的LEAN和mathlib，AI绕了一大圈又回到原点。区别在于，这一次它不再只拿着手写规则和小搜索树，而是带着神经网络、强化学习、海量数据和真正可验证的数学库。这条路最后能走多远，现在没人知道。黎曼猜想可能还很远，研究级数学也不会被一夜之间自动化。可至少有一件事已经发生：AI终于开始接受一种它无法靠话术混过去的考试。这个考试的结果，会反过来影响很多领域。如果AI能在数学里学会“可验证推理”，它就不只是在数学里有用。代码验证、科学推理、agent安全、金融风控、机器人控制，都需要类似能力。模型不能只给一个看起来合理的答案，还要能给出可以检查的理由。这也是为什么VC愿意给Axiom、Harmonic这种公司高估值。资本当然会讲故事，也会制造泡沫。但泡沫背后有一个真实问题：当AI开始写代码、做决策、操作系统，人类需要某种硬验证机制。数学证明是目前最硬的一种。所以这篇文章的问题，不能只理解成“AI能不能发现新定理”。更准确地说，它在问：AI能不能从生成漂亮答案，走向生成可信答案？如果答案是能，那数学只是第一块试金石。如果答案是不能，那数学会成为AI能力边界最诚实的照妖镜。 ![Image](/doc/1737/image/img_c2001273a1b5.jpg) ## 作者其它文章 - 手把手教你分析：你会被AI取代吗? - 一篇文章讲清大语言模型发展史 - 气吞万里如虎：回顾十九世纪的数学英豪们 - Vibe Reading：AI 时代读书的系统化方法 - 长篇分析：Manus 案折射出的中国 AI 创业生态 - 别再被 AI 新词绕晕了：Prompt、Context、Agent 背后的工程主线 - 两万字科普：AI 为什么会编程——原理、历史与未来 - 兄弟们，真·Vibe Writing 时代到来了 - 全网最详细的AI学习路线图 - 每个人都应该使用的三个最有用的 Claude Skill - SpaceX 立志传（一）：赌上全部的最后一次发射 - 估值290亿美元的套壳公司，正在被自己的房东杀死 - 黄仁勋和主持人吵红了脸：芯片封锁中国，美国到底能不能打赢？ - AI将如何颠覆教育，普通人又应该如何抢夺教育新的生态位 - 学物理的八方英雄们，物理学已死，请转行搞AI - 不会编程、没有融资、没有员工，他怎么一个人做到年入2000万 - 兄弟们想清楚：究竟是你为X打工，还是X为你打工？ - 一人公司盈利四亿美元：是骗子，还是可复制的红利？ - 2026第一季度大裁员，AI是背锅侠吗？ - 重返星辰大海：这次绕月飞行有意义吗？ - 张雪峰在美国为什么无法成功 - 2026 企业尸检报告：不用AI，你的公司能活过今年吗？ - 兄弟们，我创业失败了，人生完整了 ## 本文参考文献 - Logic Theorist - Wikipedia - LEAN Language Reference: History - LEAN官方Reference - The LEAN Theorem Prover - Microsoft Research - LEAN 4 Theorem Prover and Programming Language - Microsoft Research - Mathlib: A Foundation for Formal Mathematics Research and Verification - LEAN官方Mathlib介绍 - AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind - Harmonic About - Harmonic - Aristotle: IMO-level Automated Theorem Proving - Harmonic - Harmonic's IMO 2025 Results - GitHub - Announcing Our Series C Funding - Harmonic - AI Will Write All the Code. Mathematics Will Prove It Works. - Menlo Ventures - Axiom Math Funding Round - Gaebler / VentureDeal - Axiom - Axiom Math - Ken Ono - University of Virginia - The Math Legend Who Just Left Academia-for an AI Startup Run by a 24-Year-Old - Wall Street Journal - AI For Math Fund Announces $18 Million In Grants - Renaissance Philanthropy - AI for Math Fund - Renaissance Philanthropy - Renaissance Philanthropy and XTX Markets Launch New $9 million AI for Math Fund - Renaissance Philanthropy - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models - NeurIPS 2023 - LeanDojo-v2: AI-Assisted Theorem Proving in LEAN - LeanDojo - Is Math the Next AI Frontier? A Conversation with Terence Tao - Renaissance Philanthropy - Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark - Harmonic - Axiom LEAN Engine - Axiom Math - The job description is changing: mathematician Terence Tao on the rise of AI - Nature ## 相关链接 - [snowboat](https://x.com/snowboat84) - [@snowboat84](https://x.com/snowboat84) - [264](https://x.com/snowboat84/status/2052174034041995572/analytics) - [https://www.walfsun.com/post/gofai-the-origins-of-artificial-intelligence](https://www.walfsun.com/post/gofai-the-origins-of-artificial-intelligence) - [手把手教你分析：你会被AI取代吗?](https://x.com/snowboat84/status/2051818364507688978) - [一篇文章讲清大语言模型发展史](https://x.com/snowboat84/status/2051444935547912236) - [气吞万里如虎：回顾十九世纪的数学英豪们](https://x.com/snowboat84/status/2050371067278143931) - [Vibe Reading：AI 时代读书的系统化方法](https://x.com/snowboat84/status/2050008577511973253) - [长篇分析：Manus 案折射出的中国 AI 创业生态](https://x.com/snowboat84/status/2049643679804248305) - [别再被 AI 新词绕晕了：Prompt、Context、Agent 背后的工程主线](https://x.com/snowboat84/status/2049286033427349809) - [两万字科普：AI 为什么会编程——原理、历史与未来](https://x.com/snowboat84/status/2048919554882215954) - [兄弟们，真·Vibe Writing 时代到来了](https://x.com/snowboat84/status/2047828585537548574) - [全网最详细的AI学习路线图](https://x.com/snowboat84/status/2047457686070141051) - [每个人都应该使用的三个最有用的 Claude Skill](https://x.com/snowboat84/status/2047110768773197834) - [SpaceX 立志传（一）：赌上全部的最后一次发射](https://x.com/snowboat84/status/2046743964192276766) - [估值290亿美元的套壳公司，正在被自己的房东杀死](https://x.com/snowboat84/status/2046380497627230607) - [黄仁勋和主持人吵红了脸：芯片封锁中国，美国到底能不能打赢？](https://x.com/snowboat84/status/2046022377830801725) - [AI将如何颠覆教育，普通人又应该如何抢夺教育新的生态位](https://x.com/snowboat84/status/2044932338262667509) - [学物理的八方英雄们，物理学已死，请转行搞AI](https://x.com/snowboat84/status/2044584627046920278) - [不会编程、没有融资、没有员工，他怎么一个人做到年入2000万](https://x.com/snowboat84/status/2044216044575998136) - [兄弟们想清楚：究竟是你为X打工，还是X为你打工？](https://x.com/snowboat84/status/2043842017260908743) - [一人公司盈利四亿美元：是骗子，还是可复制的红利？](https://x.com/snowboat84/status/2043493870265422223) - [2026第一季度大裁员，AI是背锅侠吗？](https://x.com/snowboat84/status/2042766853404307931) - [重返星辰大海：这次绕月飞行有意义吗？](https://x.com/snowboat84/status/2042405716380835998) - [张雪峰在美国为什么无法成功](https://x.com/snowboat84/status/2042045634245746743) - [2026 企业尸检报告：不用AI，你的公司能活过今年吗？](https://x.com/snowboat84/status/2041672997959057517) - [兄弟们，我创业失败了，人生完整了](https://x.com/snowboat84/status/2040948420391940272) - [Logic Theorist](https://en.wikipedia.org/wiki/Logic_Theorist) - [LEAN Language Reference: History](https://lean-lang.org/doc/reference/4.20.0/Introduction/) - [Mathlib: A Foundation for Formal Mathematics Research and Verification](https://lean-lang.org/use-cases/mathlib) - [AI achieves silver-medal standard solving International Mathematical Olympiad problems](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/) - [Harmonic About](https://harmonic.fun/about) - [Aristotle: IMO-level Automated Theorem Proving](https://harmonic.fun/pdf/Aristotle_IMO_Level_Automated_Theorem_Proving.pdf) - [Harmonic's IMO 2025 Results](https://github.com/harmonic-ai/IMO2025) - [Announcing Our Series C Funding](https://harmonic.fun/news) - [AI Will Write All the Code. Mathematics Will Prove It Works.](https://menlovc.com/perspective/ai-will-write-all-the-code-mathematics-will-prove-it-works/) - [Axiom Math Funding Round](https://www.gaebler.com/VC-Funding-D062A4CB-9F5D-4E62-A5DB-FBC6D9580A9D-Axiom-Math-03-12-2026) - [Axiom](https://axiommath.ai/) - [Ken Ono](https://uva.theopenscholar.com/ken-ono/) - [The Math Legend Who Just Left Academia-for an AI Startup Run by a 24-Year-Old](https://www.wsj.com/tech/ai/math-ken-ono-carina-hong-axiom-startup-649bc417) - [AI For Math Fund Announces $18 Million In Grants](https://www.renaissancephilanthropy.org/news-and-insights/ai-for-math-fund-announces-18-million-in-grants-to-accelerate-breakthrough-discoveries-in-mathematicsnbsp) - [AI for Math Fund](https://www.renaissancephilanthropy.org/initiatives/ai-for-math-fund/) - [Renaissance Philanthropy and XTX Markets Launch New $9 million AI for Math Fund](https://renaissancephilanthropy.org/news-and-insights/renaissance-philanthropy-and-xtx-markets-launch-new-9-million-ai-for-math-fund/) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://papers.nips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html) - [LeanDojo-v2: AI-Assisted Theorem Proving in LEAN](https://leandojo.org/leandojo) - [Is Math the Next AI Frontier? A Conversation with Terence Tao](https://www.renaissancephilanthropy.org/news-and-insights/is-math-the-next-ai-frontier-a-conversation-with-terence-tao) - [Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark](https://harmonic.fun/news/verina-benchmark/) - [Axiom LEAN Engine](https://axle.axiommath.ai/) - [The job description is changing: mathematician Terence Tao on the rise of AI](https://www.nature.com/articles/d41586-026-01246-9) - [Upgrade to Premium](https://x.com/i/premium_sign_up) - [7:49 AM · May 7, 2026](https://x.com/snowboat84/status/2052174034041995572) - [264 Views](https://x.com/snowboat84/status/2052174034041995572/analytics) - [View quotes](https://x.com/snowboat84/status/2052174034041995572/quotes) --- *导出时间: 2026/5/7 08:59:26*