学习发现有趣的数学
TLDR
将定理有趣性定义为证明长度与陈述长度之比，训练27B模型预测证明难度，生成更有趣、更分布外的定理。
评分理由
Strengths include a novel, quantifiable metric for mathematical interestingness, empirical validation via correlation with downstream utility, and demonstration of more out-of-distribution theorem generation. Weaknesses include reliance on formal proof length as a proxy and limited evidence about broader mathematical or real-world significance.
Read-first 评分解释
综合优先阅读分 46.5，由主题、引用、图谱、方法、可复现性和近期性等信号加权得到。 原始总分保留为 45。
研究版图角色
前沿论文
排序敏感性
稳定性：volatile；排名波动范围：41。
关键词评分
深度分析
创新点
- 将定理的内在趣味性定义为证明长度与陈述长度之比。
- 使用以一组前提为条件的证明难度作为计算趣味性度量的原语。
- 训练一个27B模型，其预测证明难度的准确度超过前沿通用模型。
- 针对趣味性度量进行优化，生成更有趣的定理以及大量分布外的数学内容。
- 提出一个自我扩展的机器验证数学库循环，无需人工设定目标即可生成、选择并构建候选定理。
方法
本文定义了内在趣味性为证明长度与陈述长度之比，并在Mathlib等形式化数学库中验证其与外在下游效用的相关性。作者训练了一个27B模型来预测以一组前提为条件的证明难度，并将其准确度与前沿通用模型进行比较。随后，所提出的度量被用于优化生成候选定理、选择有趣定理并迭代扩展形式化库。
关键结果
内在趣味性度量与外在下游效用强相关，27B难度预测模型优于前沿通用模型。针对该度量进行优化，使与Mathlib的大量或完全重叠从91.9%降至30.6%，并生成更有趣的定理。
局限性
- 摘要未明确说明局限性；仅指出LLM生成的数学知识是否有趣或有用仍是一个开放问题，而所提出的度量是一种实用且可量化的信号。