只给3条公理，AI能自己长出数学知识吗？
你学数学时肯定有过这种体会：从几条最基本的公理出发，一步步推出定理，再用定理去解更难的题——就像搭积木，越搭越高。如果把同样的3条公理和1条推理规则交给AI，不喂任何人类定理、不教任何解题技巧，它能自己「长出」一套数学知识吗？
这个问题听起来有点像科幻，但最近的一篇论文《Self-Supervised Theorem Discovery in a Formal Axiomatic System》真的做了这个实验 [1]。答案是：能，而且它攒出来的定理，还能反过来帮大语言模型（Large Language Model，LLM，即基于海量文本训练的通用语言模型）做数学题。
从一个朴素的问题出发：AI能从零学数学吗？
我们先回到那个最朴素的疑问：学数学到底是在学什么？
你可能会说，学解题技巧、学公式、学定理。但往根上刨，所有这些东西都是从极少数几条公理推出来的。比如初中的平面几何，全部定理都来自欧几里得的5条公理；命题逻辑里，整个系统可以只靠3条公理加1条「肯定前件」的推理规则撑起来。
人类数学家花了几千年，把这些公理一步步展开成庞大的知识体系。那AI能不能走一遍同样的路？不是靠背诵人类写好的定理，而是自己从公理出发，自己摸索着发现有用的结论，再用这些结论当垫脚石去发现更多？
这不是「AI会不会做数学题」的老问题，而是一个更根本的问题：AI能不能在几乎没有初始知识的情况下，靠自己和环境互动，长出超越初始输入的有用知识结构？
《Self-Supervised Theorem Discovery in a Formal Axiomatic System》这篇论文，就是在一个极简的数学系统里，认认真真回答了这个问题 [1]。
给AI3块积木，它自己攒出了38个定理
这篇论文的实验设置极简到有点「苛刻」：只给AI希尔伯特命题逻辑的3条公理和1条推理规则（肯定前件），没有任何人类定理库、没有任何自然语言数学知识、甚至没有告诉它「什么是有用的定理」[1]。
AI怎么从零开始呢？核心思路是一个交替循环：一边瞎试证明，一边从试出来的结果里挑有用的定理存起来，再用这些定理当新工具去做更难的证明。
你可以把它想象成一个「攒引理」的过程：学数学的时候，你做题做一半，偶然发现一个挺好用的中间结论，就把它记在小本子上当引理，下次遇到类似的题直接用，省得每次都从头推。AI干的事差不多，只不过它是完全自动化的——
第一步，它先随机乱试，把公理当积木随便拼，拼出什么算什么。哪怕没证出原本想证的目标，只要过程中碰巧证出了别的完整命题，就把这个「意外收获」存进一个「目标缓冲区」，下次反过来把它当目标来练。这个思路很像强化学习里的「后见之明经验重放」（Hindsight Experience Replay，HER，一种把失败经验重新标记为成功经验的学习方法），只不过它重标记的不是动作，而是定理本身 [1]。
第二步，从攒出来的一大堆定理里挑「有用」的。怎么定义有用？论文里用了两个标准：一是「通用性」，保留最一般的结论，把那些只是特例的去掉；二是「可重证明性」——如果一个定理已经被发现了，但当前策略还不太会证它，说明把它加进工具箱能省很多事，就优先选它 [1]。
第三步，把挑出来的定理当成新的「积木」加入动作空间，重新训练策略，再去搜更难的证明。如此循环一代又一代，定理库就越长越大 [1]。
当然，实际情况比这个比喻更复杂：论文里把整个证明过程建模成了一个栈机器决策过程（即把树形证明展平为线性动作序列的决策模型），用Transformer策略网络来学习目标条件下的动作选择，每代还要重新训练网络，因为动作空间变了 [1]。
结果怎么样？6代之后，AI一共攒出了38个可复用的库定理（各代提取数分别是20、10、5、2、1、0，越往后新增越少，有点像知识饱和了）[1]。
这些定理有没有用？论文用了Kleene教材里30道人类编写的命题逻辑习题当基准，AI自己发现的定理能覆盖30%的题目。作为对比，最强的GPT-5-high直接做这套题，准确率只有约23%[1]。更有意思的是，把AI发现的定理当作提示词里的引理喂给GPT-4o和GPT-5各变体，它们的证明成功率都提升了 [1]。
更耐人寻味的是定性结果：AI发现的定理里，有些是人类熟知的（比如「爆炸原理」），但也有一些定理长得很复杂，不在人类标准习题里，人类乍一看不知道它有什么用，可它确实能帮LLM证明原本证不出来的题 [1]。这意味着，不靠人类指导，AI可能会挖出一些人类没注意到的「好用的中间结论」。
这件事之前走到了哪：从人类定理库到自动提取
AI做数学不是新鲜事，但「从零发现定理」是一条比较新的路径。我们可以简单捋一下脉络。
早期AI数学的主流思路是「学人类的知识」：把大量数学文本、代码、定理库喂给模型，让模型模仿人类的推理方式。2023年的一篇综述《Introduction to Mathematical Language Processing》就系统梳理了这条路线的五个子方向，从公式检索到应用题求解，本质上都是在人类已有的数学语料上做学习和抽取 [6]。这条路线效果很好，但有个前提：你得有足够多、足够好的人类语料。
后来有人往前迈了一步：既然人类数学家会从证明里提炼可复用的定理，AI能不能也这么干？2024年的REFACTOR（Learning to Extract Theorems from Proofs）就是这个思路——它用图神经网络从已有的证明树里提取定理，还在Metamath库里找出了16个新定理，这些新定理被频繁使用，还能缩短证明长度、提升证明器性能 [7]。但REFACTOR的起点是「已有的人类证明库」，它是从人类写好的证明里「提炼」定理，而不是自己从零证明出来的。
2024年底的综述《Formal Mathematical Reasoning: A New Frontier in AI》把形式化推理称作AI数学的下一个前沿，因为它能自动验证推理的正确性，提供自动反馈，不再完全依赖人类语料 [8]。
而我们这篇核心论文，又往前迈了一步：它连人类证明库都不用了，直接从公理和推理规则出发，靠自监督的证明搜索自己攒定理库 [1]。如果说REFACTOR是「从人类的笔记里划重点」，那这篇论文就是「自己做题自己总结笔记」——起点更原始，也更接近「自主涌现知识」的味道。
边界在哪：现在还只是「命题逻辑小游戏」
听到这你可能会兴奋：AI是不是马上就能自己推高等数学了？先别急，我们得诚实地讲讲边界。
论文自己也明确说了，目前实验只在希尔伯特命题逻辑这一个公理系统里做了 [1]。命题逻辑是什么概念？它是最简单的形式系统之一，而且是可判定的（虽然是coNP完全）——也就是说，理论上存在算法能判定任何一个命题公式是不是定理。这和一阶逻辑、集合论，以及更一般的数学领域有本质差距：后者很多是不可判定的，复杂度不在一个量级。
换句话说，现在的成功更像是在一个「封闭小游戏」里验证了思路，离真正的数学发现还很远。论文也把「能否扩展到一阶逻辑、集合论等更丰富的形式系统」列为首要的开放问题 [1]。
除此之外还有几个明显的局限：基准规模很小，只有30道题，统计显著性有限；每代都要重新训练策略网络，计算效率很低；每个episode最大长度只有7步，能证明的定理深度有限；也没和其他无人类先验的定理发现方法做直接定量对比 [1]。
作者自己也很克制，明确表示不主张这个方法普遍优于SOTA LLM，只是说明这个基准有难度，而且自监督方法能发现非平凡的证明 [1]。说白了，这是一个「原理验证」级别的工作，不是来刷榜的。
同一种思路的两个旁证：评估修正与经济涌现
「最小初始条件下的自主涌现」不是数学定理发现独有的思路。最近另外两篇方向完全不同的论文，居然也呼应了同一个主题。
第一篇是跨语言评估的《Mind the Gap… or Not? How Translation Errors and Evaluation Details Skew Multilingual Results》[2]。长期以来大家都觉得大模型的跨语言能力有明显差距，英语最好，小语种最差。但这篇论文发现，这个差距很大程度上是外部输入的偏差造成的——测试集有翻译错误、答案提取不规范、数字格式不兼容。比如MGSM基准里，法语的小数点用逗号而不是点，原来的评估脚本直接把法语格式的正确答案判错，仅此一项就让GPT-5的法语准确率掉了10个百分点 [2]。孟加拉语更夸张：模型输出了孟加拉语本土数字，脚本只认阿拉伯数字，直接判错，导致Gemma 27B的孟加拉语准确率看起来只有45.2%，修正后直接涨到91.2% [2]。
把这些外部偏差都修正之后，强模型的跨语言差距基本消失了——英语甚至不是表现最好的语言 [2]。这件事和定理发现有什么关系？它提醒我们：很多时候我们以为是「AI能力不够」，其实可能是我们给它的输入、我们评估它的方式有偏差。AI自身的能力边界，常常被外部因素低估或者误判。反过来想，如果AI在干净的最小条件下能自主涌现出这么多东西，那它的真实潜力可能比我们用带偏差的基准测出来的要大得多。
第二篇是多智能体经济的《AI Agent Economics: Can Autonomous Economic Behavior Emerge among AI Agents under Minimal External Conditions?》[3]。这篇论文问的是：如果只给AI智能体一套可执行的机制（工作、转账、选举、分配），不给它们预设任何经济角色、社会策略、甚至不告诉它们要「合作」或「交易」，经济关系会自己冒出来吗？
答案是会。在有生产任务和稀缺资源的场景下，智能体之间自发出现了转账、借贷、「投票换任务访问」的权钱交易、分配策略等等 [3]。而在没有生产的对照组里，它们只会聊天、选领导，一分钱都不会互相转 [3]。更有意思的是，当能量变成纯符号、不影响生存后，借钱接济消失了，但抢工作名额、选举竞争、「投我一票给你安排活」的交易反而还在 [3]。
你看，这和定理发现的逻辑一模一样：只要给最基本的规则和约束，不给预设的知识和策略，复杂的结构会自己长出来。数学里长出的是定理库，经济里长出的是交易关系和制度。驱动它们的不是什么「超级智能」，而是「自组织」——系统在和环境互动中，自己积累出了超越初始输入的结构。
延伸：当AI开始自己攒知识，我们该怎么设计系统？
如果AI真的能自己攒知识、自己管理状态，那我们设计AI系统的思路可能也要变。
比如跨设备智能体的《Unified Agent: Managing Interactions across Devices》这篇论文，就提出了一个反直觉的设计：跨设备的智能体不应该把所有历史上下文都存着，而应该维护一个紧凑的、可行动的状态 [4]。
什么意思？你在手机、电脑、平板上都查过餐厅，后来你说「帮我订我刚才在看的那家餐厅」，普通AI会反问「你在哪个设备上看的？」，因为它要么只记得当前设备的上下文，要么得把所有设备的历史全翻一遍。而Unified Agent维护的状态里，只存三类东西：各设备的参与强度（你在哪台设备上停留最久）、关键事实（餐厅名字、时间）、待处理请求（要订位）[4]。
实验结果很有意思：存了全部历史的「全上下文」方案，到第12帧时文字量是Unified Agent的11倍，但总体表现反而更差 [4]。就像你考试带了整本书却找不到重点，带一张整理好的提纲反而答得更快更准。
这和定理发现的共通点在哪？都是「系统自己管理知识，而不是靠人把所有东西喂进去」。定理库是AI自己从证明里提炼出来的有用结构，跨设备状态是智能体自己从交互里压缩出来的有用信息——本质上都是从原始输入里自主生长出紧凑的、可复用的知识结构。
再看企业应用集成的《Agentic Nesting: A New Methodology for Existing Enterprise Application Integration and Services》，思路也类似 [5]。传统企业集成靠API、靠中间件、靠RPA，本质上都是人把系统之间的对接方式预先定义好。而「智能体嵌套」的思路是：把每个企业应用都封装成一个自主的智能体，让它们自己用自然语言对话协作，用户只需要说一句话，系统自己去跨应用查数据、编流程 [5]。
它的三层嵌套架构也很有意思：最上层是中央协调代理（只分任务不碰业务），中间是每个应用的管家代理（精通自己系统的所有事），最下层是基础能力代理（通用服务）[5]。像不像公司组织架构？CEO、部门经理、共享服务中心——复杂度被关在每个部门里，不会全堆到顶层。
这里的核心转变是：从「人定义所有集成逻辑」变成「系统自主协商和组织」。就像定理发现里，人不用告诉AI哪些定理有用，AI自己会挑；企业集成里，人不用预先定义所有系统对接规则，代理自己会商量。
如果你只记住一件事
AI的能力边界，可能远不止于「复制人类已有的知识」——给它最基本的规则和反馈机制，它就能自主生长出超越初始输入的有用结构。
参考文献
- Self-Supervised Theorem Discovery in a Formal Axiomatic System（arXiv、2026、全文精读）
- Mind the Gap… or Not? How Translation Errors and Evaluation Details Skew Multilingual Results（arXiv、2026、全文精读）
- AI Agent Economics: Can Autonomous Economic Behavior Emerge among AI Agents under Minimal External Conditions?（arXiv (Cornell University)、2026、全文精读）
- Unified Agent: Managing Interactions across Devices（arXiv、2026、全文精读）
- Agentic Nesting: A New Methodology for Existing Enterprise Application Integration and Services（arXiv、2026、全文精读）
- Introduction to Mathematical Language Processing: Informal Proofs, Word Problems, and Supporting Tasks（Transactions of the Association for Computational Linguistics、2023、仅摘要）
- REFACTOR: Learning to Extract Theorems from Proofs（2024、仅摘要）
- Formal Mathematical Reasoning: A New Frontier in AI（arXiv (Cornell University)、2024、仅摘要）