Learning to Discover Interesting Mathematics
The paper proposes a scoring rule for whether machine-generated theorems are worth pursuing.
The authors define a theorem’s “intrinsic interestingness” as proof length divided by statement length, and say it tracks downstream usefulness. They train a 27B model to predict proof difficulty, then use that signal to rank and generate candidate theorems. In their tests, optimizing for the metric reduced substantial or full overlap with Mathlib from 91.9% to 30.6%, suggesting more out-of-distribution formal math. The goal is a self-expanding, machine-verified library that can choose promising statements without human targets. HF Daily Papers' note
The authors define a theorem’s “intrinsic interestingness” as proof length divided by statement length, and say it tracks downstream usefulness. They train a 27B model to predict proof difficulty, then use that signal to rank and generate candidate theorems. In their tests, optimizing for the metric reduced substantial or full overlap with Mathlib from 91.9% to 30.6%, suggesting more out-of-distribution formal math. The goal is a self-expanding, machine-verified library that can choose promising statements without human targets. HF Daily Papers' note
score 5