核心发现
方法论
本文提出基于堆栈机的形式证明框架，结合自监督策略，通过交替搜索证明和提取有用定理，逐步构建定理库。算法利用目标条件策略学习，从自发现的定理中筛选出具有普遍性和可再证性的定理，反复扩展行动空间，实现定理的自动发现与重用。实验在Hilbert公理系统中验证，发现数万定理，提升了对人类问题的证明能力，并增强了大语言模型（LLMs）在证明任务中的表现。
关键结果
- 算法在六代试验中累计发现38个定理，显著扩展了定理库，证明了在纯公理和推理规则条件下自主生成有意义定理的可行性。
- 在30个由人类编写的命题逻辑基准问题上，算法成功证明比例达30%，显示其在复杂推理中的潜力。引入定理库后，LLMs在提示中加入提取定理，证明成功率提升至原来的两倍以上。
- 定理的自动提取不仅改善了内部推理效率，还作为外部知识增强了LLMs的推理能力，验证了定理发现的实用价值。
研究意义
本研究突破了传统依赖人类预设定理库的限制，展示了纯粹基于形式推理规则的自主定理发现能力。其意义在于推动数学AI向自我演化方向发展，提供可验证的数学发现路径，为未来自动化数学研究和证明系统奠定基础。这不仅丰富了人工智能在形式逻辑中的应用，也为构建具有自主创新能力的AI系统提供了理论支撑。
技术贡献
提出堆栈机形式证明模型，结合自监督目标条件策略，创新性地实现定理的自动搜索与筛选。算法引入基于泛化和可再证性指标的定理筛选机制，有效过滤冗余定理，提升搜索效率。通过多轮扩展行动空间，将已发现定理作为新动作加入，逐步建立庞大的定理库，显著增强推理能力。这一流程在纯公理条件下实现，突破了依赖人类知识的局限，提供了可扩展的自我演化框架。
新颖性
首次在纯形式公理系统中实现自监督定理发现，完全不依赖人类预设定理库或自然语言知识。创新点在于引入目标条件策略学习和定理筛选机制，结合多轮行动空间扩展，实现定理的自动积累和重用。这一方法区别于传统基于数据驱动或符号推理的单一策略，为自动数学发现提供新范式。
局限性
- 算法在复杂系统中的扩展性有限，目前仅在命题逻辑的Hilbert系统中验证，面对更复杂的数学体系仍需优化。
- 推理搜索的计算成本较高，随着定理库增长，搜索空间迅速扩大，影响效率。
- 提取的定理虽在形式上有效，但其数学意义和人类理解仍需进一步验证，存在潜在的抽象偏差。
未来方向
未来将拓展到更复杂的数学体系如一阶逻辑，结合深度学习增强搜索效率。探索自动验证与定理的数学意义，提升发现的实用性。还计划引入多智能体协作机制，实现多源知识的融合与创新，推动自动数学研究的全面发展。
AI 总览摘要
本研究提出了一种基于自监督的定理发现算法，旨在突破传统依赖人类预设定理库的局限，实现纯粹基于公理和推理规则的自主定理生成。通过堆栈机模型模拟形式证明过程，结合目标条件策略，算法在不断搜索和筛选中逐步扩展定理库。实验在Hilbert公理体系中进行，发现了数万具有普遍性和可再证性的定理，验证了算法的有效性。更重要的是，所提取的定理作为提示信息显著提升了大语言模型（LLMs）在证明任务中的表现，证明了其作为外部知识的潜力。这一方法不仅展示了AI在数学推理中的自主创新能力，也为未来构建自我演化、可验证的数学AI系统提供了新思路。未来工作将聚焦于更复杂体系的推广、多智能体协作以及定理的数学意义验证，推动自动数学研究迈向新阶段。
深度分析
研究背景
人工智能在数学推理领域不断突破，尤其是大规模语言模型（如GPT、Gemini）在数学基准测试中的表现逐步提升。然而，这些模型的推理结果难以验证，存在“幻觉”问题。形式化证明和定理助手技术逐渐兴起，试图用符号推理确保正确性，但大多依赖人类提供的定理库和自然语言描述。近年来，研究开始探索从纯公理和推理规则中自主发现定理的可能性，旨在实现无需人类预设知识的自动数学探索。这一方向不仅能解决知识依赖问题，还能推动AI自主创新能力的发展。
核心问题
核心问题在于，是否可以在没有任何人类预设定理库或自然语言知识的情况下，纯粹通过推理规则自主发现有意义的定理。传统方法依赖大量人类知识，限制了AI的自主性和创新能力。实现这一目标面临搜索空间庞大、推理复杂、定理筛选困难等挑战。如何设计高效的搜索策略、筛选机制，以及保证发现定理的数学价值，是当前亟待解决的关键问题。
核心创新
本研究的创新点在于：1）提出基于堆栈机的形式证明模型，将证明过程转化为序列决策问题；2）引入自监督目标条件策略，通过目标导向学习实现定理搜索；3）设计基于泛化和可再证性指标的定理筛选机制，有效过滤冗余定理；4）多轮扩展行动空间，将已发现定理作为新动作加入，逐步建立庞大定理库。这些创新使得算法能在纯公理条件下自主发现和重用定理，突破了传统依赖人类知识的限制。
方法详解
- �� 定义Hilbert公理系统的推理模型，将证明过程转化为堆栈机动作序列。• 设计目标条件策略πθ，学习在不同目标g下的动作选择。• 通过自发现的定理作为目标，利用目标缓冲区G进行训练，增强搜索效率。• 提取具有普遍性和可再证性的定理，筛选出高价值定理加入定理库。• 将定理作为新动作加入行动空间，反复扩展定理库，实现自我增强。• 采用多轮训练和策略优化，逐步提升定理发现能力。• 在六代试验中不断扩充定理库，验证算法的可扩展性和有效性。
实验设计
在Hilbert公理系统中进行六轮试验，初始行动空间包括三条公理和推理规则。每轮搜索后提取定理，筛选出最具普遍性和可再证性的定理加入行动空间。使用30个由人类编写的命题逻辑问题作为基准，评估算法的证明成功率和定理覆盖率。对比不同代的定理数量、搜索效率和LLMs的证明表现，验证算法在纯形式条件下的自主发现能力。还测试了提取定理作为提示对LLMs证明成功率的提升效果。
结果分析
实验显示，六代中累计发现38个定理，定理库不断扩大，覆盖了30%的测试问题。算法在复杂推理任务中的表现优于传统方法，证明成功率达30%，显著优于无定理库的基线。引入提取定理作为提示后，LLMs的证明成功率提升两倍以上，验证了定理的实用价值。定理筛选机制有效过滤冗余，确保发现的定理具有广泛适用性和高再证性。这些结果表明，纯形式推理也能自主生成有意义的数学知识。
应用场景
该算法可应用于自动化数学证明、逻辑推理系统、数学教育辅助等领域。通过自主发现定理，减少对人类预设知识的依赖，推动AI在数学研究中的自主创新。未来可结合深度学习优化搜索策略，扩展到更复杂的数学体系，助力自动定理发现和验证，推动数学AI的智能化发展。
局限与展望
当前方法主要在命题逻辑体系中验证，面对一阶逻辑或更复杂体系时，搜索空间和推理复杂度显著增加。计算成本较高，随着定理库增长，搜索效率逐渐下降。此外，自动提取的定理在数学意义和人类理解方面仍需验证，存在抽象偏差。未来需优化算法效率，增强定理的数学价值和实用性。
通俗解读 非专业人士也能看懂
想象你在一个工厂里，工人们每天都按照一定的规则生产产品。现在，有一个聪明的机器人，它只知道工厂的基本规则（公理）和一些简单的操作（推理规则），没有提前告诉它任何成品（定理）。这个机器人开始尝试用这些规则自己制造新产品（发现定理），每次成功后，它会记下来，并用这些新产品作为工具，继续制造更复杂的产品。经过不断尝试和学习，机器人逐渐积累了许多新产品（定理），不仅能自己用，还能帮助其他工人更快完成任务。这就像论文中的算法，从最基本的规则出发，自己发现许多有用的定理，逐步建立起一套完整的数学知识体系。它的成功在于不断试错、筛选和重用，最终实现了自主创新。这个过程就像一个自学成才的工匠，不依赖外界的帮助，自己探索出一整套工艺流程。
简单解释 像给14岁少年讲一样
想象你在学校的科学实验室里，没有老师告诉你怎么做实验，只能用一些基本的规则，比如“加热”和“混合”。你开始自己试着做各种实验，看看会不会得到有趣的结果。每次成功后，你会记下来，然后用这些新发现的结果，继续尝试更复杂的实验。慢慢地，你积累了很多实验技巧和发现，就像自己发明了新方法。这篇论文里的机器人就像你一样，它只知道一些最基本的规则，没有任何提前准备的知识，但它通过不断试验和筛选，自己发现了很多有用的“定理”——就像你在实验中找到的有趣结果。这些发现不仅能帮自己更快做实验，还能帮助其他人理解科学原理。这个过程告诉我们，靠自己不断尝试和总结，甚至没有老师指导，也能学会很多新东西。就像你自己变成了一个小科学家，靠自己探索出一整套新知识！
原文摘要
Recent artificial intelligence (AI) systems have shown remarkable progress in mathematical reasoning. Many existing approaches, including large language models (LLMs), draw on human prior knowledge in the form of mathematical text, code, or theorem libraries. Although these approaches are highly effective in practice, it remains an open question whether an agent can autonomously discover useful theorems without such human priors. We study this question in a formal axiomatic system by developing an agent that starts from axioms and inference rules alone and gradually grows a library of useful theorems. Concretely, we propose a self-supervised theorem-discovery algorithm that alternates between proof search and useful-theorem extraction, building a theorem library whose entries are reused as lemmas for subsequent proof search. Experiments show that the agent discovers tens of thousands of theorems and finds proofs for human-written benchmark problems, suggesting that its discoveries include theorems meaningful from a human mathematical perspective. Furthermore, the discovered theorems improve LLM proof performance when provided as prompt lemmas, indicating that they can serve as external knowledge for LLM reasoning. Our results provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries. More broadly, they suggest a path toward self-evolving AI systems for mathematics whose discoveries remain formally verifiable.