Imagine a library containing every true mathematical statement anyone could write. Somewhere in its endless shelves would be profound discoveries. But so would be thousands of pages of true statements that merely repeat themselves. How could a searcher tell the difference before spending years looking?
That question is becoming practical as computers get better at producing and proving mathematical claims. A system can generate many statements, and a proof assistant can check whether they are valid. But truth is only the first clue. The tougher puzzle is choosing which true statement is worth pursuing.
A recent study by Niket Patel and colleagues proposes a measurable hint: look for theorems that are compact to state but hard to prove. The intuition is appealing. A short statement that takes a long argument to establish may conceal a dense idea. A sprawling statement may be difficult only because it bundles together many separate claims.
To turn that intuition into a test, the researchers worked inside Lean, a proof assistant that checks formal mathematical arguments. In Lean, a proof is also a piece of code, so the team could count its lines. They compared that cost with the length of the theorem’s statement, including definitions needed to express it. The study calls the resulting ratio a measure of intrinsic interestingness.
There is a catch: a theorem’s difficulty depends on what the prover already knows. A result in probability might be easy to prove if the right probability facts are available, and baffling if the library offers only algebra. So the researchers made proof difficulty conditional on a set of available premises. Their aim was not to declare that one theorem is universally interesting, but to estimate how demanding it is in a particular mathematical context.
The team built training examples from Mathlib, Lean’s large library of formal mathematics. To create richer examples, they expanded the list of premises behind theorems, moving backward through the library’s dependency network and accounting for the proofs of intermediate results. That process produced about 100,000 theorem-and-context examples. A 27-billion-parameter model then learned to predict how many lines a formal proof would take.
With that predictor in hand, the team tested whether the clue could guide theorem-making. They trained a model to propose statements that were easy to express from the supplied premises but predicted to require substantial proofs. The proposals were not accepted on faith: researchers sent them through Lean-based checks and retained statements that could be proved. Across eight areas of mathematics, the trained model’s average measured interestingness rose from 1.76 for its base version to 7.58. The increase appeared in every area tested.
Could that jump be a bookkeeping trick—longer wording, or recycled library facts? The researchers tested both possibilities. They divided proof length by statement length, rather than rewarding long proofs by themselves. They also used a separate language-model judge to assess how much each verified statement overlapped with Mathlib. In the evaluated samples, the share judged substantially or fully contained in the library fell from 91.9 percent for the base model to 30.6 percent for the trained one.
A second test asked whether the measure could help a search grow over time. Starting with mathematical premises, a conjecturer proposed hundreds of candidates per round. A proof-generating system tried to prove them in Lean, and the ten candidates with the strongest interestingness scores became premises for the next round. In comparisons, choosing by the ratio beat choosing the longest proofs. That matters: simply favoring length would be the easiest dead end, but it did worse.
The result is not a machine that has solved the mystery of mathematical taste. The iterative experiment used language models both to help produce proofs and to judge the quality and diversity of results. And proof length in code is an imperfect stand-in for intellectual difficulty: different proof styles or automation tools can change how many lines a proof needs. The authors also note that their measure may miss forms of mathematical value that come from connecting distant fields or inventing useful new definitions.
Still, the central clue is intriguing. A theorem’s usefulness might leave traces in its shape: how little is needed to state it, how much work it takes to establish, and whether later arguments can reuse it. In Mathlib, the study found that its intrinsic score correlated with a separate measure of how often a theorem helps other proofs. That does not settle what makes mathematics beautiful or important. It suggests a more precise next question: can a machine use the structure of proof to find statements that deserve a human mathematician’s attention?
For now, the answer is a cautious yes. The system can steer a search toward verified statements that are less like the library it started from, and the proof gives researchers something concrete to inspect. But the final test is still ahead: whether those statements open genuinely useful paths through mathematics. The puzzle has not been solved. It has acquired a promising new clue.
