形式公理系统中的自监督定理发现

本文探讨了智能体能否在无人类先验知识的情况下自主发现有用的定理。研究者在形式公理系统中开发了一种智能体，仅从公理和推理规则出发，通过交替进行证明搜索与有用定理提取，逐步构建可复用的定理库。实验表明，该智能体发现了数万个定理，并能解决人类编写的基准问题。此外，发现的定理作为提示引理显著提升了大语言模型的证明性能，证明了无需依赖人类提供的定理库即可涌现出有用的数学知识，为数学领域自进化 AI 系统提供了新路径。