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

AI systems paired with proof checkers can now verify mathematical correctness at scale — but verification alone doesn't guarantee value. This paper asks a deeper question: can an AI systematically discover genuinely new, worthwhile mathematics, rather than an endless flood of correct but trivial statements? The authors prove, using formal language theory, that generating non-trivial mathematics requires producing some trivia — it's mathematically unavoidable, not a design flaw. Crucially, a perfect verifier cannot substitute for mathematical taste. This has implications for automated theorem proving, AI-assisted research tools, and setting realistic expectations for what AI co-pilots for mathematicians can and cannot achieve. Authors: Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao Paper: https://arxiv.org/abs/2606.14688v1