🔥 今日值得一读
AI造出数学定理，与人类库重叠从91.9%暴降到30.6%！
Learning to Discover Interesting Mathematics
👨💼 主理人解读 · 为什么值得关注
想让LLM自动发现值得研究的数学定理？这篇用证明/陈述长度比定义有趣度，可指导自动数学探索的筛选。
📖 AI 总结
本文探讨了大语言模型在数学发现中的一个核心问题：即便模型能证明越来越多的定理，这些新知识是否真正有趣或有价值仍无定论。作者将定理的“内在趣味性”定义为证明长度与陈述长度之比，并证明该指标与定理下游实用性的外在度量高度相关。研究提出以“在给定前提下证明的难度”作为计算这些指标的基础，并训练了一个270亿参数的模型，其预测证明难度的准确度超过前沿通用模型。以该指标进行优化后，模型能生成更有趣的定理，同时将生成内容与Mathlib的重叠率从91.9%降至30.6%，表明其产出了更多分布外的数学内容。该系统可生成候选定理、筛选其中最有趣者，并迭代构建自我扩展的数学库。这一框架为构建无需人工指定目标、能自主选择有价值命题的机器验证数学库提供了可行路径。
🔑 关键词速览
| 内在有趣性 | 定理的证明长度与陈述长度之比，用于衡量定理的趣味性。 |
| 证明难度 | 以一组前提为条件的证明难度，是计算有趣性指标的有用基元。 |
| Mathlib | 一个大型的数学形式化库，用于机器验证数学定理。 |
| 分布外数学 | 与现有数学库（如Mathlib）重叠较少的新颖数学内容。 |
| 自我扩展数学库 | 能够自动生成、选择和构建新定理的机器验证数学库。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅