NYU defines a theorem's interestingness score

NYU researchers define a theorem's interestingness as its proof length divided by its statement length, in a paper defining theorem interestingness. A short claim that takes a long proof to settle says more about mathematics than a long claim that resolves in one line.

That ratio is supposed to separate real discoveries from restatements of what mathematicians already know. It matters because automated provers can generate solved proofs faster than anyone can read them.

The team, Patel, Rammal, Hayat, Munos and Kempe, built a 27-billion-parameter model trained to predict that ratio before a proof exists. It outperforms larger, general-purpose frontier models at guessing how hard a given theorem will be to prove.

The sharper result is what happens when a prover optimizes for the metric instead of raw output. Left alone, it mostly restates Mathlib, the standard formalized-math library. In testing, 91.9% of its theorems substantially or fully overlapped with results already there. Once the researchers pointed the system at interestingness instead, overlap fell to 30.6%. The system started building its own theorem library rather than rediscovering the same ground.

A month of AI systems solving hard math problems raised a question nobody had answered: which of those results were new. This is a first attempt at a number for that. It suggests most raw output from an unconstrained prover is closer to homework than discovery.