Learning to Discover Interesting Mathematics：用 proof difficulty 学习“哪些定理值得继续发现”，推动形式数学库自扩展

该工作把定理“有趣性”定义为 proof length / statement length，并显示这一内在指标与定理的下游效用存在较强相关。作者进一步把“给定 premises 后的证明难度”作为基础 primitive，训练一个 27B 模型预测 proof difficulty，并用该信号筛选候选定理。优化这一指标后，生成结果与 Mathlib 的 substantial/full overlap 从 91.9% 降到 30.6%，并演示了候选生成、interestingness selection 与自扩展 formal library 的循环。