A computer can check whether a proof is valid. That sounds like a major step toward automated mathematics—and it is. But it leaves a harder question untouched: among all the claims a computer might prove, which ones are worth proving?
A recent research team tried to turn that question into a number. Their unexpected finding is that a mathematical claim can be judged not by the length of its proof alone, but by how much proof it takes relative to how briefly the claim can be stated. That simple ratio helped steer a theorem-generating system toward results that were less like the ones already in a major formal mathematics library.
The project takes place inside Lean, a computer system that checks mathematical proofs down to their logical steps. In Lean, a theorem is not just a sentence written in familiar notation: it is a formal statement, and its proof is code that the system verifies. That makes it possible to count things that are difficult to measure in ordinary mathematics, such as the lines of code in a proof and the characters needed to state a theorem using the definitions already available.
The researchers’ intuition was that some theorems have a particular appeal: they are easy to say, but surprisingly hard to establish. Fermat’s Last Theorem for specific exponents is a classic example of the shape of this idea: the claim can be expressed simply, while its proof draws on substantial mathematics. By contrast, a long proof of a sprawling statement might be long simply because the statement contains many separate claims.
So the team’s score compares proof length with statement length, including the definitions needed to understand the statement from the available mathematical context. This qualification matters. A claim about probability may be concise if the reader already has the language of probability, but much harder to express from a starting point that contains only algebra. The score is therefore not a universal rating of a theorem’s beauty. It asks how much proving work a claim demands, given the mathematical vocabulary at hand.
Before using that score to guide a system, the researchers checked whether it tracked anything mathematicians might care about. They compared a theorem’s score with a rough measure of its later usefulness in Mathlib, the large Lean library: how many other proofs directly use it, multiplied by the effort to prove it from scratch. Across library statements with downstream users, the two measures had a Spearman correlation of 0.756. In other words, statements that were compact to describe but demanding to prove tended, in this dataset, to be reused more.
That is a correlation, not evidence that difficult proofs cause useful theorems. And the library measure captures only one kind of value: a theorem may be important because it connects ideas or helps explain something outside mathematics, even if few formal proofs call it directly. Still, the result offered a practical surprise. A feature of a theorem that can be estimated before its future role is known seemed to line up with a feature visible only after other work had built on it.
The next challenge was estimating proof difficulty without first asking a proving system to produce every proof. The team trained a 27-billion-parameter model on examples built from Lean’s Mathlib library. It learned to predict how many lines of proof code a target theorem would require, given a set of premises. On a held-out evaluation, its predictions were more accurate and better ranked by difficulty than those of the general-purpose models tested.
Then came the more direct test: could a model be trained to propose mathematically interesting claims? The team fine-tuned a theorem-generating model using the new score as a reward. When researchers later had a proving system produce proofs for its proposals, the trained model’s average measured interestingness rose from 1.76 to 7.58—more than fourfold—across eight areas of mathematics. The researchers also checked how closely each generated statement matched existing Mathlib content. In an assessment by another language model, 30.6% of the trained model’s statements were judged substantially or fully contained in the library, compared with 91.9% for the untrained base model.
Those numbers need careful reading. The propositions that made it into this comparison were proved and checked in Lean, so they were not merely plausible-sounding guesses. But “less like the existing library” does not automatically mean “mathematically important.” The overlap assessment was made by a language model, and the paper does not establish that the new results will prove useful in future research. The system’s achievement is narrower, but still striking: it changed the kinds of formally verified statements it produced by rewarding a measurable feature of their proofs.
The team also tested a small discovery loop. A conjecturing model proposed hundreds of candidate statements from a collection of existing results; a filter removed duplicates and enforced variety; and a proving system checked the survivors. The system then added selected theorems to its working collection, giving it new premises for the next round. Crucially, selecting the longest proofs alone performed worse than selecting by proof length relative to statement length. A long proof, it turned out, was not enough. The compactness of the claim mattered too.
There is a catch built into the very idea. Lines of Lean code are not a pure measure of mathematical difficulty: different proof styles and automation tools can make the same result look shorter or longer. The researchers acknowledge that their score captures only some aspects of mathematical value, and that future usefulness remains unclear. Their result is not that a formula can now recognize mathematical beauty. It is that a carefully chosen, imperfect signal can push theorem search away from producing only familiar or routine results—and can do so while every accepted claim remains machine-checked.
For generations, mathematicians have chosen problems using intuition, taste, context, and experience. A formal system cannot yet replace those judgments. But this work suggests an unexpected foothold: perhaps a machine can learn something about what makes a result worth pursuing by looking at the distance between a theorem’s small footprint as a statement and the effort required to prove it.
