MathLoopBench: Evaluating Agentic Mathematical Discovery Loops

Formal theorem-proving benchmarks hand the system a statement and ask for a proof. A mathematical discovery loop faces the decision before that: with no statement supplied, which propositions are worth proving? We introduce MathLoopBench, which measures this decision as target-blind theorem recovery. A loop starts from a small Lean 4 seed library and grows it under a fixed budget; a scorer rechecks every submitted theorem and reports the fraction of a hidden set of targets the loop recovered, against both proof attempts and model tokens. The score belongs to the whole loop, its conjecturing, proving, and orchestration, not to proof generation alone. The gap is large: the same prover solves 92.6% of the targets at solve@16 when handed their statements, while our reference loop, MDLoop, recovers 53.0% after 1000 attempts. This motivates improving conjecturing and orchestration. Under one contract, two different loops, MDLoop and CPL, are compared run by run over five seeds per domain. Still, across their runs, the two loops recover eight of the ten targets the prover missed when handed the statements.