Learning to Discover Interesting Mathematics

Learning to Discover Interesting Mathematics. By Niket Patel and four others, from FAIR at Meta, New York University, and one other institution. Published on the twenty-third of September. No code repository is linked to it.

Large language models are increasingly able to solve advanced mathematical problems, including many that had been open for decades. That opens the door to mathematical knowledge expanding at a scale never seen before. It also opens a question the abstract puts plainly. A model may conjecture and prove more and more theorems, but whether that new knowledge is interesting, or useful, remains open. Producing theorems is one capability. Knowing which ones deserve to be produced is another, and it is the second that this work goes after.

The authors start with a definition. The intrinsic interestingness of a theorem is the ratio between the length of its proof and the length of its statement. By that measure, a short statement that demands a long proof scores high, and a long statement with a short proof scores low. They then show that this intrinsic measure correlates strongly with an extrinsic one: a measure of how useful the theorem turns out to be downstream. A property you can read off the theorem itself tracks the value it has for later work.

Computing metrics like these needs one ingredient, and the paper identifies it as a useful primitive: the difficulty of a proof, conditioned on a set of premises. The authors train a twenty-seven billion parameter model to predict that difficulty, and it does so more accurately than frontier general-purpose models. Around it they build a system that can generate candidate theorems, select the most interesting among them, and iteratively build on a mathematical library that keeps expanding itself.

Optimizing for the metric yields a model capable of producing more interesting theorems. It also changes how much of the output repeats what is already known. Substantial or full overlap with Mathlib falls from ninety-one point nine percent to thirty point six percent, which the authors present as the creation of more out-of-distribution mathematics.

The metrics, they argue, give a practical and quantifiable signal for two jobs inside formal mathematical libraries: ranking conjectures, and guiding proof search.

Where this points is a mathematical library that grows on its own, stays machine-verified, and chooses worthwhile statements without relying on targets supplied by humans. What makes that plausible here is a reduction. Interestingness, a notion that seems to need a mathematician's taste, has been turned into something a model can estimate: how much proof a statement demands, relative to how much the statement says.