[LG]《Learning Interestingness in Automated Mathematical Theory Formation》G Tsoukalas, R Saha, A Thakur, S Reguyal... [UT Austin] (2025) 自动数学理论形成：学习“有趣性”引导数学发现人工智能在数学自动发现领域迈出两大关键步伐：1. Fermat环境：首次将数学概念发现与定理证明建模为马尔可夫决策过程（MDP），通过符号化动作实现数学理论的自动构建与验证，打造开放式理论探索平台。2. EvoAbstract算法：创新性引入基于大型语言模型（LLM）的进化程序合成和抽象学习，自动生成“有趣性”度量函数，指导理论发现过程，显著优于传统手工设计的启发式指标。核心贡献：- Fermat支持定义、猜想、证明等动作，构建数学知识图谱，利用Z3定理证明器验证猜想。- 有趣性被视为内在奖励函数，EvoAbstract通过多岛模型迭代进化，并周期性抽象高效子程序，促进模块化与复杂有趣度量的发现。- 在初等数论和有限域𝔽27的环境中，EvoAbstract自动合成的度量函数在发现人类数学知识的基准集合上实现了显著提升。- 发现的有趣性函数兼具可解释性，揭示了诸如示例平衡性、构造规则多样性与复杂度等关键特征对数学发现的促进作用。实验亮点：- EvoAbstract在多次独立运行中均优于随机、手工HR启发式指标和单次LLM采样策略。- 自动发现的函数能重新发掘经典度量并创新组合，体现数学对象的深度与广度特征。- 生成的数学理论涵盖加法、乘法、可除性、素数等基础概念，展现出探索潜力和自动证明能力。未来展望：- Fermat将扩展支持更复杂领域与交互式定理证明器，如Lean，实现“从零开始学会证明”。- 持续优化探索策略，解决知识图谱规模与多样性平衡，推动自动数学理论的深层次创新。开源地址：github.com/trishullab/Fermat阅读原文请见：arxiv.org/abs/2511.14778