27B math model cuts Mathlib overlap from 91.9% to 30.6%

Niket Patel, Julia Kempe and their coauthors want a computable answer to the question of whether an AI-generated theorem is worth anything. In a preprint posted to arxiv, they define "intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement," and report that it "correlates strongly with an extrinsic measure of the downstream utility of a theorem."

To operationalize the metric, the team trains a 27-billion-parameter model to predict proof difficulty conditioned on a set of premises. The abstract claims this system "predicts proof difficulty more accurately than frontier general-purpose models," though it does not name which frontier models were tested or by what margin.

The headline number is a shift in what the system generates. Optimizing for the interestingness score reduces "substantial or full overlap with Mathlib from 91.9% to 30.6%," which the authors read as evidence of "the creation of more out-of-distribution math" rather than a system that keeps rediscovering the standard Lean library.

The paper is direct about the ambition. Its framework, the authors write, "provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets."