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

The paper introduces a model for generating valuable mathematics through nested language generation, utilizing a proof assistant as a membership oracle to differentiate between valuable outputs and trivial or hallucinated statements. It establishes a dichotomy in generator performance based on trivia count, showing that allowing infinite trivia can enhance coverage of valuable statements from an optimal density of $\alpha/2$ to $1-\alpha/2$. This research underscores the necessity of generating trivial statements in order to capture unrecorded valuable mathematics, highlighting a fundamental challenge in AI-driven mathematical generation systems.