A 27B model ranks theorems by usefulness, not just solvability
A new 27B model helps LLMs find mathematically interesting theorems, giving researchers a way to rank conjectures and guide proof search instead of solving only human-supplied problems. It scores a theorem by comparing its proof length with the length of its statement, then generates candidates, picks the strongest ones, and builds on a growing formal library. Optimizing that score cut substantial or full overlap with Mathlib from 91.9% to 30.6%.