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

arXiv: https://arxiv.org/abs/2606.14688 · HTML: https://mlsanity.com/paper/2606.14688/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 91 references that are in the map.
- First posted on arXiv 12 Jun 2026.

## Builds on (most cited first, 30 of 34)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Language Generation in the Limit](https://mlsanity.com/paper/2404.06757/) (2024)
- [Generation through the lens of learning theory](https://mlsanity.com/paper/2410.13714/) (2024)
- [Exploring Facets of Language Generation in the Limit](https://mlsanity.com/paper/2411.15364/) (2024)
- [Density Measures for Language Generation](https://mlsanity.com/paper/2504.14370/) (2025)
- [Generation from Noisy Examples](https://mlsanity.com/paper/2501.04179/) (2025)
- [Representative Language Generation](https://mlsanity.com/paper/2505.21819/) (2025)
- [Language Generation in the Limit: Noise, Loss, and Feedback](https://mlsanity.com/paper/2507.15319/) (2025)
- [(Im)possibility of Automated Hallucination Detection in Large Language Models](https://mlsanity.com/paper/2504.17004/) (2025)
- [On the Query Complexity of Verifier-Assisted Language Generation](https://mlsanity.com/paper/2502.12123/) (2025)
- [Safe Language Generation in the Limit](https://mlsanity.com/paper/2601.08648/) (2026)
- [Compression is all you need: Modeling Mathematics](https://mlsanity.com/paper/2603.20396/) (2026)
- [Mistake-Bounded Language Generation](https://mlsanity.com/paper/2605.10809/) (2026)
- [Agnostic Language Identification and Generation](https://mlsanity.com/paper/2601.23258/) (2026)
- [On Generation in Metric Spaces](https://mlsanity.com/paper/2602.07710/) (2026)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)
- [Contrastive Identification and Generation in the Limit](https://mlsanity.com/paper/2605.06211/) (2026)
- [On the Price of Privacy for Language Identification and Generation](https://mlsanity.com/paper/2604.07238/) (2026)
- [A Theory of Time-Sensitive Language Generation: Sparse Hallucination Beats Mode Collapse](https://mlsanity.com/paper/2605.11302/) (2026)

## Built on by (most cited first, 2 of 2)

- [Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarchy](https://mlsanity.com/paper/2609.10525/) (2026)
- [Hallucination Rates in Language Generation](https://mlsanity.com/paper/2607.23361/) (2026)

## Abstract (arXiv)

AI systems coupled to proof assistants now generate formal mathematics at scale, and the gap between what a checker can verify and what a mathematician would value has become the binding constraint. We model the generation of valuable mathematics as nested language generation in the limit: a verifiable formal language F, accessed through a membership oracle (the proof checker), contains an unknown valuable language H ∈ H revealed only through an adversarial enumeration of a core C subseteq H of exact density α (the literature). Every output is valuable (∈ H), trivial (∈ F setminus H), or a hallucination (notin F). We settle four questions. First, the verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wise by Angluin's condition. Second, the verifier does buy sound coverage, covering all unseen valuable statements while asserting only valid ones: possible with it, impossible without it; it relocates unavoidable errors from false to trivial. Third, and centrally, a sharp dichotomy on the tight family: generators emitting finitely many trivia achieve optimal coverage α/2, while any infinite trivia allowance, even at vanishing rate, jumps the optimum to 1-α/2 (both tight, for cores presented as the candidate intersection), and one generator attains both ends. The transition is in trivia count, not rate; the gap 1-α is the unrecorded mass. Fourth, both regimes instantiate in a compression model of mathematics. A perfect verifier cannot substitute for taste: the unbounded stream of correct-but-worthless statements is not an engineering accident but a provable necessity, since covering unrecorded valuable mathematics requires an infinite, but asymptotically negligible, stream of certified trivia.