The Problem of Choosing What to Prove
A mathematician's lifetime output is typically tens to hundreds of theorems. Deciding which problem to attack is the hardest part of the craft to teach: there is no scoring function, peer review happens years later, and "is this problem worth doing?" usually rests on dinner-table intuition.
On September 23, 2026, a paper appeared on arXiv attempting to replace this intuition with a computable ratio (arXiv:2609.28603). It is titled *Learning to Discover Interesting Mathematics*, by Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos, and Julia Kempe.
📏 A Computable Ruler
The paper's definition of "interesting" is direct: a theorem's intrinsic interestingness equals its proof length divided by its statement length.
Theorems with short statements and long proofs score high. Fermat's Last Theorem — a one-sentence question that took over three centuries to answer — is the extreme sample under this definition.
A definition alone is not enough; the authors validate it by correlating the ratio with an external measure: how useful a theorem is downstream, i.e., whether other theorems build on it. The paper reports a strong correlation.
The cost of reducing "interesting" to a ratio is that it misses things mathematicians genuinely care about, such as whether a proof reveals structure. [Assessment] The authors do not claim the ratio *is* interestingness — only that it correlates with downstream usefulness and serves as a computable proxy.
The extreme case makes the ratio's range clear. Fermat's Last Theorem's statement is readable by a high schooler: the equation xⁿ + yⁿ = zⁿ has no positive integer solutions for integers n > 2. Its proof took over 300 years, culminating in a paper over a hundred pages long, resting on an entire edifice of arithmetic geometry built only afterwards.
One-line statement, three-hundred-page proof: an extremely high ratio. Most theorems in formalization libraries sit at the other end — statement and proof length comparable, ratio near one.
The implicit assumption in optimizing the ratio: high-ratio theorems are scarce, hence worth prioritizing. [Inference] Whether that holds depends on how well high ratio actually coincides with "truly important."
🎯 A 27B Difficulty Predictor
To compute proof length, you must first know how hard a problem is; to judge a new theorem's value, you must estimate "how hard is it to prove, given a set of premises?"
The paper isolates this quantity as a primitive: proof difficulty, conditioned on a premise set. The authors trained a 27B-parameter model specifically to predict this difficulty, and report it is more accurate at predicting proof difficulty than frontier general-purpose models.
A specialized small model beating general large models on a single task is no longer surprising in other domains. Its significance here: difficulty prediction can be treated as an engineering component, plugged into loops of conjecture ranking and proof search. [Assessment]
🧬 From 91.9% to 30.6%
The paper's most striking number is a drop in overlap rate.
After optimizing with this metric, the fraction of model-generated theorems substantially or entirely overlapping Mathlib fell from 91.9% to 30.6%.
Mathlib is the Lean proof assistant's mathematics library: community-maintained, with detailed contribution guidelines and code style conventions, advanced via pull requests and Zulip collaboration, with several mathematicians among its core maintainers reviewing new results. A newly generated theorem that heavily overlaps existing content adds nothing to the library, even if machine-verified.
Going from 91.9% to 30.6% says two sides of one thing: the model is no longer merely reciting the mathematics it memorized. [Assessment]
| Metric | Before optimization | After optimization | |---|---|---| | Substantial/complete overlap with Mathlib | 91.9% | 30.6% | | Difficulty prediction model | none | 27B parameters | | Difficulty prediction accuracy | below frontier general models | paper claims above frontier general models |
🔁 What a Self-Expanding Library Looks Like
The paper's closed loop has four steps: generate candidate theorems, rank them by interestingness, prove the most promising batch, add the verified theorems to the library, then use the expanded library as the premise set for the next round of generation.
The paper positions this framework as a path toward a self-expanding, machine-verified mathematical library, with the keyword "without depending on human-given goals."
That is a big step. Almost all existing work in formalization libraries started with human-chosen goals and machine-executed proofs; handing over problem selection means handing "mathematical taste" — the most human-centered element — to a ratio. [Assessment]
🧭 Three Adjacent Signals in the Same Week
This paper did not appear in isolation. Three directionally related efforts from the same week provide context.
Feige's 1/e conjecture. According to an AI news aggregator, an arXiv preprint claims a short proof of the conjecture assisted by GPT-5.6 Sol, building on recent results by Vlassis and Thomas on finite-sample validity of distribution-free p-values. Another preprint gives a sharp small-deviation inequality, confirms the conjecture for δ ≥ 1 using the Grünbaum centroid halfspace theorem and generalizations by Letwin and Yaskin, with end-to-end Lean formalization. The aggregator notes several teams produced proofs along the same lines on the same day. [Quoted from aggregator; none peer-reviewed]
INRIA's graph theory attack. A team led by Emanuele Natale (INRIA, France) used LLMs to systematically attack 800+ graph theory conjectures, open-sourced in the Graph-Theory-LLM-Proofs repository. Reportedly 30+ conjectures received complete proofs or explicit counterexamples, some verified by human mathematicians, a few formalized in Rocq.
University of Washington Math AI Lab tools. Publicly released tools include an open-problem map placing 15,000+ unsolved problems semantically, and TheoremSearch. These address exactly the starting point of the previous two: where do problems come from.
Putting the three together, the shape is clear: the four stages — problem selection, problem solving, verification, library inclusion — each saw movement this week. [Assessment]
⚠️ Three Boundaries
1. The correlation between the interestingness ratio and downstream usefulness is the paper's own empirical result; no independent replication has yet been seen. 2. The drop in Mathlib overlap measures "novelty," not "importance." A new theorem may simply be a niche result in a niche direction. [Assessment] 3. All of these results are preprints. Formal verification blocks wrong proofs; it does not block "this proposition itself has no value."
In the broader context, the mathematics community's stance on AI in proving is diverging. On September 11, an open letter signed by 25 Fields Medalists including Terence Tao opposed treating the solving of hard open problems as a leaderboard benchmark for models; Epoch AI subsequently added a Human + AI label to FrontierMath, explicitly distinguishing human-in-the-loop results from autonomous AI claims. [Quoted from public reporting]
🔭 Things to Watch
- Third-party reuse of the difficulty predictor: whether the 27B model and its evaluation set are released determines whether it can become a public component.
- Independent verification of the interestingness ratio: does the correlation with downstream usefulness hold in other branches of mathematics?
- Beyond 30.6%: how low must residual overlap go, and does reducing overlap sacrifice provability?
- Peer review of the Feige conjecture preprints: how multiple same-day preprints establish priority is this round's most worth-following case in research ethics.
- First public output of a self-expanding library: what the first theorem set selected, proven, and banked entirely by this loop looks like.
- Adoption of the Human + AI label: whether other benchmarks follow, separating "AI-autonomous" from "human-led" results.
Sources
1. Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos, Julia Kempe, *Learning to Discover Interesting Mathematics*, arXiv:2609.28603, 2026-09-23 2. AGI Hunt aggregation of preprints on GPT-5.6 Sol and Feige's 1/e conjecture, 2026-09 3. AGI Hunt coverage of INRIA Emanuele Natale team's Graph-Theory-LLM-Proofs, 2026-09 4. University of Washington Math AI Lab public tools (open problem map and TheoremSearch) 5. Public reporting on the 25 Fields Medalists' open letter and Epoch AI's new Human + AI label, 2026-09