Teaching AI to Discover Mathematics Worth Proving

Introduction

Large language models are increasingly capable of solving advanced mathematics and producing machine-checkable proofs. That progress changes the central problem. If a system can generate and prove thousands of statements, how should it decide which ones are worth pursuing?

The paper Learning to Discover Interesting Mathematics focuses on this selection problem rather than treating proof completion as the only objective. Its goal is to give mathematical discovery a practical ranking signal, allowing a model to search for results that are not merely correct, but also less obvious, less redundant, and potentially more useful.

The proposed framework

• A measurable notion of interestingness. The researchers define a theorem’s intrinsic interestingness as the length of its proof divided by the length of its statement. The intuition is that a compact claim requiring a rich derivation may contain more structure than a long statement with a nearly immediate proof.
• Proof difficulty conditioned on premises. To estimate this ratio, a system must assess how difficult a proof is given the available assumptions and mathematical library. The team trains a 27B-parameter model for this task and reports that it predicts conditional proof difficulty more accurately than frontier general-purpose models.
• Generation, ranking, and feedback. The system generates candidate theorems, scores them, selects more interesting candidates, verifies their proofs, and adds successful results to an expanding formal library. That library then becomes the premise set for later rounds of discovery.

Reported results

The paper reports a 4.3-fold increase in the proposed interestingness measure after optimization. It also reports a substantial shift away from existing formal mathematics: the share of generated results with substantial or full overlap with Mathlib falls from 91.9% to 30.6%. This suggests that the system is not simply paraphrasing or recombining familiar library content, but is finding more out-of-distribution formal statements.

The broader contribution is a way to turn an inherently vague research preference into a signal usable by training and search algorithms. If the correlation with downstream utility holds beyond the evaluated setting, such a signal could help allocate proof-search compute toward conjectures that are more likely to support future work.

The metric should not be treated as a definition of mathematical importance. Long proofs can result from inefficient formalization, while short proofs can establish profound ideas. Proof length is therefore better viewed as a candidate-ranking feature than as a final scientific judgment. Human mathematicians will still be needed to assess conceptual significance, generality, and usefulness.

The proposed loop nevertheless points toward a different kind of formal library: a model proposes statements, a proof assistant verifies them, a learned evaluator ranks them, and verified discoveries become premises for the next cycle. The difficult question is whether this loop can produce not only harder proofs, but mathematics that researchers genuinely want to understand.

Source: Hugging Face Daily Papers