Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit

Formal theory shows infinite trivial output is provably necessary for AI systems generating valuable mathematics

A new arXiv paper models AI-assisted formal mathematics generation as a nested language-generation-in-the-limit problem, using a proof checker as a membership oracle and an adversarial enumeration of the mathematical literature as the signal for 'valuable' content. The authors prove a sharp dichotomy: generators emitting only finitely many trivial (correct but worthless) statements achieve at most α/2 coverage of unseen valuable mathematics, while allowing an infinite (but asymptotically vanishing) stream of trivia raises the optimum to 1−α/2. The central result is that a perfect verifier cannot substitute for mathematical taste, and the flood of certified-but-trivial output from AI proof systems is a provable mathematical necessity, not an engineering failure. The work formalizes the gap between formal verifiability and mathematical value, which is increasingly the binding constraint as AI-proof-assistant systems scale.