The Future Is the Test: Library Abstractions for Mathematics Not Yet Written

The value of a mathematical abstraction lies in the mathematics it supports next. On major Mathlib refactors, adopted designs complete 60/60 use attempts against 29/60 for their predecessors, with no losses. We formulate future-use generalization (FUG) as evaluating abstractions on withheld mathematical uses in Lean. FUSE turns failures and recurring proof work on observed uses into revisions of shared statements. FutureUseBench connects historical designs, authored use graphs, and real-library replay to test these components separately. Across eight authored development targets, exposing use descriptions increases unseen declaration completion $2.28\times$. With accepted interfaces fixed, feedback on observed uses removes 81% of remaining declaration failures. Among jointly completed, source-screened uses, exposure reduces downstream source tokens by 16–27%, a proxy for adaptation burden. Proof dependence changes method rankings, and shared revisions can both enable reuse and lose interface acceptance. Reliable transfer to unseen proofs after revision remains open. These findings establish later mathematics as an executable test and a concrete design signal for abstraction.