Learning to Discover Interesting Mathematics
Read the paperThis item is no longer on the current shelf. Its page remains available, and editorial corrections may be made. See what is featured now.
A proof-length objective guides theorem generation; its novelty measure is limited to the evaluated formal library.
What it does
The authors train a 27B model to estimate proof difficulty and use proof length relative to statement description length as an interestingness objective. Generated theorems have machine-checked proofs. In the evaluated cohort, an LLM judge classifies substantial or full Mathlib containment for 30.6% of trained-model statements versus 91.9% for the base model.
Why it matters
This offers a computable selection signal for formal discovery. The containment result is a judged library-overlap measure, not proof that every statement is new or valuable to mathematicians.
How it applies
Compare conjecture selection under the same proof-search budget. Check proofs, inspect overlap and ask whether the selected lemmas help subsequent work; the paper does not measure every kind of mathematical value.
The short version
A theorem can be valid without being worth adding to a library.
My take
I would use this as a candidate-ranking experiment, then require independent checks of overlap and downstream usefulness. A high proxy score would not settle adoption.
How it connects
- Treat proof checking as a correctness gate and library utility as a separate evaluation.
- Keep claims about applications outside formal mathematics conditional.
Bottom line
Test whether the ranking saves proof-search effort on your library. Primary paper.
Takeaways
- Interestingness is conditioned on the available premises and description vocabulary.
- The overlap comparison concerns substantial or full containment in Mathlib, judged by an LLM.
- Formal verification and usefulness are separate questions.
Historical Brendon Score: 8.5/10
Recorded for a previous shelf selection. Editorial corrections do not constitute a new assessment.
- Quality: 8.0/10 — base
- Authority: 7.0/10 — +0.20
- Freshness: 8.2/10 — +0.16
- Relevance: 8.0/10 — +0.00
- Corroboration: 2.1/10 — +0.16
- Sum: 8.52
- Total (rounded): 8.5/10
Why this is here
Independently surfaced by 1 community: HuggingFace Papers.
First seen: .