arXiv CSopen access

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

Flood and Harvest The Provable Necessity of Trivia for Generating Valuable Mathematics

arXiv:2606.14688v1 [cs.LG] 12 Jun 2026

via the Lens of Language Generation in the Limit

1

Xiaoyu Li1

Andi Han2

Dai Shi3

Zheng Gao1

Jiaojiao Jiang1

Junbin Gao2

University of New South Wales {xiaoyu.li2, zheng.gao1, jiaojiao.jiang}@unsw.edu.au 2 University of Sydney {andi.han, junbin.gao}@sydney.edu.au 3 University of Cambridge [email protected] June 15, 2026

Abstract 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 ⊆ H of exact density α (the literature). Every output is valuable (∈ H), trivial (∈ F \ H), or a hallucination (∈ / 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. The flood of the title is that stream; the harvest is the unrecorded value that only the flood can buy. “ What, in fact, is mathematical discovery? It does not consist in making new combinations with mathematical entities that are already known. That can be done by any one, and the combinations that could be so formed would be infinite in number, and the greater part of them would be absolutely devoid of interest. Discovery consists precisely in not constructing useless combinations, but in constructing those that are useful, which are an infinitely small minority. Discovery is discernment, selection.” — Henri Poincaré ♢ ♢

Quoted from Poincaré’s discussion of mathematical discovery in Science and Method (1914).

1

Flood and Harvest

Contents 1 Introduction 1.1 New model: nested language generation in the limit . . . . . . . . . . . . . . . . . . . . 1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Technical overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3 4 5 6 6

2 The Model 2.1 Ground set, generation in the limit, and breadth . . . . . . . . . . . . . . . . . . . . . 2.2 Partial enumeration and the revealed core . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 The nested model: validity versus value . . . . . . . . . . . . . . . . . . . . . . . . . .

7 7 8 9

3 Main Results 3.1 Verification is not taste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Sound coverage: what the verifier does buy . . . . . . . . . . . . . . . . . . . . . . . . 3.3 The trivia phase transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10 11 11 13

4 Case Study: Instantiation in a Compression Model of Mathematics

18

5 Discussion

19

6 Outlook: We Must Generate. We Will Select.

21

A Notation

28

B Map of the Results

28

C Mathematical Background C.1 Monoids and canonical orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . C.2 The macro framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . C.3 The usage of ABFM models in the case study . . . . . . . . . . . . . . . . . . . . . . .

29 29 30 31

D Deferred Proofs D.1 Verification is not taste (Theorem 3.1) . . . . . . . . . . . . . . . . . . . . . . . . . . . D.2 The exhaustive generator and the separation (Theorem 3.2) . . . . . . . . . . . . . . . D.3 The race lemma (Lemma 3.5) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . D.4 Impossibility side of the dichotomy (Theorem 3.6) . . . . . . . . . . . . . . . . . . . . D.5 Achievability: sweep and the tight generator (Theorem 3.7) . . . . . . . . . . . . . . . D.6 The instantiation (Theorem 4.1 and Propositions 4.2 and 4.3) . . . . . . . . . . . . . . D.6.1 Abelian refinement chains (Theorem 4.1) . . . . . . . . . . . . . . . . . . . . . D.6.2 Free-monoid pairs (Proposition 4.2) . . . . . . . . . . . . . . . . . . . . . . . . D.6.3 Imprecision of exhaustive generation (Proposition 4.3) . . . . . . . . . . . . . .

31 31 33 35 37 38 40 40 41 43

E Summary of Oracle and Feedback Models

44

F Numerical Validation

45

G The Dichotomy by Hand: A Worked Miniature

46

H Additional Related Work H.1 AI for mathematics and automated discovery . . . . . . . . . . . . . . . . . . . . . . . H.2 Language generation in the limit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . H.3 Classical inductive inference and language identification in the limit . . . . . . . . . .

47 47 48 49

I

49

A Taxonomy of Generation in the Limit

J What This Says, and Does Not Say, to Prover Builders

52

K Discernment, Selection: A Prehistory of Mathematical Taste

53

2

Flood and Harvest

1

Introduction

Machine-generated mathematics has moved from aspiration to practice. Language models coupled to proof assistants are run as tireless provers, from GPT-f through HyperTree search to DeepSeekProver and Goedel-Prover (Lample et al., 2022; Lin et al., 2025; Polu and Sutskever, 2020; Xin et al., 2024); olympiad-level systems now solve hard competition problems (Chervonyi et al., 2025; Hubert et al., 2026; Trinh et al., 2024); AI-assisted discovery has produced genuine new mathematics (Davies et al., 2021; Georgiev et al., 2025; Romera-Paredes et al., 2024); large formalization efforts have put substantial bodies of mathematics into machine-checkable form (Aksenov et al., 2026; Avigad, 2023); and autonomous systems now generate conjectures and theory at scale (Barkeshli et al., 2026; Tsoukalas et al., 2025). The shared substrate is a membership oracle for a formal language, a checker that accepts a string exactly when it encodes a valid derivation, against which such a system can emit, one after another, an unbounded stream of statements each of which is, by construction, correct (see Ju and Dong (2026); Li et al. (2024) for surveys). Practitioners face a problem the empirical literature documents and laments without formalizing: the checker certifies validity, not value. It accepts a derivation; it does not certify that the theorem is worth proving, a distinction Thurston famously drew between proof and mathematical understanding (Thurston, 1994). A generator can therefore flood its output with statements that are formally impeccable and mathematically worthless, or it can aim instead at the conjectures a mathematician would care about and risk being wrong. And the flood is alarmingly cheap to manufacture: a short script written for this paper generated, and machine-verified, the statement Γ 12 π

2

+ e

iπ

+ 2 φ − φ −2 ζ(0) = exp

2

∞ X (−1)k+1 k=1

k

!

,

in which Euler’s identity, the golden ratio, the Gamma function, and the Riemann zeta function all make cameo appearances, and none is needed. The verification is instant; the mathematical content is 1 + 1 = 2. Nothing in the checker’s verdict distinguishes this confection from a theorem. The gap between what is verifiable and what is valuable is, in this record, the central bottleneck, and it has no formal account. In this paper we study this problem theoretically. We ask the question no prior model addresses. With a perfect verifier in hand, what can a generator provably guarantee about value, and what, if anything, does the verifier buy? We prove exactly what is and is not achievable. We work in the framework of language generation in the limit (Kleinberg and Mullainathan, 2024), extended to a nested pair of languages; the extension is the source of the new phenomena, so we describe it before stating results. The title names the two regimes this theory prices. The flood is the unbounded stream of certified trivia that any broad generator must emit; the harvest is the unrecorded valuable mathematics that only such a stream can reach. Tao (2025) envisions machine assistance under which “mathematical explorations become possible at scales that are not currently feasible”: fields that today “study one or two equations at a time” may come to “study hundreds of equations at once.” Our results price that vision. Explored at scale, mathematics yields its unrecorded value only to generators that flood, and the flood can be made certified-true and asymptotically negligible in rate, but never finite (Figure 1). The boundary this draws for system design is clean: verification decides where exploration may step, while examples of recorded value decide where it should, and no amount of the former substitutes for the latter. The remainder of this introduction makes the model precise, states the four results, and locates them in the literature. 3

Flood and Harvest

U : all statements Whitehead problem

CH

(independent of ZFC)

hallucinations stopped here

(independent of ZFC)

F : provable, machine-checkable

×

1111111112 = 12345678987654321 digits 762–767 of π read 999999

1 + 2 + · · · + 100 = 5050 the 1000th prime is 7919

generator + verifier 1F

the flood: valid but worthless (F \ H)

H: valuable (unknown)

tomorrow’s theorems FLT (1995)

2592 = 25 · 92

PNT (1896)

this paper? (pending peer review)

Green–Tao (2008) Galois theory (1846)

2+2=5 C: the literature (density α)

Euler’s sum-of-powers conjecture (false: 275 +845 +1105 +1335 = 1445 )

the harvest: unrecorded value H \ C, mass 1 − α

Figure 1: The nested worlds of machine-generated mathematics, with inhabitants. The verifier guards the boundary

of F and nothing more (Theorem 3.1): within F it cannot tell a checkable banality from a theorem worth recording. Outside F live the falsehoods, from the crude to the seductive (Euler’s sum-of-powers conjecture stood for two centuries before its counterexample), and, more subtly, the independent statements: validity is always relative to a fixed formal world, and neither the continuum hypothesis nor the Whitehead problem is decided by ZFC. The literature C records a density-α fraction of the valuable language H; covering the rest, the harvest, provably requires emitting infinitely many statements from the flood F \ H (Corollary 3.10). Placement of examples is illustrative; the identity 2592 = 25 · 92 is Dudeney (1917)’s “printer’s error”, charming, checkable, and still worthless, and this paper itself waits at the edge of C, pending peer review. Color code, here and throughout: blue for the formal world, gold for the valuable, red for the false or adversarial, gray for the trivial.

1.1

New model: nested language generation in the limit

Fix a countable ground set U of strings with a canonical order. An instance is a pair (F, H) with H ⊆ F ⊆ U , both infinite: the formal language F is the verifiable ambient (membership in F is decided by an oracle, the proof checker), and the valuable language H is the target, which the generator never sees directly. The adversary draws (F, H) from a countable collection, grants the generator a membership oracle for F , and enumerates a core C ⊆ H of lower density α, the literature, which records only a fraction of what is valuable. Round by round the generator reads the enumerated prefix St , queries the oracle, and outputs a fresh string at ∈ / St . Each output falls into exactly one of three modes (Figure 1): mode

condition

meaning

hallucination triviality valuable

at ∈ /F at ∈ F \ H at ∈ H \ St

not even valid (the classical failure) valid but worthless (the new failure) new and valuable (hence also valid)

We measure coverage by the lower density c = d(O ∩ H, H) of the valuable statements the run eventually produces, in the limit-set sense of Kleinberg and Wei (2025). The verifier eliminates one failure mode (no output need ever be a hallucination), and the question becomes how the remaining two, triviality and missed value, trade against each other. 4

Flood and Harvest

1.2

Contributions

We settle four questions; the headline is the third. 1. Verification is not taste (Theorem 3.1). With a membership oracle for F , the collections admitting generation with exact (resp. approximate) breadth (outputs eventually covering all unseen valuable statements) are exactly those admitting it in the oracle-free model, characterized fiber-wise by Angluin’s tell-tale condition (resp. its weak form). The verifier’s entire informational content, for the in-the-limit breadth goal, is identification of the ambient F ; within a fiber of candidates sharing one F it discriminates nothing. Taste must be learned from examples, never from a checker. 2. What the verifier does buy (Theorem 3.2). The oracle is not useless: it characterizes sound coverage: covering every unseen valuable statement while asserting only valid ones. With the verifier, the exhaustive generator Gn = F \ Sn achieves sound coverage for every countable collection; without it, there is a collection on which no generator can. The verifier thus relocates the unavoidable errors of broad generation from false (∈ / F ) to merely trivial (∈ F \ H); it does not reduce their number, and it cannot locate value. 3. The trivia dichotomy (Lemma 3.5, Theorem 3.6, Theorem 3.7, Corollary 3.10). This is the headline. The KW α/2 frontier is exactly the finite-trivia-count slice of a count dichotomy: on the tight family Hα with its canonical core presentation (the revealed core C ⊆ K is the candidate intersection), infinite allowance, even at vanishing rate, yields 1 − α/2, tight, with a matching necessity theorem (any generator exceeding α/2 must emit infinitely many trivia). The tight family has revealed core of exact density α, and the phase transition separates two populations of generators: trivia allowance

optimal coverage at truth K ′

tight?

finitely many infinitely many

α/2 1 − α/2 (core = candidate intersection, C ⊆ K)

yes (Theorems 3.6 and 3.7) yes (Theorems 3.6 and 3.7)

A single sound generator G∗ attains both ends at every realized truth, with zero trivia when the record is incomplete (Theorem 3.7). The transition is in the trivia count, not its rate: any √ infinite allowance suffices even at trivia count ⌊ N ⌋ in the first N rounds, i.e. rate O(N −1/2 ). The gap 1 − α between the two optima is exactly the unrecorded mass F -valuable but outside the core. Thus an unbounded stream of correct-but-worthless theorems is necessary for any generator covering more than α/2, and sufficient at asymptotically negligible rate. Beyond the tight family, the sweep is universal: it gives c ≥ 1 − d(C, H) for every countable collection. 4. Instantiation in a compression model of mathematics (Theorem 4.1, Proposition 4.2, Proposition 4.3). We realize the dichotomy inside the macro-dictionary model of Aksenov et al. (2026). Structured abelian refinement chains are identifiable with singleton tell-tales: in the structured regime, valuable generation needs no trivia at all (Theorem 4.1). Free-monoid name-cut dictionary pairs realize the tight family at every rational α, and an unbounded-cut construction realizes the dichotomy’s extreme 0-vs-1 point: finite-trivia coverage 0 against sweep coverage 1 (Proposition 4.2). The exhaustive generator’s precision is polynomially small in radius, while the sweep’s precision tends to 1 (Proposition 4.3). We use this model as substrate and motivation, not as a source of borrowed theorems.

5

Flood and Harvest

1.3

Technical overview

The four results draw on three mechanisms. Fixed-advice relativization carries Theorem 3.1. Within a fiber, the candidates sharing one ambient F , the oracle is one fixed function 1F , so a relativized generator’s adaptive query tree, of finite depth, resolves to an ordinary set-valued function of the enumerated prefix. The oracle-free characterizations of Kalavasis et al. (2026) then apply verbatim, and a one-round identification stage locates the correct fiber. We say plainly that this transfer is light by design: its easiness is the message, that verification is information-theoretically orthogonal to taste. The technical weight lives in the next two mechanisms. A sandwich-exclusion lemma, deployed two-sidedly, carries the separation Theorem 3.2. The lemma itself is a three-line containment argument: on a nested Gold chain Hj ↑ H∞ with fattened ambients, no single output set can sound-cover both a chain member and the union against the same seen-set. The two-sidedness lives not in the lemma but in how the adaptive phase construction deploys it: forcing any oracle-free generator to fail on one or the other infinitely often, so that soundness must be denied above and below the same transcript. A race lemma and a sweep pointer carry the dichotomy. The lower bounds (Lemma 3.5, Theorem 3.6) come from a racing adversary that enumerates the core from the bottom, so that any generator and the adversary read the same transcript under two different truths, capping coverage at 1/2 along the raced core and at 1 − α/2 overall—a same-transcript two-readings cap. The upper bounds (Theorem 3.7) come from interleaving a sparse sweep schedule into the race: because density is a property of the limit set, not of any per-prefix deadline, a vanishing-rate sweep of the candidate intersection eventually claims every never-enumerated valuable string, recovering 1 − α/2. The matching constructions of Theorem 4.1 and Proposition 4.2 verify that the abstract interface the lower bound requires is met by genuine compressible-language families.

1.4

Related work

Generation in the limit. The model originates with Kleinberg and Mullainathan (2024): every countable collection is generable in the limit, in contrast to Gold–Angluin identification, but breadth is sacrificed. The breadth resource was then mapped: Kalavasis et al. (2025, 2026) characterize exact and approximate breadth by Angluin’s tell-tale condition and its weak form, the characterizations we relativize in Theorem 3.1. Their pivotal positive result, that positive and negative examples of the target restore breadth for every collection (Kalavasis et al., 2025, Thm. 3.13), marks precisely the contrast we exploit: true negative examples collapse the Angluin boundary, whereas our verifier supplies negatives only outside F and none in the grey zone F \ H, so it cannot move the boundary at all. The oracle results of the line concern different oracles: Charikar and Pabbaraju (2025) show membership queries to collection members are insufficient, and Bai et al. (2026) show finite same-level feedback is worth nothing; our oracle queries an ambient superset, a different construction with a different verdict. Density. Kleinberg and Wei (2025) introduce the limit-set density we use and achieve a universal positive density. Kleinberg and Wei (2026b) sharpen this: full enumeration permits tight lower density 1/2, and partial enumeration of a core of density α permits the tight bound α/2. We show that α/2 is exactly the finite-trivia regime of our larger dichotomy; their model reveals a fraction of the same target, whereas our nesting sits between a target and an ambient, not between a revealed and an unrevealed part of one language. Kleinberg and Wei (2026a) establish a Banach-density dichotomy by Cantor–Bendixson rank, which we cite as a caution for embedded instantiations.

6

Flood and Harvest

The errors-buy-coverage moral, elsewhere. Ganju et al. (2026) reach a kindred slogan, that sparse hallucination beats mode collapse, in a timeliness model with no nested pair, no verifier, and no distinction between trivial and false. Anastasopoulos et al. (2026) study the opposite geometric task, avoiding a harmful sublanguage rather than hitting a valuable one. Verifier-assisted decoding. Botta et al. (2025) also place a verifier beside a generator, but ask a different question: a process verifier supplies prefix-completability for constrained decoding, and the results are computational query complexity, with no unknown target and no breadth or density. We share a word, not a model. Other variants. The line includes generation through a learning-theoretic lens (Raman et al., 2025), union-closedness failures (Hanneke et al., 2025), representative generation (Peale et al., 2025), noisy examples (Li and Zhang, 2026; Raman and Raman, 2025), Pareto-optimal non-uniform generation (Charikar and Pabbaraju, 2026), contamination (Mehrotra et al., 2026a), privacy (Mehrotra et al., 2026b), metric spaces (Li et al., 2026a), agnostic generation and identification (Høgsgaard and Pabbaraju, 2026), and complexity barriers (Arenas et al., 2026). None carries a verifiable ambient or the triviality mode. Mathematics as structured strings. Our instantiation is built on the compression model of Aksenov et al. (2026) and the structural program of Barkeshli et al. (2026); we use the model, not its theorems. Related empirical and conceptual work on the structure and interestingness of mathematical corpora (Colton et al., 2000; Herrmann and Schmidhuber, 2026; Tsoukalas et al., 2025; Wernhard and Zombori, 2025) motivates the value question but proves no generation theorems. The empirical AI4Math line, its benchmarks and its autoformalization and proof-search pipelines (Jiang et al., 2023; Yang et al., 2023; Zheng et al., 2022), supplies exactly the phenomena our model formalizes. We defer the discussion of classical inductive inference and language identification in the limit, the broader line of work on language generation in the limit, and practical developments in machinegenerated mathematics to Section H.

2

The Model

We pose the model before stating any result, because every answer below changes with it. The objects are languages (subsets of a fixed countable universe), the protocol is adversarial enumeration in the limit, and the question is how much of a hidden valuable language a generator can cover without ever leaving a fixed formal one.

2.1

Ground set, generation in the limit, and breadth

Fix a countable ground set U of statements with a fixed canonical total order ≺, written x1 ≺ x2 ≺ · · · . For an infinite L ⊆ U we write L[1. . .M ] for the set of its first M elements under ≺ (so L[1. . .M ] is always an initial segment of L in ≺-order, and indexing is 1-based: L[1. . .1] = {min≺ L}). A language is an infinite subset of U ; all languages in this paper are infinite unless stated otherwise. The Kleinberg–Mullainathan protocol. We use the generation-in-the-limit protocol of Kleinberg and Mullainathan (2024). An adversary fixes an unknown target language H and a Kleinberg– Mullainathan (KM) enumeration of it: an infinite stream w1 , w2 , . . . whose set of values is exactly H (every element of H appears, repetitions allowed). At round t the generator has seen the prefix and we

7

Flood and Harvest

write St := {w1 , . . . , wt } for the seen-set. The generator must commit to an output before round t + 1. Two output conventions appear in the literature, and we keep both, in disjoint roles. Set-valued generators (breadth; KMV conventions). A set-valued generator G maps the seen-set to a set Gn (Sn ) ⊆ U ; this is the convention of Kalavasis et al. (2026) (hereafter KMV), used for the characterization results of Sections 3.1 and 3.2. We say G achieves exact breadth in the limit on H if there is n∗ with Gn = H \ Sn for all n ≥ n∗ (it outputs all and only the unseen valuable statements), and approximate breadth in the limit if eventually Gn ⊆ H and |H \ Gn | < ∞. No computability is assumed of G: it is an arbitrary function of the prefix (KMV Remark 2.3). Element-based generators and the limit set (KW conventions). An element-based generator maps the seen-set to a single new statement at = G(St ) ∈ U with at ∈ / St ; this is the convention of Kleinberg and Wei (2026b) (hereafter KW), used for the density results of Section 3.3. The object of study over an infinite run is the limit set of all outputs, O := { at : t ≥ 1 },

(2.1)

the set of all statements the generator ever emits across the entire run (KW Definition 1.1). We emphasize that O is a property of the whole infinite run, not of any finite stage. To measure how much of a language a set covers we use prefix densities in the canonical order: for L′ ⊆ L, |L′ ∩ L[1. . .N ]| , N →∞ N

|L′ ∩ L[1. . .N ]| , N N →∞

d(L′ , L) := lim inf

d(L′ , L) := lim sup

(2.2)

writing d(L′ , L) for the common value when the limit exists. Generators in this mode are deterministic. Angluin’s conditions. The combinatorial quantity that controls breadth is Angluin’s tell-tale condition (Angluin, 1980). A countable collection H of languages satisfies Angluin’s condition if every L ∈ H has a finite tell-tale TL ⊆ L such that no L′ ∈ H with TL ⊆ L′ is a proper subset of L. It satisfies the weak Angluin condition if the tell-tale separates L from every L′ ∈ H with |L \ L′ | = ∞ rather than from every proper subset. These are exactly the conditions under which a Gold-style ascending chain S L1 ⊊ L2 ⊊ · · · with union j Lj in the collection fails to be identifiable, since every finite subset of the union lies in some proper sub-language of the chain (Gold, 1967).

2.2

Partial enumeration and the revealed core

The density results take place in KW’s partial model (Kleinberg and Wei, 2026b), which weakens the protocol in exactly the way the mathematical reading demands: the adversary need not enumerate all of H. Instead the adversary enumerates an infinite revealed core C ⊆ H (the “literature”: the valuable statements actually written down) and may leave the rest of H forever unseen. We parametrize the core by its lower density in the target, α := d(C, H), (2.3) and speak of an instance (H, C, enumeration) as legal if the enumeration is a repetition-free listing whose value-set is C. The relevant restated results are the following. We restate both results verbatim, version-locked to the public preprint, so the later argument can quote them with no paraphrase. In their statement, generation in the limit with partial enumeration means that “for some time t∗ , its outputs at satisfy at ∈ K − St for all t ≥ t∗ ” (Kleinberg and Wei, 2026b, §1), where K is the true language and St the enumerated prefix.

8

Flood and Harvest

Fact 2.1 (Partial-enumeration generation; (Kleinberg and Wei, 2026b, Theorem 1.6 in arXiv version)). There is an algorithm A that achieves generation in the limit with partial enumeration with the following guarantee: “for any adversarial enumeration E of an infinite subset C of one of the languages K ∈ X such that C has lower density at least α > 0 in K, the set of output strings O(E, A) [. . . ] has a lower density in K that is at least α/2.” Moreover, “α/2 also serves as an upper bound on the lower density achievable by any algorithm.” In our notation: for every countable collection X there is an element-based generator with d(O, H) ≥ 12 d(C, H) on every legal instance, and from some round t∗ on it outputs only elements of H. Fact 2.2 (Chain validity in the partial model; (Kleinberg and Wei, 2026b, Lemma 2.5(1) in arXiv version)). For the identified-intersection sequence I (t) that KW’s generator maintains, “there is a finite time T such that after which all the identified intersection I (t) are valid,” where valid means I (t) ⊂ K. The statement and its proof are in the partial-enumeration model. In our notation: there is a finite round T0 with I (t) ⊆ H for all t ≥ T0 .

2.3

The nested model: validity versus value

We now state our contribution to the model. Mathematical generation distinguishes two notions that the single-language model conflates: a statement can be valid (formally provable, machine-checkable) without being valuable (worth proving). We formalize this by nesting. Definition 2.3 (Pair model). A pair model is a countable collection P = {(Fi , Hi )}i of pairs of infinite languages with Hi ⊆ Fi ⊆ U . We call Fi the formal language (its membership oracle is a proof checker) and Hi the valuable language (the unknown target). The fiber over a set F is PF := { Hi : Fi = F } ,

(2.4)

the collection of candidate targets sharing the formal world F as a set. The adversary picks an index z, fixes (F, H) = (Fz , Hz ), and presents an enumeration of its core (full enumeration of H in the breadth setting). Definition 2.4 (Verifier oracle). A relativized (verifier-assisted) generator may, in each round, issue finitely many adaptive membership queries to the indicator 1F of the true formal language (a perfect proof checker for the realized ambient) before producing its output. The query budget per round is finite but unbounded; no computability is assumed (KMV Remark 2.3 conventions). The adversary is non-effective: it may decide infinitary conditions on the generator’s behavior. This is the standard convention for impossibility results in this line (Kalavasis et al., 2026). Definition 2.5 (Error trichotomy). At a round in which the generator emits a, with true pair (F, H) and seen-set St , the output is a hallucination if a ∈ / F (formally false), a triviality if a ∈ F \H (valid but worthless), and valuable if a ∈ H \ St (a genuinely new valuable statement; being in H ⊆ F , it is in particular valid). Throughout, valid refers to membership in the formal world F ,

9

Flood and Harvest

valuable to membership in the target H. The triviality rate through round N is trvN :=

|{ t ≤ N : at ∈ F \ H }| , N

(2.5)

and the trivia count is |O ∩ (F \ H)|. We distinguish count from rate throughout: a generator may emit infinitely many trivia at rate tending to 0. Definition 2.6 (Coverage, soundness, sound coverage). In the density setting, the coverage of a generator at truth H is c := d(O ∩ H, H), the lower density of the valuable statements it emits. A generator is sound if it never hallucinates: at ∈ F for all t, i.e. O ⊆ F . A set-valued generator achieves sound coverage in the limit on (F, H) if there is n∗ with H \ Sn ⊆ Gn (Sn ) ⊆ F

for all n ≥ n∗ :

(2.6)

it covers every unseen valuable statement while asserting only formally valid ones. Sound coverage is the natural “cover everything true and worthwhile, hallucinate nothing” goal; (2.6) sandwiches the output between the unseen value (lower) and the formal world (upper). The trichotomy of Definition 2.5 is what makes the nested model richer than the single-language one: errors no longer collapse to a single kind, and Section 3.2 shows the verifier acts precisely on which kind occurs. Restated characterizations (cited facts). The breadth results of Section 3.1 reduce to KMV’s oracle-free characterizations, which we use verbatim. Fact 2.7 (Breadth characterizations; (Kalavasis et al., 2026, Theorems 3.3 and 3.8)). A countable collection H admits a set-valued generator achieving exact breadth in the limit if and only if H satisfies Angluin’s condition (Theorem 3.3), and admits approximate breadth in the limit if and only if H satisfies the weak Angluin condition (Theorem 3.8). The bridge between modes. The two output conventions are reconciled by the standard setversus-element bridge (a KW analogue of KMV Lemma 2.3): a set-valued breadth statement and an element-based density statement about the same family agree on which statements are eventually emitted. We use set-valued generators only in Sections 3.1 and 3.2 (where the question is whether a family is coverable) and element-based generators only in Section 3.3 (where the question is how much of it is covered).

3

Main Results

We organize the results around one question: in the nested model, what does a perfect verifier buy, and what is the price of covering more value than the verifier alone can locate? Section 3.1 shows the verifier does not buy taste: breadth is governed by the same Angluin condition as without it. Section 3.2 shows what it does buy: sound coverage, achievable for every model with the verifier and impossible in general without it, by relocating errors from false to trivial. Then Section 3.3 prices that relocation exactly — a phase transition in trivia count — and Section 4 instantiates the whole picture as a case study in a compression model of mathematics.

10

Flood and Harvest

3.1

Verification is not taste

The first result locates the entire information content of a perfect verifier, for the breadth goal. One might hope that a proof checker, by certifying validity, helps a generator find value, distinguishing the valuable target H from the worthless remainder F \ H. It does not. The verifier’s answers depend only on the formal world F , which is shared across a fiber; within a fiber it supplies zero bits about which candidate is the true target. Breadth is therefore governed, fiber by fiber, by exactly the Angluin condition of the oracle-free model. Theorem 3.1 (Verification is not taste). Let P = {(Fi , Hi )} be a countable pair model (Definition 2.3), with a relativized generator (Definition 2.4) that queries the perfect verifier 1F . (a) Exact breadth in the limit on P is achievable if and only if every fiber PF satisfies Angluin’s condition. (b) Approximate breadth in the limit on P is achievable if and only if every fiber satisfies the weak Angluin condition. (c) In the single-ambient case Fi ≡ F , the relativized characterization coincides with the oraclefree characterization of Fact 2.7. In the multi-ambient case the verifier’s entire information content, for the in-the-limit breadth goal, is exactly ambient identification: locating which F is realized, after which it adds nothing. (d) (Zero-discrimination.) For Hi , Hj in the same fiber the oracle is the identical function 1F ; the realized query path and output at any prefix Sn are identical across the two instances. Every behavioral distinction within a fiber is driven by the enumeration alone. Proof sketch. For necessity, restrict the adversary to one fiber: the oracle is then a single fixed function, so stripping it yields an ordinary set-valued generator that would have to beat Fact 2.7 on a violating fiber. For sufficiency, a sample-independent first stage queries canonical points to identify the ambient F in finite time, after which a fixed per-fiber breadth generator (which exists by Fact 2.7) runs to completion. Part (d) is immediate from 1Fi = 1Fj . Full proof in Section D.1. Part (c) holds because the verifier’s answers are determined by F alone: in a single-ambient model F is known a priori, and within a fiber the oracle discriminates nothing (part (d)). Note also that (c) is scoped to breadth: for other goals, such as sound coverage in Section 3.2, the verifier does strictly more. The contrast that makes (c) sharp: a single negative example inside F \ H would collapse the Angluin boundary entirely, but the verifier returns only “valid” on all of F and so never supplies one. Verification certifies the world; it does not reveal the worth of a statement within it.

3.2

Sound coverage: what the verifier does buy

If the verifier does not buy taste, what does it buy? Exactly sound coverage, and exactly by relocating unavoidable errors. With the verifier, the exhaustive generator Gn = F \ Sn already sound-covers every pair model: it asserts all unseen formal statements, hence all unseen valuable ones, and never a falsehood. Without the verifier no such guarantee is possible in general: there is a pair model on which no oracle-free generator sound-covers. The price the exhaustive generator pays is visible in the trichotomy: when F \ H is infinite, F \ Sn contains infinitely many trivia. The verifier has not removed the errors; it has moved them from the false region U \ F into the trivial region F \ H.

11

Flood and Harvest

demand of the union: G ⊇ L∗ \ S, all but finitely many L∗ =

G⊇ S (finite)

S j

Hj

(truth (F∞ , L∗ ))

⊊ ··· ↗ H3 , missing R≥3 ⊊ H2 , missing R≥2 ⊊

demand of the chain element: G ⊆ Hj — yet the band covers the tail: the infinite R≥j must hide inside the finite S: contradiction (Lemma D.2). H1 , missing R≥1

Lemma D.3: every finite S sits inside some chain element, so the adversary can pose the dilemma at ever-larger j, forever.

Figure 2: The engine of the separation. The targets form a Gold chain H1 ⊊ H2 ⊊ · · · (bars) with union L∗ (top);

each chain element misses an infinite tail R≥j (hatched). Sound coverage of the union forces the output set G (dashed band) to cover all of L∗ but the finite seen-set; sound coverage of a chain element forces the same G inside Hj , i.e. off its tail. The band over the hatched region (outlined) is the contradiction (Lemma D.2), and non-identifiability (Lemma D.3) lets the adversary pose the dilemma infinitely often.

Theorem 3.2 (The exhaustive generator and the separation). In the pair model with the protocol of Definition 2.3: (a) (Exhaustive generator) With the verifier 1F , the generator Gn = F \ Sn achieves sound coverage in the limit on every countable pair model: at every round, it has zero hallucination, and (when F \ H is infinite) infinitely many trivia. (b) (Separation) There is a countable pair model P † (all languages infinite, every Fi \ Hi infinite) on which no oracle-free set-valued generator (an arbitrary function of the prefix) achieves sound coverage in the limit. (c) The verifier strictly enlarges the class of pair models admitting sound coverage, from a proper subclass to all of them; this is in contrast to breadth, where within a fiber it adds nothing (Theorem 3.1(c)). Proof sketch. Part (a) is immediate from H ⊆ F . For (b), the model P † is built on a Gold-style chain H1 ⊊ H2 ⊊ · · · with union L∗ in the collection. A sandwich-exclusion lemma (Lemma D.2; Figure 2) shows no output set can sound-cover both the union (F∞ , L∗ ) and a chain element (Fj , Hj ) against the same finite seen-set; a fresh-index lemma (Lemma D.3) keeps the chain non-identifiable. An adaptive phase construction then forces any oracle-free generator to fail on one of the realized instances; the construction is a non-effective adversary, the standard convention for impossibility results in this line (Definition 2.4). Part (c) combines (a) and (b). Full proof in Section D.2. Remark 3.3 (Two regimes in part (c)). Where the oracle identifies the ambient (and hence the target), as on P † , whose fibers are singletons, it suffices for sound coverage, and its absence makes sound coverage impossible. Within a non-singleton fiber, by contrast, the oracle adds nothing about which target is valuable (Theorem 3.1(d)), so there its power is exactly to keep the unavoidable

12

Flood and Harvest

optimal coverage c∗ G∗ (Theorem 3.7)

1 − α/2 jump = 1 − α the unrecorded mass d(H \ C, H)

KW frontier (Fact 2.1)

α/2

finite count

infinite count (any rate, even → 0) trivia allowance

Figure 3: The trivia phase transition (Corollary 3.10). The optimum jumps by exactly the unrecorded mass 1 − α

as the trivia allowance crosses from finite to infinite count; the rate at which trivia are emitted is irrelevant, and the right endpoint is attained by the single generator G∗ at vanishing rate. The colors are the title’s: blue for the raced core, gold for the harvested surplus.

overshoot inside F : relocating errors from false to trivial, reducing neither their number nor locating value.

3.3

The trivia phase transition

Throughout this subsection the ambient is F = N and the verifier is the constant function: the dichotomy is a verifier-free theorem about nested targets. The verifier’s role in the paper is settled by Theorems 3.1 and 3.2, and what follows quantifies the value/trivia tradeoff that remains after verification is granted. We now price the relocation exactly, in the partial (density) model. The setting is a single family on which the optimal guaranteed coverage is determined — and on which a sharp dichotomy appears: with only finitely many trivia the optimum is α/2, and allowing infinitely many trivia (even at rate tending to 0) jumps it to 1 − α/2. The transition is in trivia count, not rate. The tight family. We work over U = N in numeric order. Let K ′ := {evens} with K ′ [j] = 2(j − 1) be the formal world’s coverable part, and for a target density α ∈ (0, 1) define K := { K ′ [⌈k/α⌉] : k ≥ 1 } ⊊ K ′ ,

D := K ′ \ K,

F = N.

(3.1)

The family is Hα := {K, K ′ }, with K the sparse revealed target and K ′ the full coverable world. The point of (3.1) is that it realizes exact density for every real α, not merely rational α: |K ∩ K ′ [1. . .N ]| = ⌊αN ⌋

for all N,

hence

d(K, K ′ ) = α exactly,

(3.2)

and moreover K ∩ K ′ [1. . .N ] = K[1. . .mN ] with mN = ⌊αN ⌋, while F \ K ′ = {odds} is infinite. The two readings K and K ′ share a single transcript when the adversary enumerates K, which is what makes the caps bind for every generator. Here K plays the role of the valuable target H, K ′ that of the coverable part of F , and F \ K ′ (the odd column) is the inexhaustible trivia reservoir; the verifier is inert since F = N is known. The lower bounds rest on a self-contained race lemma (Figure 4). It says two things at once: a generator following a greedy “race” rule covers at least half of a target, and an adversary running a “racing” enumeration caps every generator at half.

13

Flood and Harvest

adversary AK : enumerates the least unused element, one per round generator: outputs the least unused element of K, one per round K[1]

K[2]

K[3]

K[4]

K[5]

K[6]

K[7]

K[8]

K[9] K[10] K[11] K[12] K[13] K[14]

···

at rounds t = 2n : re-enumerate a generator-claimed element (keeps the enumeration complete; only O(log) many) every prefix K[1. . .M ] splits M ± O(log M ) each: the cap (R2) and the share (R1) 2

Figure 4: The race on the canonical order of K (Lemma 3.5). Each round the adversary enumerates one element

and the generator outputs one, so every prefix splits roughly in half: no generator beats 1/2 on a raced core (R2), and the greedy racer secures 1/2 against every enumeration (R1). The power-of-two recycling steps keep the adversary’s stream a legal full enumeration at a cost of O(log M ) per prefix.

Definition 3.4 (The racing adversary). For infinite K ⊆ U , the racing adversary AK enumerates, at every round t ̸= 2n , the ≺-least element of K \ (St−1 ∪ Ot−1 ) (the least string unused by either side), and at every round t = 2n the ≺-least element of (Ot−1 ∩ K) \ St−1 , recycling a generator-claimed element so that the enumeration stays complete (falling back to the fresh rule if no such element exists). Lemma 3.5 (Race lemma). Let K ⊆ U be infinite and let Trace ⊆ N have density 1, with w(t) := t − |Trace ∩ [1 . . . t]| = o(t). (R1) (Greedy cover) If at every t ∈ Trace the generator outputs the ≺-least element of K \(St ∪Ot−1 ), then against every adversary enumeration, |O ∩ K[1. . .M ]| ≥ 12 (M − w(τM ) − 1) for all M , where τM is the index of the M -th race round; hence d(O ∩ K, K) ≥ 1/2. (R2) (Racing cap) The racing adversary AK of Definition 3.4 is a legal repetition-free enumeration of K. Against it, every generator satisfies |O ∩ K[1. . .M ]| ≤ M/2 + log2 M + 3 for M ≥ 2; hence d(O ∩ K, K) ≤ 1/2. Proof sketch. For (R1), at any race round with K[1. . .M ] not yet resolved the greedy output is a new element of O ∩ K[1. . .M ] (the ≺-least unresolved element of K lies in the downward-closed K[1. . .M ]); counting contributions against “steals” into the seen-set gives the bound. For (R2), the racing adversary alternates fresh enumeration with recycling the generator’s hoarded elements; an injection from output-elements to fresh-enumerated elements, with O(log M ) exceptions at powers of two, gives the cap. Full proof in Section D.3. The race lemma drives the impossibility side of the dichotomy. It establishes that on Hα no generator can exceed 1 − α/2 in coverage, and that a generator confined to finitely many trivia cannot exceed α/2. Theorem 3.6 (Impossibility side of the dichotomy). On the tight family Hα of (3.1), with deterministic element-based generators and limit-set coverage: (a) (Race cap) For every deterministic generator there are two legal instances of Hα sharing one transcript (the adversary is AK inside K), with coverage at most 1/2 at truth K and at most

14

Flood and Harvest

one interaction: the racing stream inside K, one limit set O w1

w2

w3

w4

w5

w6

w7

w8

···

Reading 2: truth K ′ . E is a partial enumeration: core C = K, density α. Cap: c ≤ (1 − α) + α/2 = 1 − α/2.

Reading 1: truth K. E is a full enumeration of K. Race cap (R2): d(O ∩ K, K) ≤ 1/2.

the generator cannot tell the readings apart, so both caps bind the same run (and finitely many trivia under Reading 1 forces |O ∩ D| < ∞ under Reading 2: the α/2 cap)

Figure 5: One transcript, two readings (Theorem 3.6). The racing stream inside K is simultaneously a legal full

enumeration of K and a legal partial enumeration of K ′ with core K. A deterministic generator produces one limit set, so the race cap binds at truth K and the 1 − α/2 cap at truth K ′ ; finitely many trivia at the first reading collapse the second to α/2.

1 − α/2 at truth K ′ (revealed core C = K, density α). Hence no generator guarantees coverage exceeding 1 − α/2 on Hα , nor exceeding 1/2 at truth K. (b) (Finite-trivia cap) Every deterministic generator that emits finitely many trivia on every legal instance has coverage at most α/2 on the truth-K ′ racing instance. (c) (Necessity of trivia) Any generator guaranteeing coverage exceeding α/2 on all of Hα emits infinitely many trivia on some instance; with Theorem 3.7(iii), α/2 is exactly the finite-trivia frontier. The caps bind per instance for every generator; no adaptivity to the realized truth is used, and the per-prefix forms with explicit constants appear in the proofs. The remaining sparse-core dodge (a singleton-core variant) is left open. Proof sketch. Run any generator against AK (Figure 5): a single transcript serves both the truth-K reading (full enumeration of K, capped at 1/2 by Lemma 3.5(R2)) and the truth-K ′ reading (core C = K of exact density α). For (a) at truth K ′ , split K ′ [1. . .N ] = K[1. . .mN ] ⊔ (D ∩ K ′ [1. . .N ]) with mN = ⌊αN ⌋ and cap the K-part by (R2). For (b), finite trivia at truth K forces |O ∩ D| < ∞, so a density-composition lemma carries the α/2 cap to truth K ′ . Full proof in Section D.4. The matching achievability is a single explicit generator, G∗ , that races on the conjunction of the consistent candidates and sweeps on their union. We define it together with the universal sweep generator Gsw , which gives the universal lower bound c ≥ 1 − d(C, H) for every countable collection. S For a countable collection H, write Ut = {H ′ ∈ H : St ⊆ H ′ } for the union of the consistent candidates and let I (t) be KW’s identified intersection (Fact 2.1); the universal sweep generator is at =

 ≺ -least of Ut \ (St ∪ Ot−1 ),

t ∈ R := {k 2 : k ≥ 1},

≺ -least of I (t) \ (S ∪ O

t∈ / R.

t

t−1 ),

(3.3)

(In spirit, Gsw is the gleaner of Millet’s painting: it walks the field in canonical order and gathers S whatever the reapers have left behind.) On the tight family, with Ht = {H ′ ∈ Hα : St ⊆ H ′ }, Ut = Ht ,

15

Flood and Harvest

fixed prefix K ′ [1. . .N ]; thick cells = K (raced), thin cells = D (swept); filled = claimed by O T = 2 · 104 : 0.304 T = 2 · 105 : 0.610 T = 106 : 0.830 the horizon T grows; the reading at the fixed prefix climbs to 1 − α/2 = 5/6 (sweep rounds have density 0: the trivia count is infinite, the rate is not)

Figure 6: Coverage is a property of the limit set. Snapshots of the same fixed prefix K ′ [1. . .N ] (α = 1/3) as the

horizon grows; the measured coverage (right, from Section F) climbs to 1 − α/2. Sweep rounds are sparse, so the trivia rate vanishes even though every D-cell is eventually claimed. The snapshots also illustrate why simulations must fix the prefix and grow the horizon.

and It =

T

Ht , the tight generator is at =

 ≺ -least of Ut \ (St ∪ Ot−1 ),

t ∈ R := {k 2 : k ≥ 1},

≺ -least of I \ (S ∪ O

t∈ / R.

t

t

t−1 ),

(3.4)

Theorem 3.7 (Achievability side: sweep and the tight generator). With the partial model and limit-set coverage: (i) (Universal sweep) The generator Gsw of (3.3) is sound (zero hallucination, unconditionally) and on every legal instance achieves O ⊇ H \ C, hence coverage c ≥ 1 − d(C, H) √ (≥ 1 − α when d(C, H) = α exists), with trivia rounds among [1 . . . N ] bounded by T0 + ⌊ N ⌋ (T0 finite, instance-dependent): the trivia rate tends to 0 while the count is infinite in general (necessarily, by Theorem 3.6(c)). (ii) (Tight generator on Hα ) On the tight family Hα the single deterministic generator G∗ of (3.4) achieves, with zero hallucination: √ (a) truth K (any C ⊆ K, any order): c ≥ max(1/2, 1 − d(C, K)), trivia rate ≤ ⌊ N ⌋/N ; (b) truth K ′ with C ⊆ K (covering all of Theorem 3.6(a)’s tight instances): c ≥ 1−α/2−o(1), with zero trivia; (c) truth K ′ with C ̸⊆ K: c ≥ max(1/2, 1 − d(C, K ′ )), zero trivia. (iii) (Finite-trivia side; restated) Fact 2.1 gives a generator with d(O, H) ≥ 12 d(C, H) for every countable collection and eventually zero trivia; on Hα it attains α/2 at truth K ′ and 1/2 at truth K, matching Theorem 3.6’s caps. Proof sketch. A pointer lemma drives (i): any x ∈ H \ C stays in Ut (as H is consistent) and is never enumerated, so if it were never output the sweep rounds (of which there are infinitely many) would always emit a new element strictly below x, which is impossible, as only finitely many positions lie below x. For (ii), G∗ races on the conjunction It (which equals K while the seen-set sits inside K) and sweeps on the union Ut = K ′ , so race covers half of K and the sweep claims all of D = K ′ \ K; at truth K ′ the two disjoint contributions sum to 1 − α/2. A key consistency point: at truth K the sweep eventually claims all of D, so O ∩ D = D is infinite, which is exactly why Theorem 3.6(b)’s finite-trivia cap does not apply to G∗ . For (iii) we need nothing about the internal mechanics of KW’s generator: since it achieves generation in the limit (∃t∗ ∀t ≥ t∗ : at ∈ H \ St ) and H ⊆ F , it is eventually sound 16

Flood and Harvest

Table 1: The trivia phase transition on Hα (revealed core C ⊆ K of exact density α, presented as the candidate

intersection). The optimum jumps by the unrecorded mass 1 − α as the trivia allowance crosses from finite to infinite count, even though the infinite-count optimum is attained at trivia rate → 0.

Trivia allowance

Optimal coverage c∗

Finite count Infinite count (rate → 0)

Attained by

Tight by

α/2

Fact 2.1 (KW)

1 − α/2 (G , core C ⊆ K)

G∗ , Equation (3.4)

Theorem 3.6(b) Theorem 3.6(a)

∗

Jump = 1 − α = unrecorded mass and eventually zero-trivia, which is exactly what our soundness and finite-trivia hypotheses require. Full proof in Section D.5. Remark 3.8 (Scope on part (ii)). The unqualified “1 − α/2 at truth K ′ ” is false for general C ⊆ K ′ : if C = K ′ is enumerated by the racing adversary, every generator is capped at 1/2. Case (b)’s restriction C ⊆ K is exactly what the dichotomy needs. Remark 3.9 (Consistency mechanism). At truth K, G∗ emits infinitely many elements of D = F \ K (the sweep covers the union K ′ ⊇ D), so its trivia count there is infinite. This is the mechanism that reconciles Theorem 3.6(b) with Theorem 3.7(ii): the finite-trivia cap of α/2 governs only generators whose trivia count is finite on every instance, and G∗ is not one of them. The infinitude of O ∩ D at truth K is precisely the resource that pays for coverage 1 − α/2 at truth K ′ . Combining the two sides gives the dichotomy in closed form. Corollary 3.10 (The trivia dichotomy). On the tight family Hα of (3.1) with revealed core of exact density α, the optimal guaranteed coverage of valuable mathematics is c∗ =

 α/2,

under any finite-trivia allowance, and

1 − α/2,

under any infinite-trivia allowance,

(3.5)

both bounds tight, the latter already attained at vanishing trivia rate. The transition is in trivia count, not rate. The jump 1 − α between the two regimes is exactly the unrecorded mass — the valuable statements never written into the core. Proof. The finite-trivia value α/2 is upper-bounded by Theorem 3.6(b) and attained by Theorem 3.7(iii). The infinite-trivia value 1 − α/2 is upper-bounded by Theorem 3.6(a) and attained by G∗ at vanishing rate via Theorem 3.7(ii)(b). The gap is (1 − α/2) − α/2 = 1 − α = 1 − d(C, H), the lower density of H \ C in H. Remark 3.11 (Interface of the impossibility proofs). The proofs of Lemma 3.5 and Theorem 3.6 use only the following properties of the triple (K, K ′ , F ): a countable ground set with a canonical order; nesting K ⊊ K ′ ⊆ F with all three infinite; F \K ′ infinite; and mN := |K ∩K ′ [1. . .N ]| = αN +O(1) with α > 0 exact. Any triple meeting this interface inherits Lemma 3.5 and Theorem 3.6 verbatim. We invoke this in Proposition 4.2 to transport the dichotomy into the compression model.

17

Flood and Harvest

4

Case Study: Instantiation in a Compression Model of Mathematics

The dichotomy was stated abstractly. We close more modestly: we exhibit, inside a concrete model of mathematics-as-compression, the macro framework of Aksenov et al. (2026) (hereafter ABFM), concrete compressible-language families that meet the lower-bound interface of Remark 3.11, together with a structured family where no trivia are needed. We claim no more than this, not a theorem about all compressible languages. In ABFM a “valuable” statement is a compressible string: one whose length under a macro dictionary is far below its raw length. We are explicit about the ledger: no ABFM theorem is an ingredient. ABFM supplies the definitional substrate (macros, wrapped length, geometric dictionaries) and the motivating asymmetry between the abelian monoid An and the free monoid Fn ; the proofs below are self-contained. We work in the abelian monoid An and the free monoid Fn , each with its canonical order isomorphic to N (as Lemma 3.5 and Theorem 3.6 demand), and write HD := { w : |w|G∪D ≤ θκ (|w|G ) } for the sublanguage compressible under a macro dictionary D, where |w|G∪D is the wrapped length and θκ (L) = κ log2 (1 + L) the compressibility cut (Section C collects the definitions and the macro framework). The abelian regime is benign: compressible languages there form an identifiable chain, so breadth needs no trivia at all. t

Theorem 4.1 (Abelian refinement chains are identifiable). Fix κ ≥ 1 and b ≥ 16κ2 , and set bt := b2 and Dt := {btj ai : i ≤ n, j ≥ 1} (geometric dictionaries, nested by refinement: Dt+1 ⊆ Dt ). Then Hab := {HDt }t is a strictly descending chain of infinite languages satisfying Angluin’s condition b +b3

with the singleton tell-tales Tt = {a1 t t }. Consequently, by Theorem 3.1(a) (single fiber F = An ), exact breadth in the limit is achievable on Hab : in the structured abelian regime, valuable generation needs no trivia. (The partial-enumeration behavior of this chain is open.) Proof sketch. A digit-sum formula computes the wrapped length, |w|G∪Dt = i sbt (Ni ) (replace bt copies of btj by one btj+1 , terminating at the base-bt representation). Same-count representations P

b +b3

transfer down the chain, giving nesting; the witness a1 t t has digit sum 2 in base bt but 2bt in base b2t , separating HDt from HDt+1 because 2bt > 5κ log2 bt for b ≥ 16κ2 . Full proof in Section D.6.1. In the free regime we exhibit families meeting the lower-bound interface (Remark 3.11). Name-cut pairs realize the tight family at every rational density, and an unbounded-cut variant realizes the extreme separation point: finite-trivia coverage 0 against sweep coverage 1. These are worked instances, not a statement about every compressible-language pair. Work in Fn (n ≥ 2) with letters {a, x} and a target density α = p/q. The construction uses the m macros µm,i := xi a xq+1−i a x2 (m ≥ 1, 1 ≤ i ≤ q) and, under the bounded cut θ ≡ 1 (HD,1 = G ∪ D, the nameable corpus), the name-cut pair K := {a, x} ∪ {µm,i : i ≤ p} ⊊ K ′ := {a, x} ∪ {all µm,i }.

(4.1)

Proposition 4.2 (Free-monoid pairs realize the dichotomy). In Fn (n ≥ 2), with letters {a, x}: (i) (Name-cut pairs at every rational α) The pair (4.1) satisfies |K ∩ K ′ [1. . .N ]| = αN + O(q), so d(K, K ′ ) = α exactly; it meets the interface of Remark 3.11, and the dichotomy (Corollary 3.10) holds verbatim inside the compression model.

18

Flood and Harvest

(ii) (Obstruction: the bounded cut is forced) For the unbounded cut θκ with dictionary-only m wrapped length and nested tag-dictionaries (µ̂m,i = aa xi a xq+1−i a x2 , tags ≤ p versus all), the analogous pair (K̂, K̂ ′ ) has d(K̂, K̂ ′ ) = 0 (unique parsing via aa-blocks; the total count of compressible strings is exponential in L, the k-block counting Nk (L) ≤ q k (log2 L + 1)k bounds the small-k mass, and the tag restriction truncates the rest; the good-word fraction vanishes at rate Θ(1/ log L) along prefix scales). Nested tag-pairs under unbounded cuts realize no α ∈ (0, 1). (iii) (Extreme separation point) For that pair (K̂, K̂ ′ ), finite-trivia sound generators have coverage 0 at truth K̂ ′ (same-transcript transfer and d(K̂, K̂ ′ ) = 0), while Gsw of Theorem 3.7(i) achieves coverage 1 with vanishing trivia rate. The free regime exhibits the maximal gap of the dichotomy: coverage 0 versus 1. Finally, the exhaustive generator is quantitatively imprecise: among formal statements within a ball, only a polynomially small fraction is valuable. Proposition 4.3 (Imprecision of exhaustive generation). In An with base c ≥ 4 and κ < n(1 − 1/ log2 c), the compressible sublanguage H = HDc satisfies c1 r 1/ log2 c−n ≤

|H ∩ BG (r)| ≤ c2 r−δ , |BG (r)|

δ = n − κ − n/ log2 c > 0,

(4.2)

where BG (r) is the wrapped-length ball of radius r. The fraction of compressible statements is polynomially small in the radius r, equivalently exponentially small in ABFM’s compressed scale s (since r = cΘ(s) ; interpretation only). The exhaustive generator’s precision thus tends to 0 polynomially in volume, while the sweep generator’s precision tends to 1. Proof sketch. Two-sided counting of compressible multisets: the upper bound counts representations with small digit sums against the volume of BG (r), the lower bound exhibits a positive density of compressible points. Full proof in Section D.6. Remark 4.4 (Numerical sanity checks). The density claims were sanity-checked numerically using the limit-set methodology: fix the prefix size N , grow the run length T , and compute coverages in exact rational arithmetic to avoid floating-point artifacts in the density limits. The race share converges to 1/2, and on Hα with α = 1/3 the truth-K ′ coverage of G∗ converges to 5/6 = 1 − α/2 while a pure-race generator stalls at α/2 ≈ 0.17. See Section F for the details.

5

Discussion

What the results say for practice. The picture for verifier-coupled mathematical generation is sharp and, we think, not the one a practitioner expects. A proof checker guarantees validity and makes every error benign (under sound coverage no output is ever false, Theorem 3.2), but it supplies no information about value (Theorem 3.1). Covering unrecorded valuable mathematics is therefore not free: by Corollary 3.10 any generator reaching beyond coverage α/2 must emit infinitely many certified trivia, and a generator that does so is the provably optimal shape of a broad generator, not a defect to be engineered away. What can be engineered away is its visible cost: those trivia are needed only at asymptotically negligible rate (Theorem 3.7). The corollary for system design is that selectivity—taste, 19

Flood and Harvest

the decision of which valid statements are worth recording—cannot come from the verifier and must come from examples; “filter the trivia” is a post-processing question about value, orthogonal to the validity the checker already certifies. The count budget collapses (a finding, not an open problem). One might hope for a finer hierarchy between the finite and the infinite trivia regimes, indexed by a count budget g(N ) on the trivia emitted in the first N rounds. There is none. Our achievability proof shows that the sweep claims every never-enumerated valuable string under any unbounded trivia allowance, so every g(N ) → ∞ already buys the full 1 − α/2 (Theorem 3.7); the finite-trivia cap α/2 is exactly the complementary case (Theorem 3.6). The dichotomy is genuinely count-finite versus count-infinite, full stop, and not the coarse shadow of a smoother trade-off. Open problems. 1. The singleton sparse-core race. On the tight family the recorded core is the conjunction of the candidates and is raceable at exactly 1/2. When the core is an unstructured sparse set (a singleton collection), a bottom-racing adversary outruns any core-blind generator, and the optimal share of the recorded mass is governed by combinatorics we have not resolved. We conjecture the optimum is 1 − α for α ≤ 1/2; settling it is a cat-and-mouse problem about which the present techniques are silent. 2. Partial enumeration of structured chains. Theorem 4.1 establishes breadth for abelian refinement chains in the breadth model; the behavior of their relative densities under partial enumeration, whether the structured regime that needs no trivia for breadth also escapes them for density, is open. 3. Statistical rates. We work distribution-free and in the limit. A relativization of the rate analysis of Kalavasis et al. (2025) to the nested pair, quantifying how fast coverage approaches its optimum, is left open. 4. Computational and efficient versions. Our generators are arbitrary functions of the prefix; whether the dichotomy survives a computability or efficiency constraint, in the spirit of the complexity barriers of Arenas et al. (2026), is open in the nested model. 5. Oracle-free sound coverage. Theorem 3.2(b) exhibits one pair model on which no oracle-free generator achieves sound coverage, but we do not characterize which pair models admit it. We ask for an Angluin-type condition on P (a combinatorial property of the candidate pairs) deciding whether oracle-free sound coverage (equivalently, the sandwich property of (2.6)) is achievable; our separation gives one failure, a full characterization is open. Limitation. The dichotomy is stated for the tight family Hα , where the recorded core is the conjunction of candidates; the universal sweep bound c ≥ 1 − d(C, H) holds for every countable collection, but the matching lower bound 1 − α/2 does not, and core structure, not merely density, decides the optimum, as the singleton race above shows. The compression instantiation is a worked realization, not a theorem about all compressible languages: Proposition 4.2 exhibits families meeting the lower-bound interface, not a generic-language statement. And throughout, value is modeled as an unknown language, not defined; the contribution is the price of covering it, not a theory of what makes mathematics worth doing.

20

Flood and Harvest

6

Outlook: We Must Generate. We Will Select.

A century ago, Poincaré (1914) located mathematical discovery not in the production of true statements, which “can be done by any one,” but in the discernment that selects among them. Our results give that observation a quantitative edge in the machine age. A perfect verifier secures the border of the formal world: within it nothing is false, and every unavoidable error has been demoted to mere triviality (Theorem 3.2). About which truths deserve to be kept, however, the verifier is silent (Theorem 3.1), and the dichotomy prices that silence. A generator that would harvest the unrecorded valuable mathematics must flood; the flood can be thinned to a vanishing fraction of the stream, but never dammed to a finite count (Theorem 3.7, Corollary 3.10). Flood and harvest are not a defect and its remedy. They are two faces of a single process, and the first cannot be dispensed with if the second is to be complete. What remains, for machines as it has always been for mathematicians, is taste: the selection that must follow correctness and that no checker can supply. If machines are to help expand mathematics, they must first be allowed to generate more truth than anyone cares to know, and we must learn to find, inside that flood, the part worth keeping. Hilbert’s confidence, broadcast to the world in 1930, has lost none of its force. Our theorems only add a quiet corollary: the knowing will not arrive alone. “Wir müssen wissen. Wir werden wissen.” “We must know. We will know.” — David Hilbert, Königsberg address (1930)

References Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. Large language models for mathematical reasoning: Progresses and challenges. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics: Student Research Workshop, pages 225–237, 2024. Vitaly Aksenov, Eve Bodnia, Michael H. Freedman, and Michael Mulligan. Compression is all you need: Modeling mathematics. arXiv preprint arXiv:2603.20396, 2026. Antonios Anastasopoulos, Giuseppe Ateniese, and Evgenios M. Kornaropoulos. Safe language generation in the limit. arXiv preprint arXiv:2601.08648, 2026. Dana Angluin. Finding patterns common to a set of strings. In Proceedings of the 11th Annual ACM Symposium on Theory of Computing (STOC), pages 130–141, 1979. doi: 10.1145/800135.804406. Dana Angluin. Inductive inference of formal languages from positive data. Information and Control, 45(2):117–135, 1980. Dana Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87–106, 1987. doi: 10.1016/0890-5401(87)90052-6. Dana Angluin. Queries and concept learning. Machine Learning, 2(4):319–342, 1988. doi: 10.1007/ BF00116828. Dana Angluin and Carl H. Smith. Inductive inference: Theory and methods. ACM Computing Surveys, 15(3):237–269, 1983. doi: 10.1145/356914.356918. 21

Flood and Harvest

Marcelo Arenas, Pablo Barceló, Luis Cofré, and Alexander Kozachinskiy. Language generation: Complexity barriers and implications for learning. In Proceedings of the 43rd International Conference on Machine Learning (ICML), 2026. Jeremy Avigad. Mathematics and the formal turn. arXiv preprint arXiv:2311.00007, 2023. Yannan Bai, Debmalya Panigrahi, and Ian Zhang. Language generation in the limit: Noise, loss, and feedback. In Proceedings of the ACM-SIAM Symposium on Discrete Algorithms (SODA), 2026. arXiv:2507.15319. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Proceedings of the 36th International Conference on Machine Learning (ICML 2019), volume 97 of Proceedings of Machine Learning Research, pages 454–463. PMLR, 2019. Maissam Barkeshli, Michael R. Douglas, and Michael H. Freedman. Artificial intelligence and the structure of mathematics. arXiv preprint arXiv:2604.06107, 2026. Edoardo Botta, Yuchen Li, Aashay Mehta, Jordan T. Ash, Cyril Zhang, and Andrej Risteski. On the query complexity of verifier-assisted language generation. In Proceedings of the 42nd International Conference on Machine Learning (ICML), 2025. arXiv:2502.12123. Moses Charikar and Chirag Pabbaraju. Exploring facets of language generation in the limit. In Proceedings of the 38th Conference on Learning Theory (COLT), pages 854–887, 2025. arXiv:2411.15364. Moses Charikar and Chirag Pabbaraju. Pareto-optimal non-uniform language generation. In 37th International Conference on Algorithmic Learning Theory (ALT), 2026. Moses Charikar, Chirag Pabbaraju, and Ambuj Tewari. A characterization of list language identification in the limit. In The 39th Annual Conference on Learning Theory (COLT), 2026. Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, and Thang Luong. Gold-medalist performance in solving olympiad geometry with AlphaGeometry2. Journal of Machine Learning Research (JMLR), 2025. Simon Colton. Automated Theory Formation in Pure Mathematics. Springer, London, 2002. Simon Colton, Alan Bundy, and Toby Walsh. Automatic concept formation in pure mathematics. In Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI), pages 786–791, 1999. Simon Colton, Alan Bundy, and Toby Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human-Computer Studies, 53(3):351–375, 2000. Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev, Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli. Advancing mathematics by guiding human intuition with AI. Nature, 600(7887):70–74, 2021. doi: 10.1038/s41586-021-04086-x.

22

Flood and Harvest

Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28. 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625–635. Springer, 2021. doi: 10.1007/978-3-030-79876-5_ 37. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction – CADE-25. 25th International Conference on Automated Deduction, Berlin, Germany, August 1–7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015. doi: 10.1007/978-3-319-21401-6_26. Henry Ernest Dudeney. Amusements in Mathematics. Thomas Nelson and Sons, London, 1917. Source of the “printer’s error” identity 2592 = 25 · 92 . Évariste Galois. Œuvres mathématiques d’évariste galois. Journal de Mathématiques Pures et Appliquées, 11:381–444, 1846. Published posthumously by Joseph Liouville. Atul Ganju, Travis McVoy, Shaddin Dughmi, and Shang-Hua Teng. A theory of time-sensitive language generation: Sparse hallucination beats mode collapse. arXiv preprint arXiv:2605.11302, 2026. William I. Gasarch and Mark G. Pleszkoch. Learning via queries to an oracle. In Proceedings of the 2nd Annual Workshop on Computational Learning Theory (COLT), pages 214–229, 1989. Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner. Mathematical exploration and discovery at scale. arXiv preprint arXiv:2511.02864, 2025. E. Mark Gold. Language identification in the limit. Information and Control, 10(5):447–474, 1967. Ben Green and Terence Tao. The primes contain arbitrarily long arithmetic progressions. Annals of Mathematics, 167(2):481–547, 2008. doi: 10.4007/annals.2008.167.481. arXiv:math/0404188. Jacques Hadamard. Sur la distribution des zéros de la fonction ζ(s) et ses conséquences arithmétiques. Bulletin de la Société Mathématique de France, 24:199–220, 1896. doi: 10.24033/bsmf.545. Steve Hanneke, Amin Karbasi, Anay Mehrotra, and Grigoris Velegkas. On union-closedness of language generation. In The Thirty-ninth Annual Conference on Neural Information Processing Systems (NeurIPS), 2025. Godfrey Harold Hardy. A Mathematician’s Apology. Cambridge University Press, Cambridge, 1940. Vincent Herrmann and Jürgen Schmidhuber. Interestingness as an inductive heuristic for future compression progress. arXiv preprint arXiv:2605.14831, 2026. David Hilbert. Naturerkennen und logik. Die Naturwissenschaften, 18(47):959–963, 1930. doi: 10.1007/BF01492194. Mikael Møller Høgsgaard and Chirag Pabbaraju. Agnostic language identification and generation. arXiv preprint arXiv:2601.23258, 2026. Thomas Hubert, Rishi Mehta, Laurent Sartran, et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651(8106):607–613, 2026. doi: 10.1038/s41586-025-09833-y. Published online 12 November 2025 (AlphaProof). 23

Flood and Harvest

Shima Imani, Liang Du, and Harsh Shrivastava. MathPrompter: Mathematical reasoning using large language models. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 5: Industry Track), pages 37–42, 2023. Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath – deep sequence models for premise selection. In Advances in Neural Information Processing Systems 29 (NIPS 2016), 2016. arXiv:1606.04442. Sanjay Jain, Daniel N. Osherson, James S. Royer, and Arun Sharma. Systems That Learn: An Introduction to Learning Theory. MIT Press, 2nd edition, 1999. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In Proceedings of the 11th International Conference on Learning Representations (ICLR), 2023. arXiv:2210.12283. Haocheng Ju and Bin Dong. Ai for mathematics: Progress, challenges, and prospects. arXiv preprint arXiv:2601.13209, 2026. Alkis Kalavasis, Anay Mehrotra, and Grigoris Velegkas. On the limits of language generation: Trade-offs between hallucination and mode collapse. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC), 2025. doi: 10.1145/3717823.3718108. arXiv:2411.09642. Alkis Kalavasis, Anay Mehrotra, and Grigoris Velegkas. On characterizations for language generation: Interplay of hallucinations, breadth, and stability. In 37th International Conference on Algorithmic Learning Theory (ALT), 2026. Amin Karbasi, Omar Montasser, John Sous, and Grigoris Velegkas. (Im)possibility of automated hallucination detection in large language models. In Proceedings of the 2nd Conference on Language Modeling (COLM), 2025. arXiv:2504.17004. Jon Kleinberg and Sendhil Mullainathan. Language generation in the limit. In Advances in Neural Information Processing Systems (NeurIPS), 2024. arXiv:2404.06757. Jon Kleinberg and Fan Wei. Density measures for language generation. In Proceedings of the 66th IEEE Symposium on Foundations of Computer Science (FOCS), 2025. arXiv:2504.14370. Jon Kleinberg and Fan Wei. Banach density of generated languages: Dichotomies in topology and dimension. arXiv preprint arXiv:2604.02385, 2026a. Jon Kleinberg and Fan Wei. Language generation and identification from partial enumeration: Tight density bounds and topological characterizations. In The 58th ACM Symposium on Theory of Computing (STOC), 2026b. Jon Kleinberg, Anay Mehrotra, Amin Saberi, and Grigoris Velegkas. On language generation in the limit with bounded memory. arXiv preprint arXiv:2605.30324, 2026a. Jon Kleinberg, Charlotte Peale, and Omer Reingold. Mistake-bounded language generation. arXiv preprint arXiv:2605.10809, 2026b.

24

Flood and Harvest

Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Advances in Neural Information Processing Systems 35 (NeurIPS), pages 34651–34664, 2022. arXiv:2205.11491. Steffen Lange, Thomas Zeugmann, and Sandra Zilles. Learning indexed families of recursive languages from positive data: A survey. Theoretical Computer Science, 397(1–3):194–232, 2008. doi: 10.1016/j. tcs.2008.02.030. Douglas B. Lenat. Automated theory formation in mathematics. In Proceedings of the 5th International Joint Conference on Artificial Intelligence (IJCAI), pages 833–842, 1977. Douglas B. Lenat. Eurisko: A program that learns new heuristics and domain concepts. Artificial Intelligence, 21(1–2):61–98, 1983. Aaron Li and Ian Zhang. Quantifying noise in language generation. In Proceedings of the 43rd International Conference on Machine Learning (ICML), 2026. Jiaxun Li, Vinod Raman, and Ambuj Tewari. On generation in metric spaces. arXiv preprint arXiv:2602.07710, 2026a. Xiaoyu Li, Andi Han, Jiaojiao Jiang, and Junbin Gao. Contrastive identification and generation in the limit. arXiv preprint arXiv:2605.06211, 2026b. Xiaoyu Li, Andi Han, Jiaojiao Jiang, and Junbin Gao. On the price of privacy for language identification and generation. arXiv preprint arXiv:2604.07238, 2026c. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. In Proceedings of the First Conference on Language Modeling (COLM), 2024. arXiv:2404.09939. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025. Anay Mehrotra, Grigoris Velegkas, Xifan Yu, and Felix Zhou. Language generation with infinite contamination. In The 39th Annual Conference on Learning Theory (COLT), 2026a. Anay Mehrotra, Grigoris Velegkas, Xifan Yu, and Felix Zhou. Differentially private language generation and identification in the limit. In The 39th Annual Conference on Learning Theory (COLT), 2026b. Hristo Papazov and Nicolas Flammarion. Learning algorithms in the limit. In The 38th Annual Conference on Learning Theory (COLT), pages 4486–4510. PMLR, 2025. Charlotte Peale, Vinod Raman, and Omer Reingold. Representative language generation. In Proceedings of the 42nd International Conference on Machine Learning (ICML), 2025. arXiv:2505.21819. Binghui Peng, Amin Saberi, and Grigoris Velegkas. Language identification in the limit with computational trace. In The Fourteenth International Conference on Learning Representations (ICLR), 2026. Plato. The Republic. Project Gutenberg edition, 375 BC. c. 375 BC. Stephanus pagination cited. 25

Flood and Harvest

Plato. Meno. Project Gutenberg edition, 380 BC. c. 385 BC. Stephanus pagination cited. Henri Poincaré. Science and Method. Thomas Nelson and Sons, London, Edinburgh, Dublin, and New York, 1914. English translation of Science et méthode. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. Giorgio Racca, Michal Valko, and Amartya Sanyal. Language generation with replay: A learningtheoretic view of model collapse. In Proceedings of the 43rd International Conference on Machine Learning (ICML), 2026. Ananth Raman and Vinod Raman. Generation from noisy examples. In Proceedings of the 42nd International Conference on Machine Learning (ICML), 2025. arXiv:2501.04179. Vinod Raman, Jiaxun Li, and Ambuj Tewari. Generation through the lens of learning theory. In Proceedings of the 38th Conference on Learning Theory (COLT), 2025. arXiv:2410.13714. Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models. Nature, 625(7995):468–475, 2024. doi: 10.1038/s41586-023-06924-6. Frank Stephan. Learning via queries and oracles. Annals of Pure and Applied Logic, 94(1–3):273–296, 1998. doi: 10.1016/S0168-0072(97)00077-8. Terence Tao. Machine-assisted proof. Notices of the American Mathematical Society, 72(1):6–13, 2025. doi: 10.1090/noti3041. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), January 20–21, 2020, New Orleans, LA, USA, pages 367–381. ACM, 2020. doi: 10.1145/3372885.3373824. arXiv:1910.09336. William P. Thurston. On proof and progress in mathematics. Bulletin of the American Mathematical Society, 30(2):161–177, 1994. doi: 10.1090/S0273-0979-1994-00502-6. arXiv:math/9404236. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024. doi: 10.1038/s41586-023-06747-5. George Tsoukalas, Rahul Saha, Amitayush Thakur, Sabrina Reguyal, and Swarat Chaudhuri. Learning interestingness in automated mathematical theory formation. In Advances in Neural Information Processing Systems (NeurIPS), 2025. Christoph Wernhard and Zsolt Zombori. Mathematical knowledge bases as grammar-compressed proof terms: Exploring metamath proof structures. arXiv preprint arXiv:2505.12305, 2025. Andrew Wiles. Modular elliptic curves and Fermat’s Last Theorem. Annals of Mathematics, 141(3): 443–551, 1995. doi: 10.2307/2118559. Ludwig Wittgenstein. Tractatus Logico-Philosophicus. Kegan Paul, Trench, Trubner & Co., London, 1922. Ludwig Wittgenstein. Remarks on the Foundations of Mathematics. Basil Blackwell, Oxford, 1956. 26

Flood and Harvest

Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Advances in Neural Information Processing Systems 35 (NeurIPS 2022), 2022. arXiv:2205.12615. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems 36 (NeurIPS), Datasets and Benchmarks Track, 2023. arXiv:2306.15626. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. MetaMath: Bootstrap your own mathematical questions for large language models. In Proceedings of the 12th International Conference on Learning Representations (ICLR), 2024. Jie M. Zhang, Cezara Petrui, Kristina Nikolić, and Florian Tramèr. RealMath: A continuous benchmark for evaluating language models on research-level mathematics. In Advances in Neural Information Processing Systems 38 (NeurIPS), Datasets and Benchmarks Track, 2025. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal olympiad-level mathematics. In Proceedings of the 10th International Conference on Learning Representations (ICLR), 2022. arXiv:2109.00110.

27

Flood and Harvest

Appendix A

Notation

We collect the symbols used throughout. The conventions are those of Section 2; this table is a reference, not a redefinition, and every entry points to the section where the object is introduced.

B

Symbol

Meaning

U F H P PF H Ht St at O C α d(·, ·), d(·, ·) c trichotomy trvN Hα K ⊊ K′ mN T It = Ht S Ut = Ht I (t) Gsw G∗ R = {k 2 } AK EM Trace , w(t) θκ (L) = κ log2 (1 + L) HD An , Fn

countable ground set of statements, fixed canonical order ≺; 1-based L[1. . .N ] ambient formal (verifiable) language; membership oracle is the proof checker valuable target language, H ⊆ F pair model {(Fi , Hi )} (Definition 2.3) fiber over F : candidates {Hi : Fi = F } sharing one ambient a countable collection of candidate targets candidates consistent with St : {H ′ : St ⊆ H ′ } seen-set: values enumerated by the adversary through round t generator’s output at round t (element-based, at ∈ / St ) limit set {at : t ≥ 1} of all outputs over the run revealed core: infinite C ⊆ H the adversary enumerates lower density d(C, H) of the core in the target lower / upper prefix density (liminf / limsup of |L′ ∩ L[1. . .N ]|/N ) coverage at truth H: c = d(O ∩ H, H) hallucination (a ∈ / F ) / triviality (a ∈ F \ H) / valuable (a ∈ H) triviality rate through round N (Definition 2.5) tight family {K, K ′ } of (3.1) sparse revealed target K inside coverable world K ′ ; D = K ′ \ K |K ∩ K ′ [1. . .N ]| = ⌊αN ⌋, the K-count in the K ′ -prefix conjunction of consistent candidates union of consistent candidates KW’s identified intersection (Fact 2.2) universal sweep generator (3.3) tight generator on Hα (3.4) sweep schedule (density-0, infinite) racing adversary (Definition 3.4) fresh-exhaustion round for K[1. . .M ] (Section D.3) race rounds (density 1) and the non-race deficit w(t) = o(t) compressibility cut (Section C) D-compressible sublanguage {w : |w|G∪D ≤ θκ (|w|G )} free abelian monoid on n generators; free monoid on n letters

Map of the Results

Figure 7 traces the dependency structure. The map has four layers. The restated facts supply the two external inputs: KMV’s breadth characterization (Fact 2.7) and KW’s partial-enumeration guarantees (Facts 2.1 and 2.2). The lemmas are the load-bearing mechanisms: sandwich-exclusion and fresh-index 28

Flood and Harvest

Fact 2.7

Theorem 3.1

Theorem 4.1

restated

Lemma D.2 Theorem 3.2 Remark 3.11

Lemma D.3 e fac

er int

Lemma D.4 Theorem 3.6

Corollary 3.10

Lemma 3.5

Facts 2.1 and 2.2

Theorem 3.7

Proposition 4.2

restated

Lemma D.5

Proposition 4.3

Figure 7: Dependency map. Dashed boxes are restated prior facts; solid boxes are results of this paper. The

impossibility theorem (Theorem 3.6) and the achievability theorem (Theorem 3.7) meet at the dichotomy (Corollary 3.10); the case study (Theorem 4.1, Proposition 4.2, Proposition 4.3) reads the dichotomy off the interface of Remark 3.11.

(Lemmas D.2 and D.3) for the separation, the race lemma and density-composition (Lemmas 3.5 and D.4) for the lower bound, and the pointer lemma (Lemma D.5) for the sweep. The theorems assemble these: taste (Theorem 3.1) from KMV, the separation (Theorem 3.2) from the two chain lemmas, the caps (Theorem 3.6) and the sweep theorem (Theorem 3.7) from the race, composition, and pointer lemmas. The caps and the sweep theorem meet at the dichotomy (Corollary 3.10). Finally the case study instantiates the abstract picture: Theorem 4.1 reads off taste, while Proposition 4.2 reads the dichotomy off the interface (Remark 3.11) and reuses the sweep pointer for its extreme separation point.

C

Mathematical Background

The case study of Section 4 works inside two monoids and the macro framework of Aksenov et al. (2026) (ABFM). We collect the definitions here so the body can name them in one line. We use this model as a substrate only: no theorem of ABFM is an ingredient in any proof below.

C.1

Monoids and canonical orders

A monoid is a set with an associative binary operation and an identity element. Two monoids carry the case study. Q i The free abelian monoid An on generators a1 , . . . , an is the set of formal products ni=1 aN i with Ni ∈ N, multiplied coordinate-wise; it is isomorphic to (Nn , +), with each element identified with its P exponent vector (N1 , . . . , Nn ). The raw length (the generator count) is |w|G = ni=1 Ni . We order An by degree-then-lex: first by |w|G , then lexicographically on the exponent vector. The free monoid Fn on n letters is the set of finite words over the alphabet, with concatenation as the operation and the empty word as identity; |w|G is the word length. We order Fn by length-then-lex.

29

Flood and Harvest

N2

ε

6

3

a

b

1

2

7

aa

ab

ba

bb

4

8

3 . . .

4 . . .

5 . . .

6 . . .

2

5

1

9

N1

1 N2 A2 : elements aN are lattice points; 1 a2

F2 : words are tree nodes; length-then-lex reads the tree level by level

degree-then-lex snakes through the diagonals

Figure 8: The two monoids and their canonical orders (Section C.1). Left: A2 ∼ = (N2 , +); degree-then-lex enumerates

the lattice diagonal by diagonal, so the order is isomorphic to N. Right: F2 ; length-then-lex reads the word tree level by level. In both cases L[1. . .N ] is a well-defined initial segment, which is all the density machinery of Section 2 needs.

Both orders are order-isomorphic to N (Figure 8; each has finitely many elements below any given one, and the order is total), which is exactly the structure the density machinery of Section 2.1 requires: a countable ground set with a canonical order in which L[1. . .N ] is a well-defined initial segment.

C.2

The macro framework

Following ABFM, a dictionary D is a finite or infinite set of designated monoid elements, called macros. Generation is allowed to use the augmented generating set G ∪ D: a factorization of w is an expression of w as a product of elements of G ∪ D. The wrapped length |w|G∪D := min{ k : w = g1 · · · gk , gj ∈ G ∪ D }

(C.1)

is the minimum number of symbols from G ∪ D in any factorization of w, and the raw (unwrapped) length |w|G uses G alone. A macro that abbreviates a long element shortens its wrapped length below its raw length: this is the precise sense in which “compressible” means “short under the dictionary.” For An the relevant dictionaries are geometric: Dc = { c j ai : i ≤ n, j ≥ 1 } provides single-letter powers at every scale cj . For this dictionary the wrapped length has a closed form, |w|G∪Dc =

n X

sc (Ni ),

(C.2)

i=1

where sc (N ) is the sum of the base-c digits of N (Figure 9) (the digit-sum lemma, Lemma D.7; the minimizing factorization is the base-c representation of each coordinate). The compressibility cut is the threshold θκ (L) := κ log2 (1 + L),

(C.3)

HD := { w : |w|G∪D ≤ θκ (|w|G ) },

(C.4)

and the compressible sublanguage is

the elements whose wrapped length is logarithmic in their raw length. A bounded cut θ ≡ 1 (used in Proposition 4.2(i)) collapses HD,1 to the nameable corpus G ∪ D itself. 30

Flood and Harvest

one macro: a27 ∈ D3 |a27 |G∪D3 = s3 (27) = 1 ≤ log2 28: compressible (∈ HD3 )

|a25 |G∪D3 = s3 (25) = 5 > log2 26: not compressible (just misses the cut) a9

a9

a3

a3

a

Figure 9: Wrapped length and the compressibility cut, by example (Section C.2; A1 , geometric dictionary

D3 = {a3 , a9 , a27 , . . . }, κ = 1). The wrapped length is the base-3 digit sum (C.2): a27 compresses to a single macro and passes the cut, while a25 = a9 a9 a3 a3 a needs five symbols and just misses it. Compressibility is thin, which is the precision phenomenon Proposition 4.3 quantifies.

We are explicit about the ledger: the framework supplies definitions (macros, wrapped length, geometric dictionaries) and the motivating asymmetry between An and Fn , and nothing more. The proofs in Section D.6 are self-contained; no ABFM theorem is invoked.

C.3

The usage of ABFM models in the case study

Section 4 uses these objects in two shapes. In An it builds refinement chains: nesting the geometric dictionaries by Dt+1 ⊆ Dt gives a descending chain of compressible languages HDt separated by m digit-sum witnesses (Theorem 4.1). In Fn it builds name-cut pairs: words xi a xq+1−i a x2 whose unique parsing lets an a-position cut the corpus into a sparse target K and a full world K ′ at any rational density (Proposition 4.2).

D

Deferred Proofs

This appendix restates each result with its original number and gives the full proof.

D.1

Verification is not taste (Theorem 3.1)

Theorem 3.1 (Verification is not taste). Let P = {(Fi , Hi )} be a countable pair model (Definition 2.3), with a relativized generator (Definition 2.4) that queries the perfect verifier 1F . (a) Exact breadth in the limit on P is achievable if and only if every fiber PF satisfies Angluin’s condition. (b) Approximate breadth in the limit on P is achievable if and only if every fiber satisfies the weak Angluin condition. (c) In the single-ambient case Fi ≡ F , the relativized characterization coincides with the oraclefree characterization of Fact 2.7. In the multi-ambient case the verifier’s entire information content, for the in-the-limit breadth goal, is exactly ambient identification: locating which F is realized, after which it adds nothing. (d) (Zero-discrimination.) For Hi , Hj in the same fiber the oracle is the identical function 1F ; the realized query path and output at any prefix Sn are identical across the two instances. Every behavioral distinction within a fiber is driven by the enumeration alone.

31

Flood and Harvest

Proof. We prove (a) and (b) together (necessity, then sufficiency), then (c) and (d) and the edge cases. Necessity. Suppose some fiber PF ∗ violates the relevant condition. Write H := PF ∗ ; it is countable, nonempty, and all its members are infinite. Restrict the adversary to instances (F ∗ , H) with H ∈ H. On every such instance the verifier handed to a relativized generator G is always the single fixed function 1F ∗ . Define the oracle-stripped ordinary generator G′n (Sn ) := Gn1F ∗ (Sn ).

(D.1)

This is well defined: in round n the generator’s adaptive query tree has finite depth, and the fixed function 1F ∗ resolves every query, selecting one leaf and one output. Thus G′n is an arbitrary set-valued function of the prefix, exactly the object KMV quantify over (Fact 2.7; their Remark 2.3 imposes no computability). Extensional agreement holds across all of H: for every fiber instance and every enumeration, 1 Gn Fz (Sn ) = G′n (Sn ) for all n (∗) because Fz = F ∗ for every z indexing a member of the fiber, so the oracle is the identical function. Now if G achieved exact (resp. approximate) breadth in the limit on all of P, then by (∗) the ordinary generator G′ would achieve it on every target in H, contradicting Fact 2.7, since H violates Angluin’s (resp. the weak Angluin) condition. Hence the condition is necessary in each part. Sufficiency. Assume every fiber satisfies the relevant condition. Stage 1 (ambient identification; sample-independent). In round n the generator queries the canonical point xn to the verifier. Call index i ambient-consistent at n if Fi ∩ {x1 , . . . , xn } = F ∩ {x1 , . . . , xn }, and let ẑn be the least ambient-consistent index (the set is nonempty since the true index z qualifies). Lemma D.1 (Stage-1 stabilization). ẑn stabilizes in finite time to z0 := min{i : Fi = F }. Proof. z0 is ambient-consistent at every n, so ẑn ≤ z0 always. Each i < z0 has Fi ̸= F (by minimality of z0 ), hence there is a least canonical point xm(i) ∈ Fi △ F , and i is permanently inconsistent from round m(i) on. Taking N1 := maxi<z0 m(i) < ∞, every i < z0 is eliminated by round N1 , so ẑn = z0 for all n ≥ N1 . (No distinctness of the Fi is needed; duplicates share the fiber.) Stage 2 (fiber generation). For each ambient set F that occurs, fix, by the achievability half of Fact 2.7 applied to the fiber PF , an ordinary generator Γ(F ) achieving exact (resp. approximate) breadth in the limit on PF . (The choice ranges over the countably many occurring ambient sets; we use the axiom of choice over this countable index, removable by taking the ≺-lexicographically least generator in a fixed enumeration; see the closing remark.) The constructions’ internal mechanics are absorbed into the fixed function level; no computability is claimed. Define the composite relativized generator (F

)

Gn1F (Sn ) := Γn ẑn (Sn ).

(D.2)

For n ≥ N1 , Lemma D.1 gives Fẑn = F , so ) Gn1F (Sn ) = Γ(F n (Sn )

for n ≥ N1 .

(†)

The true target H = Hz lies in the true fiber PF (witnessed by z), and Sn is the genuine prefix of a genuine KM enumeration of H: the generator never restarts the enumeration at N1 . By the guarantee of Γ(F ) there is a finite round n∗Γ from which the breadth property holds; for n ≥ max(N1 , n∗Γ ), (†) 32

Flood and Harvest

transfers it to G. The pre-stabilization rounds form a finite prefix, absorbed by “in the limit”. This proves (a) and (b). (c). In the single-ambient case the verifier is the fixed function 1F from round 1, so (∗) gives relativized ⇐⇒ oracle-free, and both ⇐⇒ (weak) Angluin by Fact 2.7. Thus, for the breadth goal, the verifier’s only information content in the pair model is the identification of F performed in Stage 1; within a fiber it changes nothing. (The scope is essential: Theorem 3.2 shows that for the sound-coverage goal the verifier does strictly more.) (d). For Hi , Hj in the same fiber, 1Fi = 1Fj = 1F literally. The adaptive query tree, resolved by 1F on a fixed prefix Sn , yields the identical path and identical output regardless of which of Hi , Hj is the true target. Hence any behavioral distinction within a fiber is driven by the enumeration alone. Edge cases. (E1) Duplicates. Angluin’s conditions are properties of the underlying set system and are invariant under repetition of languages in the collection. (E2) Finite fibers. A finite fiber satisfies Angluin’s condition: for each ordered pair i = ̸ j with Hi \ Hj = ̸ ∅, place a witness tij ∈ Hi \ Hj into the tell-tale Ti (at most m − 1 elements for a fiber of size m); then any Hj ⊇ Ti forces Hi ⊆ Hj , so Hj is not a proper subset of Hi . (E3) Only occurring ambients are ever guessed, and occurring fibers are nonempty (they contain the realized target). (E4) The same valuable language appearing under two different ambients constitutes two different instances in two different fibers; Stage 1 separates them by the ambient query. Choice avoidance. The use of the axiom of choice in Stage 2 is cosmetic. Fix once and for all a canonical enumeration of all ordinary generators (e.g. a ≺-lexicographic order on finite descriptions); for each occurring ambient F , let Γ(F ) be the lexicographically least generator achieving the required breadth on PF . This is a definable choice, so no appeal to the axiom of choice is needed.

D.2

The exhaustive generator and the separation (Theorem 3.2)

We first record the two structural lemmas underlying the separation, then give the phase construction. Lemma D.2 (Sandwich-exclusion). Work over U = N × {0, 1}. Let L∗ = U0 (column 0), let the spine be the even column-0 indices R = {(2m, 0) : m ≥ 0}, and set Hj = L∗ \ R≥j with R≥j = {(2m, 0) : m ≥ j}. Let Fj = Hj ∪ Aj and F∞ = L∗ ∪ A∞ with Aj , A∞ ⊆ U1 (column 1) infinite. Then for every j, every finite S ⊆ U , and every G ⊆ U , G cannot satisfy both (i) L∗ \ S ⊆ G ⊆ F∞ , (ii) Hj \ S ⊆ G ⊆ Fj . Proof. Suppose both hold. From the lower side of (i) and the upper side of (ii), L∗ \S ⊆ G ⊆ Fj = Hj ∪Aj . Intersect with U0 (column 0): since L∗ ⊆ U0 and Aj ⊆ U1 are disjoint columns, L∗ \ S = (L∗ \ S) ∩ U0 ⊆ (Hj ∪ Aj ) ∩ U0 = Hj . Hence L∗ \ Hj ⊆ S, i.e. R≥j ⊆ S. But R≥j is infinite and S is finite, a contradiction. (The set A∞ is never used; the contradiction lives entirely in column 0.) Lemma D.3 (Fresh-index availability). With the parameters of Lemma D.2: for every finite T ⊆ L∗ and every N ∈ N there is j ≥ N with T ⊆ Hj ⊊ L∗ and L∗ \ Hj = R≥j infinite. Consequently

33

Flood and Harvest

{Hj }j ∪ {L∗ } is a Gold-style ascending chain with union L∗ , non-identifiable from positive data, and L∗ violates Angluin’s condition in this collection. Proof. Since T is finite, T ∩ R is finite, so for all sufficiently large j we have T ∩ R≥j = ∅, i.e. T ⊆ L∗ \ R≥j = Hj ; any such j ≥ N works. For every j, R≥j is infinite, so Hj ⊊ L∗ with infinite difference; and Hj contains all the odd column-0 indices, so it is infinite. The chain is ascending, S T H1 ⊆ H2 ⊆ · · · , with j Hj = L∗ \ j R≥j = L∗ . This is the textbook non-identifiable family: every finite T ⊆ L∗ lies in a proper sub-language Hj of L∗ in the collection, which is exactly the Angluin violation at L∗ . Theorem 3.2 (The exhaustive generator and the separation). In the pair model with the protocol of Definition 2.3: (a) (Exhaustive generator) With the verifier 1F , the generator Gn = F \ Sn achieves sound coverage in the limit on every countable pair model: at every round, it has zero hallucination, and (when F \ H is infinite) infinitely many trivia. (b) (Separation) There is a countable pair model P † (all languages infinite, every Fi \ Hi infinite) on which no oracle-free set-valued generator (an arbitrary function of the prefix) achieves sound coverage in the limit. (c) The verifier strictly enlarges the class of pair models admitting sound coverage, from a proper subclass to all of them; this is in contrast to breadth, where within a fiber it adds nothing (Theorem 3.1(c)). Proof. (a). Since H ⊆ F we have H \ Sn ⊆ F \ Sn ⊆ F , so Gn = F \ Sn satisfies (2.6) at every round (with n∗ = 0), on every countable pair model, with zero hallucination. When F \ H is infinite, the trivia count |(F \ H) \ Sn | is infinite at every n. (b). Take P † = {(Fj , Hj )}j ∪ {(F∞ , L∗ )} with the parameters of Lemmas D.2 and D.3, choosing the Aj , A∞ pairwise almost disjoint (this is a modeling convenience and is not load-bearing: Lemma D.2 is purely column-0). All languages are infinite, Hi ⊊ Fi , and Fi \ Hi = Ai is infinite. Fix any oracle-free set-valued generator G. We construct an adversary that defeats it. Fix the canonical repetition-free enumeration E ∗ of L∗ , and maintain the invariant that after phase ℓ the shown set is an initial segment {e1 , . . . , etℓ } of E ∗ . In phase ℓ, choose (by Lemma D.3) an index jℓ > max(jℓ−1 , tℓ−1 ) with the current shown set contained in Hjℓ ⊊ L∗ . Subphase A. Continue the enumeration in E ∗ -order, but restricted to Hjℓ (append not-yet-shown elements of Hjℓ in E ∗ -order). Two cases. • (A-fail) If G never sound-covers (Fjℓ , Hjℓ ) at any finite round of this continuation, declare (Fjℓ , Hjℓ ) the true pair. The produced sequence is a legal KM enumeration of Hjℓ : its initial segment lies in Hjℓ by choice of jℓ , and the tail exhausts Hjℓ . Since sound coverage in the limit would in particular hold at some finite round, its negation means G fails sound coverage at infinitely many rounds, so G fails in the limit. Done. • (A-succeed) Let t′ℓ be the first round at which Gt′ℓ sound-covers (Fjℓ , Hjℓ ). By Lemma D.2, at this round G does not sound-cover (F∞ , L∗ ). (‡) ∗ Subphase B (only in the (A-succeed) case). Let PA be the maximum E -position among all elements shown through round t′ℓ (a finite number). Append, in E ∗ -order, the not-yet-shown elements ek up to

34

Flood and Harvest

some tℓ ≥ max PA , tℓ−1 + 1, ℓ ,

(D.3)

restoring the initial-segment invariant: all shown elements lie in {e1 , . . . , etℓ }, repetition-free. The bound (D.3) clears PA because subphase A’s filtered enumeration may race ahead in E ∗ -position. Conclusion. If some phase ends in (A-fail), G fails as shown. Otherwise every phase completes via (A-succeed), so tℓ → ∞ by (D.3), and the limit sequence E † shows every element of L∗ exactly once, a legal KM enumeration of L∗ . At each of the infinitely many rounds t′ℓ , (‡) holds, so G fails sound coverage for (F∞ , L∗ ) at infinitely many rounds, hence fails in the limit. Declare (F∞ , L∗ ) the true pair. Either way, G fails on P † . (c). Part (a) shows the with-verifier class is all countable pair models; part (b) exhibits a model outside the without-verifier class. Strictness follows. The breadth contrast is Theorem 3.1(c). For the error-relocation reading: under sound coverage all outputs lie in F (no hallucination), and when F \ H is infinite the trivia count |(F \ H) \ Sn | is infinite (the exhaustive generator); by Theorem 3.1(d) the verifier supplies zero bits about H within a fiber, so it cannot reduce errors or locate value. What it buys is exactly keeping the unavoidable overshoot inside F . The two regimes of part (c) are genuinely distinct: P † has singleton fibers, so there the verifier identifies the target and eliminates errors; the relocation reading is the within-fiber regime.

D.3

The race lemma (Lemma 3.5)

Lemma 3.5 (Race lemma). Let K ⊆ U be infinite and let Trace ⊆ N have density 1, with w(t) := t − |Trace ∩ [1 . . . t]| = o(t). (R1) (Greedy cover) If at every t ∈ Trace the generator outputs the ≺-least element of K \(St ∪Ot−1 ), then against every adversary enumeration, |O ∩ K[1. . .M ]| ≥ 12 (M − w(τM ) − 1) for all M , where τM is the index of the M -th race round; hence d(O ∩ K, K) ≥ 1/2. (R2) (Racing cap) The racing adversary AK of Definition 3.4 is a legal repetition-free enumeration of K. Against it, every generator satisfies |O ∩ K[1. . .M ]| ≤ M/2 + log2 M + 3 for M ≥ 2; hence d(O ∩ K, K) ≤ 1/2. Proof. Call x resolved at t if x ∈ St ∪ Ot . (R1). Let tM be the first round at which all of K[1. . .M ] is resolved. Step 1. At any race round t ∈ Trace with K[1. . .M ] not yet resolved before the output, the output is a new element of O ∩ K[1. . .M ]. Indeed the rule outputs the ≺-least element of K \ (St ∪ Ot−1 ), and the ≺-least unresolved element of K lies in the downward-closed set K[1. . .M ] (some element of K[1. . .M ] is unresolved, and the global minimum over K of unresolved elements is ⪯ it, hence in K[1. . .M ]). Step 2. Consequently tM ≤ τM : each of the (at most) M race rounds up to tM that finds K[1. . .M ] unresolved contributes a distinct element of K[1. . .M ], and M such contributions exhaust K[1. . .M ]. Step 3. At most one race round ≤ tM is non-contributing: by minimality of tM , K[1. . .M ] is unresolved at every race round strictly before tM , so each such round contributes; only the round tM itself may be non-contributing (it may resolve the last element via the seen-set). Hence |O ∩ K[1. . .M ]| ≥ tM − w(tM ) − 1, where w(tM ) counts the non-race rounds up to tM . 35

Flood and Harvest

Step 4. Steal bound. Each x ∈ K[1. . .M ] \ O is resolved only by entering StM ; distinct elements have distinct first-enumeration rounds ≤ tM , so |K[1. . .M ] \ O| ≤ tM . Adding Step 3 and Step 4, 2|O ∩ K[1. . .M ]| ≥ M − w(tM ) − 1 ≥ M − w(τM ) − 1 (using tM ≤ τM and monotonicity of w). Since τM = M + w(τM ) ∼ M and w = o(t), dividing by M and taking the liminf gives d(O ∩ K, K) ≥ 1/2. (R2). Legality of AK . At t = ̸ 2n the adversary enumerates the ≺-least element of K \ (St−1 ∪ Ot−1 ) (a fresh round); at t = 2n it enumerates the ≺-least element of (Ot−1 ∩ K) \ St−1 (a recycle round, draining the generator’s hoarded backlog from the bottom; if empty, it uses the fresh rule as a fallback). We claim every x ∈ K is enumerated at some finite round, so AK is a legal repetition-free enumeration of K. The ≺-least un-enumerated element of K advances monotonically: fresh rounds push it forward, and recycle rounds drain the O-backlog from the bottom, so no element below the current pointer can be hoarded forever. Hence every fixed x ∈ K is enumerated at a finite round. No rate is claimed or needed: legality is eventual only. The cap. Fix M ≥ 2. Let FM be the set of fresh-enumerated elements in K[1. . .M ] and GM = O ∩ K[1. . .M ]. (C1) FM ∩GM = ∅ (an element is either enumerated by the adversary or output by the generator first, in the sense that an output element at ∈ / St is not among the fresh-enumerated by definition of the rule), so |FM | + |GM | ≤ M . (C2) Injection GM → FM up to exceptions. Map the entry round t of an O-element to round t + 1. If t + 1 is a fresh round and K[1. . .M ] is not yet fresh-exhausted, the fresh rule at t + 1 enumerates an element of FM . There are exactly two kinds of exception, which we count separately: (i) power-of-two recycle rounds: rounds t with t + 1 = 2n . Up to the fresh-exhaustion round EM (defined next) there are at most ⌊log2 EM ⌋ + 1 of these; (ii) the single post-exhaustion threshold: after EM the fresh rule no longer enumerates a new element of K[1. . .M ], costing O(1) further exceptions. Hence the total number of exceptions is at most ⌊log2 EM ⌋ + 1 + O(1) ≤ log2 EM + 2. (C3) The fresh-exhaustion round EM . Define EM as the round by which every element of K[1. . .M ] is used (lies in S ∪ O), equivalently the round by which the fresh pointer has passed K[M ], skipping any O-hoarded elements. We bound EM non-circularly. Each fresh round outputs the ≺-least un-enumerated element of K, so fresh claims strictly ≺-increase the fresh pointer; within M fresh rounds the pointer therefore passes K[M ]. Writing T := EM , the number of non-fresh (recycle) rounds up to T is at most ⌊log2 T ⌋ + 1 (one per power of two ≤ T ), so the number of fresh rounds up to T is at least T − log2 T − 1. Requiring this to reach M gives the implicit bound T ≤ M + log2 T + 1; solving it yields EM ≤ M + log2 (M + 1) + 2. Combining (C1)–(C3): |O ∩ K[1. . .M ]| = |GM | ≤ |FM | + (log2 EM + 2) ≤ M/2 + log2 M + 3, using EM ≤ M + log2 (M + 1) + 2 so that log2 EM ≤ log2 M + O(1). Dividing by M and taking the limsup gives d(O ∩ K, K) ≤ 1/2. Caution on EM . The round EM must not be read as the round of full enumeration of K[1. . .M ]: against a hoarding generator, full enumeration of K[1. . .M ] can take exponentially many rounds (the recycle trickle drains the backlog one element per power-of-two round). The cap argument needs only fresh-exhaustion, which advances at rate 1 per fresh round.

36

Flood and Harvest

D.4

Impossibility side of the dichotomy (Theorem 3.6)

Theorem 3.6 (Impossibility side of the dichotomy). On the tight family Hα of (3.1), with deterministic element-based generators and limit-set coverage: (a) (Race cap) For every deterministic generator there are two legal instances of Hα sharing one transcript (the adversary is AK inside K), with coverage at most 1/2 at truth K and at most 1 − α/2 at truth K ′ (revealed core C = K, density α). Hence no generator guarantees coverage exceeding 1 − α/2 on Hα , nor exceeding 1/2 at truth K. (b) (Finite-trivia cap) Every deterministic generator that emits finitely many trivia on every legal instance has coverage at most α/2 on the truth-K ′ racing instance. (c) (Necessity of trivia) Any generator guaranteeing coverage exceeding α/2 on all of Hα emits infinitely many trivia on some instance; with Theorem 3.7(iii), α/2 is exactly the finite-trivia frontier. We first record the composition lemma that carries densities between K and K ′ . Lemma D.4 (Density composition). Let K ⊆ K ′ be infinite with d(K, K ′ ) = α > 0 exact. For any A ⊆ K, d(A, K ′ ) = α · d(A, K), d(A, K ′ ) = α · d(A, K). Proof. Listings restrict to the canonical order, so A ∩ K ′ [1. . .N ] = A ∩ K[1. . .mN ] with mN := |K ∩ K ′ [1. . .N ]|. Write Xm := |A ∩ K[1. . .m]|/m. Then |A ∩ K ′ [1. . .N ]| |A ∩ K[1. . .mN ]| mN mN = · = XmN · . N mN N N The sequence (mN ) is nondecreasing with increments in {0, 1} and mN → ∞, so it hits every large integer; hence lim supN XmN = lim supm Xm and likewise for lim inf. Since mN /N → α > 0, the limits factor as claimed. Proof of Theorem 3.6. (a). Run any deterministic generator G against the racing adversary AK of Lemma 3.5(R2). The transcript is a single object O, and any verifier is fixed advice (F = N under both readings), so the two readings K and K ′ share it. Legality of both readings. As truth K, AK is a full repetition-free enumeration of K (Lemma 3.5(R2)). As truth K ′ , the same stream is a legal partial enumeration of K ′ with revealed core C = K of exact density d(K, K ′ ) = α ((3.2)). Truth K. By Lemma 3.5(R2), c ≤ d(O ∩ K, K) ≤ 1/2, i.e. coverage ≤ 1/2 + O(log M )/M . Truth K ′ . Split K ′ [1. . .N ] = K[1. . .mN ] ⊔ (D ∩ K ′ [1. . .N ]) with mN = ⌊αN ⌋ (by (3.2)). Then |O ∩ K ′ [1. . .N ]| ≤ |O ∩ K[1. . .mN ]| + |D ∩ K ′ [1. . .N ]| ≤

mN mN 2 + log2 mN + 3 + (N − mN ) = N − 2 + O(log N ),

using Lemma 3.5(R2) on the K-part. Dividing by N and taking the liminf gives c ≤ 1 − α/2, i.e. coverage ≤ 1 − α/2 + O(log N )/N . Per-instance. The caps bind for every generator on the single instance AK ; no adaptivity to the realized truth is used. Hence no generator guarantees coverage exceeding 1 − α/2 on Hα , nor exceeding 1/2 at truth K. 37

Flood and Harvest

(b). Run G against the same AK , so the transcript is shared. Suppose G emits finitely many trivia on every legal instance; in particular at the legal truth-K instance, |O∩(F \K)| < ∞, so C0 := |O∩D| < ∞. At truth K ′ , |O ∩ K ′ [1. . .N ]| ≤ |O ∩ K ∩ K ′ [1. . .N ]| + C0 . Applying Lemma D.4 with A = O ∩ K and then Lemma 3.5(R2), c = d(O ∩ K ′ , K ′ ) ≤ d(O ∩ K, K ′ ) = α · d(O ∩ K, K) ≤ α · 12 = α2 . (c). The contrapositive of (b): any generator guaranteeing coverage exceeding α/2 on all of Hα must emit infinitely many trivia on some instance. Exactness of the finite-trivia frontier at α/2 follows from Theorem 3.7(iii), which attains α/2 at truth K ′ with eventually zero trivia.

D.5

Achievability: sweep and the tight generator (Theorem 3.7)

Theorem 3.7 (Achievability side: sweep and the tight generator). With the partial model and limit-set coverage: (i) (Universal sweep) The generator Gsw of (3.3) is sound (zero hallucination, unconditionally) and on every legal instance achieves O ⊇ H \ C, hence coverage c ≥ 1 − d(C, H) √ (≥ 1 − α when d(C, H) = α exists), with trivia rounds among [1 . . . N ] bounded by T0 + ⌊ N ⌋ (T0 finite, instance-dependent): the trivia rate tends to 0 while the count is infinite in general (necessarily, by Theorem 3.6(c)). (ii) (Tight generator on Hα ) On the tight family Hα the single deterministic generator G∗ of (3.4) achieves, with zero hallucination: √ (a) truth K (any C ⊆ K, any order): c ≥ max(1/2, 1 − d(C, K)), trivia rate ≤ ⌊ N ⌋/N ; (b) truth K ′ with C ⊆ K (covering all of Theorem 3.6(a)’s tight instances): c ≥ 1−α/2−o(1), with zero trivia; (c) truth K ′ with C ̸⊆ K: c ≥ max(1/2, 1 − d(C, K ′ )), zero trivia. (iii) (Finite-trivia side; restated) Fact 2.1 gives a generator with d(O, H) ≥ 12 d(C, H) for every countable collection and eventually zero trivia; on Hα it attains α/2 at truth K ′ and 1/2 at truth K, matching Theorem 3.6’s caps. Proof. Pointer lemma.

We first prove the fact that drives both generators.

Lemma D.5 (Pointer lemma). Suppose at each sweep round t ∈ R the generator outputs the ≺-least element of Vt \ (St ∪ Ot−1 ) for a family Vt with H ⊆ Vt for all t, and R is infinite. Then for every x ∈ H never enumerated by the adversary, x ∈ O. Proof. Fix such an x at H-position p. Since H ⊆ Vt always, x ∈ Vt ; since x is never enumerated, x∈ / St for all t. Suppose x ∈ / O. At every sweep round t ∈ R, the output is the ≺-least element of Vt \ (St ∪ Ot−1 ), which is ⪯ x (as x itself is available) and ̸= x (as x ∈ / O), hence strictly ≺ x — a new element of H strictly below position p. But only p − 1 positions lie below x, and R is infinite, a contradiction. Hence x ∈ O.

38

Flood and Harvest

(i) Universal sweep Gsw . Recall Ut = {H ′ ∈ H : St ⊆ H ′ } and the sweep schedule R = {k 2 }. Apply Lemma D.5 with Vt = Ut : for any x ∈ H \ C, H is consistent (St ⊆ C ⊆ H) so H ∈ Ht and x ∈ Ut , while x ∈ / C is never enumerated. Hence O ⊇ H \ C. Therefore S

|O ∩ H[1. . .N ]| ≥ N − |C ∩ H[1. . .N ]|,

so

c ≥ 1 − d(C, H),

which is ≥ 1 − α when d(C, H) = α exists. Trivia rate. By Fact 2.2 there is a finite T0 with I (t) ⊆ H for all t ≥ T0 , so every non-sweep output from T0 on lies in√H; the only possible trivia rounds among [1 . . . N ] are √ the ≤ T0 early non-sweep rounds and the ⌊ N ⌋ sweep rounds, giving a trivia count ≤ T0 + ⌊ N ⌋ and rate → 0. The count is infinite in general, necessarily so, by Theorem 3.6(c). S Soundness. Ut ⊆ H ⊆ F ; I (t) is contained in some candidate ⊆ F ; the fallback lies in F . Hence O ⊆ F : zero hallucination. (The restated KW lemma is used only for the non-sweep half of the trivia bound. A bare conjunction default would fail on a general H: for H = {N \ {n}} the conjunction of consistent candidates is just St . On Hα , G∗ below avoids this restated lemma entirely.) (ii) Tight generator G∗ on Hα . Recall Ht = {H ′ ∈ Hα : St ⊆ H ′ }, It = structure is: St ⊆ K =⇒ Ht = {K, K ′ }, It = K, Ut = K ′ ;

T

Ht , Ut =

S

Ht . The

St ̸⊆ K =⇒ Ht = {K ′ }, It = Ut = K ′ .

(a) Truth K. Here every enumerated element is in C ⊆ K, so St√⊆ K always and It = K. The non-sweep rounds form the set N \ R, of density 1 with w(t) = ⌊ t⌋ = o(t); on them G∗ runs Lemma 3.5(R1)’s greedy race on K (the ≺-least element of It \ (St ∪ Ot−1 ) = K \ (St ∪ Ot−1 )). Thus d(O ∩ K, K) ≥ 1/2, i.e. c ≥ 1/2. Applying Lemma D.5 with Vt = Ut = K ′ ⊇ K gives O ⊇ K \ C, so c ≥ 1 − d(C, K); together c ≥ max(1/2, 1 − d(C, K)). Trivia.√Race outputs lie in K; the sweep covers Ut = K ′ ⊇ D, so trivia rounds among [1 . . . N ] number ≤ ⌊ N ⌋, rate → 0. Note O ∩ D = D is infinite: the sweep eventually claims all of D via Lemma D.5 (each d ∈ D lies in Ut = K ′ and is never enumerated at truth K). This infinitude is exactly why Theorem 3.6(b)’s finite-trivia cap does not apply to G∗ . (b) Truth K ′ with C ⊆ K. The transcript is identical to case (a): C ⊆ K means St ⊆ K throughout, so G∗ cannot and need not distinguish the two truths, and runs (R1)’s race on K exactly as before. By Lemma D.5 with H = K ′ (every x ∈ K ′ \ C is never enumerated and lies in Ut = K ′ ), O ⊇ K ′ \ C ⊇ D. For coverage, split K ′ [1. . .N ] = K[1. . .mN ] ⊔ (D ∩ K ′ [1. . .N ]) (mN = ⌊αN√ ⌋); the sweep claims all ′ N − mN elements of D ∩ K [1. . .N ] and the race claims at least mN /2 − O( N ) of K[1. . .mN ], and the two parts are disjoint, so √ √
|O ∩ K ′ [1. . .N ]| ≥ (N − mN ) + m2N − O( N ) = N 1 − α2 − O( N ), giving c ≥ 1 − α/2 − o(1). Trivia. Race outputs ⊆ K ⊆ K ′ and sweep outputs ⊆ K ′ , so zero trivia at truth K ′ . (c) Truth K ′ with C ̸⊆ K. Let t0 be the first (finite) round with wt0 ∈ / K. From t0 on, St ̸⊆ K, ′ ′ so It = Ut = K . Apply Lemma 3.5(R1) with K ← K and Trace = (N \ R) \ [1 . . . t0 ] (still density 1): c ≥ 1/2. Lemma D.5 with Vt = Ut = K ′ gives c ≥ 1 − d(C, K ′ ); together c ≥ max(1/2, 1 − d(C, K ′ )). All outputs lie in K ′ , so zero trivia. Scope. The unqualified “1 − α/2 at truth K ′ ” is false for general C ⊆ K ′ : if C = K ′ enumerated by the racing adversary, the cap of Lemma 3.5(R2) holds with K ← K ′ and pins every generator at 1/2. Case (b)’s restriction C ⊆ K is exactly the regime the dichotomy needs.

39

Flood and Harvest

(iii) Finite-trivia side (restated). By Fact 2.1, KW’s generator achieves d(O, H) ≥ 12 d(C, H) for every countable collection, never consulting F ; generation in the limit gives ∃t∗ ∀t ≥ t∗ : at ∈ H \ St , so the trivia rounds are confined to t < t∗ : eventually zero. Because H ⊆ F , the same statement at ∈ H for t ≥ t∗ makes the generator eventually sound (at ∈ F ) as well; this is exactly what our model’s soundness (eventually at ∈ F ) and finite-trivia (eventually at ∈ / F \ H) hypotheses require, and it follows from the generation guarantee alone. No claim about the pre-t∗ outputs (and in particular no inference from the internal pod construction of KW’s generator) is needed for the load-bearing path. On Hα this yields α/2 at truth K ′ and 1/2 at truth K, matching the caps of Theorem 3.6. Remark D.6 (Non-load-bearing aside). KW’s pods are in fact candidate-contained at all times, so one expects the pre-t∗ outputs also to lie in F here; we record this only as an aside, as the eventual-soundness argument above already supplies everything the dichotomy uses.

D.6

The instantiation (Theorem 4.1 and Propositions 4.2 and 4.3)

D.6.1

Abelian refinement chains (Theorem 4.1) t

Theorem 4.1 (Abelian refinement chains are identifiable). Fix κ ≥ 1 and b ≥ 16κ2 , and set bt := b2 and Dt := {btj ai : i ≤ n, j ≥ 1} (geometric dictionaries, nested by refinement: Dt+1 ⊆ Dt ). Then Hab := {HDt }t is a strictly descending chain of infinite languages satisfying Angluin’s condition b +b3

with the singleton tell-tales Tt = {a1 t t }. Consequently, by Theorem 3.1(a) (single fiber F = An ), exact breadth in the limit is achievable on Hab : in the structured abelian regime, valuable generation needs no trivia. (The partial-enumeration behavior of this chain is open.) Proof. Write w = three lemmas.

Ni ∼ n i ai ∈ An = (N , +), identified with its exponent vector (N1 , . . . , Nn ). We use

Q

Lemma D.7 (Digit-sum formula). For the geometric dictionary Dc = {c j ai : i ≤ n, j ≥ 1} (with P c = bt ), the wrapped length is |w|G∪Dc = ni=1 sc (Ni ), where sc (N ) is the sum of the base-c digits of N . i Proof. Each coordinate aN i is factored independently (the dictionary words are single-letter powers). For one coordinate: a factoring corresponds to a representation of Ni as a sum of powers of c with nonnegative integer coefficients (multiplicities), and its symbol count is the sum of those multiplicities. Replacing c copies of the macro c j ai by one copy of c j+1 ai preserves the represented power and strictly decreases the symbol count, so every minimizing representation has all multiplicities < c; the unique representation with all multiplicities < c is the base-c representation of Ni . Hence the minimum symbol count is its digit sum sc (Ni ). Summing over coordinates gives the formula.

Lemma D.8 (Nesting). HDt+1 ⊆ HDt , so {HDt }t is a descending chain. Proof. Since bt+1 = b2t , we have Dt+1 ⊆ Dt . A richer dictionary cannot increase the minimal factoring length, so |w|G∪Dt ≤ |w|G∪Dt+1 for every w. Therefore every w with |w|G∪Dt+1 ≤ θκ (|w|G ) also satisfies |w|G∪Dt ≤ θκ (|w|G ): membership transfers downward and the chain is descending. 40

Flood and Harvest

b +b3t

Lemma D.9 (Witness / singleton tell-tale). wt := a1 t tell-tale for HDt in the chain.

∈ HDt \ HDt+1 , and Tt = {wt } is a

Proof. By Lemma D.7, |wt |G∪Dt = sbt (bt + b3t ) = 2 (the number bt + b3t has base-bt digits 1 at positions 1 and 3). In base bt+1 = b2t , the same number is bt +bt ·b2t = bt (1+b2t ), whose base-b2t digit sum is 2bt (a digit bt at positions 0 and 1). The raw length is |wt |G = bt + b3t , so θκ (|wt |G ) = κ log2 (1 + bt + b3t ) ≤ 5κ log2 bt for large bt . Then |wt |G∪Dt = 2 ≤ θκ , so wt ∈ HDt ; while |wt |G∪Dt+1 = 2bt > 5κ log2 bt ≥ θκ since b ≥ 16κ2 forces 2bt > 5κ log2 bt , so wt ∈ / HDt+1 . As the chain is descending, {wt } separates HDt from every proper sub-language HDt′ , t′ > t: any HDt′ ∋ wt would need t′ ≤ t, so no proper sub-language j contains the tell-tale. The languages are infinite (e.g. all ac1 have wrapped length 1). The three lemmas give a strictly descending chain of infinite languages with singleton tell-tales, so Hab satisfies Angluin’s condition. By Theorem 3.1(a), applied in the single fiber F = An , exact breadth in the limit is achievable: in the abelian regime valuable generation needs no trivia. (The partial-enumeration behavior of the chain, its relative densities, is open.) D.6.2

Free-monoid pairs (Proposition 4.2)

Proposition 4.2 (Free-monoid pairs realize the dichotomy). In Fn (n ≥ 2), with letters {a, x}: (i) (Name-cut pairs at every rational α) The pair (4.1) satisfies |K ∩ K ′ [1. . .N ]| = αN + O(q), so d(K, K ′ ) = α exactly; it meets the interface of Remark 3.11, and the dichotomy (Corollary 3.10) holds verbatim inside the compression model. (ii) (Obstruction: the bounded cut is forced) For the unbounded cut θκ with dictionary-only m wrapped length and nested tag-dictionaries (µ̂m,i = aa xi a xq+1−i a x2 , tags ≤ p versus all), the analogous pair (K̂, K̂ ′ ) has d(K̂, K̂ ′ ) = 0 (unique parsing via aa-blocks; the total count of compressible strings is exponential in L, the k-block counting Nk (L) ≤ q k (log2 L + 1)k bounds the small-k mass, and the tag restriction truncates the rest; the good-word fraction vanishes at rate Θ(1/ log L) along prefix scales). Nested tag-pairs under unbounded cuts realize no α ∈ (0, 1). (iii) (Extreme separation point) For that pair (K̂, K̂ ′ ), finite-trivia sound generators have coverage 0 at truth K̂ ′ (same-transcript transfer and d(K̂, K̂ ′ ) = 0), while Gsw of Theorem 3.7(i) achieves coverage 1 with vanishing trivia rate. The free regime exhibits the maximal gap of the dichotomy: coverage 0 versus 1. Proof. (i) Name-cut pairs. With the bounded cut θ ≡ 1, the compressible language is exactly the nameable corpus HD,1 = G ∪ D: the letters {a, x} together with the macro words. Each µm,i = m xi a xq+1−i a x2 has a unique parsing (the two a’s mark the boundaries, and the three x-blocks have lengths i, q + 1 − i, 2m recovering m, i unambiguously), so the words are distinct and the a-position encodes i. Order Fn by length-then-lex. For each m, the q words {µm,i }qi=1 form an equal-length stratum (all have length q + 3 + 2m ), lex-ordered by i via the position of the first a. Of these q words, the p with i ≤ p lie in K; so within each stratum the count of K-elements is p out of q. Summing over strata up to position N , |K ∩ K ′ [1. . .N ]| = αN + O(q), α = p/q,

41

Flood and Harvest

the O(q) accounting for the partial last stratum and the two letters. Hence d(K, K ′ ) = α exactly. The pair (K, K ′ , Fn ) meets the interface of Remark 3.11: Fn is countable with the length-then-lex canonical order; K ⊊ K ′ ⊆ Fn are infinite; Fn \ K ′ is infinite (it contains all non-macro words); and mN = αN + O(q) = αN + O(1). By Remark 3.11, Lemma 3.5 and Theorem 3.6 hold verbatim for this pair, so the dichotomy (Corollary 3.10) holds inside the compression model. (ii) Obstruction. Now use the unbounded cut θκ with dictionary-only wrapped length and the m nested tag-dictionaries built from µ̂m,i = aa xi a xq+1−i a x2 (the leading aa-block is a unique delimiter). Parsing is unique via the aa-blocks. Write N (L) for the number of compressible strings of length ≤ L, and Nk (L) for those parsing into exactly k tag-blocks (k ≥ 0). We bound the upper density d(K̂, K̂ ′ ) in five displayed steps. (1) Deletion injection. Map a k-block word (k ≥ 1) to the (k − 1)-block word obtained by deleting its first aa-block (and the empty word for k = 1). A preimage of a given image is recovered by choosing the deleted block: a tag i ∈ [q] and a scale m ≤ log2 L, so each image has at most 1 + q(log2 L + 1) preimages. Hence
N (L) ≤ 1 + q + q log2 L N (L − 1). (D.4) (2) Small-k mass. A length-≤ L word with k blocks chooses, per block, a tag i ≤ q and a scale 2m ≤ L (i.e. m ≤ log2 L), so Nk (L) ≤ q k (log2 L + 1)k . For B := ⌈2 log log L/ log(q/p)⌉, X

Nk (L) ≤ B q B (log2 L + 1)B = exp O((log log L)2 ) .

(D.5)

k≤B

(3) Tag truncation. A k-block word lies in K̂ only if all k tags satisfy i ≤ p (versus all i ≤ q for K̂ ′ ). For k > B this costs a factor at most (p/q)k ≤ (p/q)B = (log L)−2

(D.6)

on the corresponding mass, by the choice of B. (4) Lower bound on N . The true count is exponential in L; we need only the weaker N (L) ≥ exp c log L · log log L , (D.7) √ √ witnessed at the block count k ∗ = ⌊κ log2 (1 + L)⌋: force one scale near L so every word passes the √ ∗ ∗ cut θκ , and choose the remaining k − 1 scales freely below L/k . This weaker bound suffices. (5) Conclusion. Split the K̂-mass at B blocks. By (D.5) the k ≤ B part is exp(O((log log L)2 )); by (D.6) the k > B part is at most (log L)−2 N (L). With (D.4) and N ≥ N (L − 1),

|K̂ ∩ K̂ ′ [1. . .N ]| exp(O((log log L)2 )) + (log L)−2 N (L) ≤ N N (L − 1) ≤ o(1) + (log L)−2 1 + q + q log2 L

= Θ(1/ log L),

(D.8)

using (D.7) to absorb the exp(O((log log L)2 )) term into o(1). The bound (D.8) holds along the prefix scales N = N (L − 1); interpolating between consecutive scales (the count grows by the factor (D.4) between L − 1 and L) gives the same o(1) rate for general N . Hence d(K̂, K̂ ′ ) = 0 : nested tag-pairs under the unbounded cut realize no α ∈ (0, 1). This is why the bounded cut θ ≡ 1 is forced for the name-cut construction shape; we present (i) as a worked example and (ii) as its obstruction, not as a generic compressible-language theorem. 42

Flood and Harvest

(iii) Extreme separation point. For the pair (K̂, K̂ ′ ) of (ii): run any finite-trivia sound generator against the racing enumeration of K̂ as the revealed core. As in Theorem 3.6(b), the same transcript serves both truths, and d(K̂, K̂ ′ ) = 0 forces the coverage at truth K̂ ′ to satisfy c ≤ d(K̂, K̂ ′ ) = 0 plus the finite-trivia correction C0 /N → 0; hence coverage 0 at truth K̂ ′ . On the other hand, Gsw of Theorem 3.7(i) achieves c ≥ 1 − d(C, K̂ ′ ) = 1 (since d(C, K̂ ′ ) = d(K̂, K̂ ′ ) = 0) with vanishing trivia rate. The free regime thus exhibits the maximal gap of the dichotomy: coverage 0 versus 1. D.6.3

Imprecision of exhaustive generation (Proposition 4.3)

Proposition 4.3 (Imprecision of exhaustive generation). In An with base c ≥ 4 and κ < n(1 − 1/ log2 c), the compressible sublanguage H = HDc satisfies c1 r 1/ log2 c−n ≤

|H ∩ BG (r)| ≤ c2 r−δ , |BG (r)|

δ = n − κ − n/ log2 c > 0,

(4.2)

where BG (r) is the wrapped-length ball of radius r. The fraction of compressible statements is polynomially small in the radius r, equivalently exponentially small in ABFM’s compressed scale s (since r = cΘ(s) ; interpretation only). The exhaustive generator’s precision thus tends to 0 polynomially in volume, while the sweep generator’s precision tends to 1. Proof. Work in An with base c ≥ 4 and κ < n(1 − 1/ log2 c). The wrapped-length ball BG (r) = {w : P |w|G ≤ r} has volume |BG (r)| = Θ(rn ) (the number of exponent vectors (N1 , . . . , Nn ) with i Ni ≤ r). P By Lemma D.7, w ∈ H = HDc iff i sc (Ni ) ≤ θκ (|w|G ) = κ log2 (1 + |w|G ) ≤ κ log2 (1 + r). P P Upper bound. The number of vectors with i sc (Ni ) ≤ κ log2 r and i Ni ≤ r is at most the number of vectors whose total base-c digit sum is at most D := κ log2 r, each coordinate < c L with L = logc r. A standard count of nonnegative integer vectors with bounded digit sum gives |H ∩ BG (r)| ≤ c′2 r n/ log2 c+κ up to logarithmic factors; dividing by |BG (r)| = Θ(rn ) gives |H ∩ BG (r)| ≤ c2 r−δ , |BG (r)|

δ = n − κ − n/ log2 c > 0,

where δ > 0 by the hypothesis κ < n(1 − 1/ log2 c). Lower bound. Restrict to vectors all of whose coordinates are powers of c (digit sum 1 each, total ≤ n ≤ κ log2 r for large r): there are Θ((logc r)n ) = Θ((log r)n ) of these within BG (r), but a stronger family gives the stated rate. Take a single coordinate to range over base-c blocks of magnitude up to r1/ log2 c (digit sum 1, the rest fixed); these lie in H ∩ BG (r) and number Θ(r1/ log2 c ). Dividing by Θ(rn ) gives |H ∩ BG (r)|/|BG (r)| ≥ c1 r 1/ log2 c−n . The two sides of (4.2) do not have matching exponents: the upper bound decays as r−δ with δ = n − κ − n/ log2 c, while the lower bound decays as r1/ log2 c−n , and δ = ̸ n − 1/ log2 c in general (they differ by κ + (n − 1)/ log2 c). The bound therefore brackets the precision between two polynomial rates without pinning it; closing the gap, determining the exact polynomial exponent, is open. Combining the two sides gives (4.2). The fraction is polynomially small in the radius r. Interpreting r as ABFM’s compressed scale via r = cΘ(s) turns the polynomial-in-r decay into an exponential-in-s decay (interpretation only, not used in the bound). The exhaustive generator thus has precision tending to 0 polynomially in volume, while the sweep generator of Theorem 3.7(i) has precision tending to 1.

43

Flood and Harvest

E

Summary of Oracle and Feedback Models

The verifier of Definition 2.4 is one of several side-information channels studied in this line, and the channels are not interchangeable: what a generator can learn depends sharply on what the oracle answers about. We tabulate the channels in Table 2 along the axis that organizes our results, namely whether the oracle speaks about the unknown target or about a fixed superset. Table 2: Side-information channels in the generation-in-the-limit line. The ambient oracle of this paper is the only

one that answers about a fixed superset of the target rather than about the target or the collection.

Model

Oracle answers

What it buys

KM membership queries to is x in a named member of the collection members (Klein- collection berg and Mullainathan, 2024)

internal to their algorithm; not a separate resource

MOP: decidability of the generator’s own support (Kalavasis et al., 2025)

defines the restriction class for the breadth impossibility

is x in the generator’s current guess

feedback queries to the is x in H (same-level member- finitely many add nothing; intarget (Bai et al., 2026; ship) finitely many are strictly more Charikar and Pabbaraju, powerful 2025) negative examples of the tar- a stream of points outside H get (Kalavasis et al., 2025)

restores breadth for every countable collection

prefix-completability pro- can this prefix extend to an ac- query complexity of constrained cess verifier (Botta et al., cepted string decoding; no unknown target 2025) computational traces / execution traces of the accept- restores identification beyond richer observations (Papa- ing machine; time-bounded ob- input–output data (Chomsky zov and Flammarion, 2025; servations of the algorithm hierarchy; learning algorithms) Peng et al., 2026) classical MQ + EQ / oracle- membership / equivalence to identification of the target from aided inference (Angluin, the target; Turing-degree ora- queries 1987, 1988; Gasarch and cles Pleszkoch, 1989; Stephan, 1998) this paper: ambient mem- is x formally valid (in F ) bership 1F

validity for free, breadth unchanged (Theorem 3.1); sound coverage enabled (Theorem 3.2); dichotomy unaffected (Corollary 3.10 is verifier-free)

The placement of our oracle is the source of every result. Because 1F returns “valid” on all of F and never supplies a negative inside the grey zone F \ H, it is informationless within a fiber: two candidates sharing one ambient receive identical answers, which is exactly why it cannot move the 44

Flood and Harvest

Angluin boundary (Theorem 3.1). Yet across ambients the same oracle is decisive: it identifies the formal world, which is all the verifier contributes to breadth and all that sound coverage needs (Theorem 3.2).

F

Numerical Validation

The main results of the paper are purely theoretical. This appendix records the simulations that sanity-checked the density claims and the two arithmetic traps a naive implementation falls into. Methodology. Coverage is a property of the limit set (Fact 2.1, following KW’s Definition 1.1), not of any finite stage, so a simulation must fix the prefix size N and grow the run length T until the measured coverage stabilizes. Reading coverage at the run frontier (where the prefix and the horizon advance together) systematically under-reads, because the sweep has not yet claimed the never-enumerated valuable elements within H[1. . .N ]: a fixed-N series at α = 1/3, N = 999 read 0.263 → 0.480 → 0.830 as T grew to 5 · 105 , converging only once T ≫ N . Second, membership in K must be computed in exact rational arithmetic. With floating point, ⌈42/0.7⌉ evaluates from 60.00000000000001 and misclassifies the boundary element; at α = 0.7 this manufactured spurious counterexamples to the density identity (3.2) that exact arithmetic dissolves. The tight family at α = 1/3. Table 3 reports coverage of G∗ and of two control generators against the racing adversary AK on Hα . The race share converges to 1/2, the truth-K ′ coverage of G∗ to 1 − α/2 = 5/6, and a pure conjunction race (the finite-trivia representative) stalls at α/2. The naive K ′ -sweeper that omits the race covers exactly 1−α, confirming that the race/sweep split is load-bearing: dropping the race loses exactly the half-of-K contribution. Table 3: Tight family Hα , α = 1/3, racing √ adversary AK . Measured coverage (fixed N , grown T ) against the

proven limit. The trivia counts confirm ⌊ T ⌋ trivia at truth K (rate → 0) and zero at truth K ′ .

Generator

Truth

N (or M )

Measured

Predicted limit

pure conj. race naive K ′ -sweep (no race)

K K′ K′ K′

M = 103

0.4930 0.8317 0.1702 0.6667

1/2 1 − α/2 = 5/6 ≈ 0.8333 α/2 ≈ 0.1667 1 − α = 0.6667

G∗ trivia G∗ trivia

K K′

T = 106 —

G∗ G∗

N = 104 , T = 4.5 · 107 — —

√ 1000 = ⌊ T ⌋ 0 (exactly)

rate → 0 0

Other densities. Table 4 reports the truth-K ′ coverage of G∗ across α, measured at N = 103 . Convergence is to 1 − α/2 from below, and slows as α → 0 (the small-α deficit is dominated by the √ O( N )/N race correction, which is largest relative to the tiny α/2 race contribution). Table 4: G∗ truth-K ′ coverage at N = 103 across densities. The α = 0.01 row needed T ≈ 3 · 106 to stabilize; the

others converge faster.

α

Measured

Predicted 1 − α/2

0.7 0.99 0.01

0.644 0.503 0.994

0.65 0.505 0.995

In every run convergence approaches the proven limit from below, with a deficit consistent with √ the O( N )/N + O(log N )/N corrections of Theorems 3.6 and 3.7; and hostile enumeration orders 45

Flood and Harvest

breached no bound (a deliberately delaying order read 0.5260 ≥ 1/2 at truth K, on the correct side of the cap).

G

The Dichotomy by Hand: A Worked Miniature

The race lemma and the two ends of the dichotomy can be watched in twenty rounds. Take the tight family (3.1) at α = 1/2: the coverable world is the evens K ′ = {0, 2, 4, . . . }, the revealed target is every second even, K = {2, 6, 10, . . . } (the residue 2 mod 4), the difference is D = {0, 4, 8, . . . } (the residue 0 mod 4), and the ambient is F = N, so the odds sit idle throughout: neither player ever touches them. The adversary is the racing adversary AK of Definition 3.4, which enumerates fresh ≺-least elements of K except at rounds t = 2n , where it re-enumerates an element the generator has already claimed. The generator is the tight generator G∗ of (3.4), which sweeps the union Ut = K ′ at square rounds t ∈ R = {1, 4, 9, 16, . . . } and races the intersection It = K otherwise. Within a round the adversary moves first; the generator sees St and Ot−1 . Table 5 replays the first twenty rounds; the trace, the prefix counts, and the coverage figures below are machine-generated and machine-checked. t

AK move

G∗ move

st

at

t

AK move

G∗ move

st

at

1 2 3 4 5 6 7 8 9 10

∗

sweep race race sweep race race race race sweep race

2 6 14 10 22 30 38 18 50 54

0 10 18 4 26 34 42 46 8 58

11 12 13 14 15 16 17 18 19 20

fresh fresh fresh fresh fresh recycle (= a5 ) fresh fresh fresh fresh

race race race race race sweep race race race race

62 70 78 86 94 26 102 110 118 126

66 74 82 90 98 12 106 114 122 130

fresh fresh∗ fresh recycle (= a2 ) fresh fresh fresh recycle (= a3 ) fresh fresh

Table 5: Twenty rounds of G∗ against AK at α = 1/2. Sweep outputs (bold) land in D: trivia at truth K, harvest

at truth K ′ . At the recycling rounds t = 4, 8, 16 the adversary re-enumerates an element the generator had claimed at an earlier round (a2 , a3 , a5 ), keeping its stream a legal full enumeration of K while cancelling generator work. ∗ At t = 1, 2 the recycle set is empty and AK falls back to the fresh rule.

Reading the race. Off the special rounds the two players simply alternate down the canonical order of K: the adversary enumerates the least unused element, the generator claims the next one. This alternation is what splits every prefix in half. The recycling rounds are the adversary’s whole trick: at t = 4 it re-enumerates 10, which the generator had output at t = 2. The move costs the adversary nothing it needed (its stream must eventually list all of K anyway, and 10 has to appear sometime), but it converts a generator success into a seen element, and since there are only log2 M powers of two below M , the cost of staying legal is the O(log M ) term in Lemma 3.5(R2). After twenty rounds the prefix K[1. . .M ] splits as |O ∩ K[1. . .4]| = 1,

|O ∩ K[1. . .8]| = 3,

|O ∩ K[1. . .16]| = 7,

each safely under the cap M/2 + log2 M + 3 of Lemma 3.5(R2) (7, 10, and 15 respectively), and each within reach of the greedy guarantee of (R1); the recycled elements 10, 18, 26 are exactly the ones counted on both sides of the ledger.

46

Flood and Harvest

Reading the dichotomy. The twenty outputs are one transcript serving two truths (Theorem 3.6). At truth K the race outputs are valuable and the four sweep outputs 0, 4, 8,√12 ∈ D are trivia: this is the flood, infinite in count (one per square round) but of vanishing rate ⌊ N ⌋/N . At truth K ′ the same sweep outputs are valuable, and the transcript contains no trivia at all, since every output is even. Quantitatively, coverage must be read in the limit-set sense (Section F): fixing the prefix K ′ [1. . .12] and growing the horizon T = 12, 50, 200, 1000 gives covered counts 5, 8, 8, 8, i.e. the prefix stabilizes at 2/3, short of the limit, because a fixed prefix retains the race’s early, pre-asymptotic rounds. Growing the prefix recovers the theorem: the stabilized coverage of K ′ [1. . .N ] at N = 12, 40, 120, 400, 1200 is 2 3,

29 40 ,

89 120 ,

297 400 ,

179 240 ,

climbing to 1 − α/2 = 3/4 from below, exactly the −o(1) of Theorem 3.7(ii)(b). The miniature also shows why the finite-trivia cap binds: forbid the sweep rounds and the generator is confined to the race, whose share of K ′ is the K-half of a half, α/2 = 1/4.

H

Additional Related Work

The body situates our model against its nearest neighbors in Section 1.4; here we walk the rest of the generation-in-the-limit line thematically, with one clause per paper recording its relation to the nested pair model. None of these works carries a verifiable ambient or distinguishes valid-but-worthless output from false output, so each meets our model along a single axis.

H.1

AI for mathematics and automated discovery

Machine-generated mathematics in practice. The empirical line our model abstracts begins with neural premise selection (Irving et al., 2016) and reinforcement-learning proof environments (Bansal et al., 2019), and runs through the neural theorem provers: GPT-f (Polu and Sutskever, 2020), HyperTree proof search (Lample et al., 2022), and the recent open frontier of DeepSeek-Prover (Xin et al., 2024) and Goedel-Prover (Lin et al., 2025), each a generator coupled to a proof assistant whose accept/reject verdict is exactly our membership oracle for F , in practice the Lean prover and its community library Mathlib (de Moura and Ullrich, 2021; de Moura et al., 2015; The mathlib Community, 2020). Olympiad-level systems push the same loop to competition difficulty: AlphaGeometry and its successor (Chervonyi et al., 2025; Trinh et al., 2024) and the formal reinforcement-learning prover AlphaProof (Hubert et al., 2026), whose proofs are valid by construction but whose value their pipelines must decide separately. AI-assisted discovery (Davies et al., 2021), program search (Romera-Paredes et al., 2024), and exploration at the scale of dozens of open problems (Georgiev et al., 2025) produce genuinely new mathematics, the regime our coverage measure quantifies: how much unrecorded valuable structure a sound generator can reach. The infrastructure that makes the loop reproducible, the miniF2F benchmark (Zheng et al., 2022), the LeanDojo retrieval environment (Yang et al., 2023), and LLM autoformalization (Jiang et al., 2023; Wu et al., 2022), instantiates the verifiable ambient F and the revealed core C our adversary enumerates. On the informal side, prompting and data-augmentation techniques improve mathematical reasoning in language models without any verifier in the loop (Imani et al., 2023; Yu et al., 2024), and research-level benchmarks probe how far this reaches (Zhang et al., 2025); in our terms these pipelines tune the generator, while the model here asks what any such generator can guarantee. None of these systems quantifies the value its perfect verifier cannot locate, which is the gap our dichotomy prices; Ahn et al. (2024); Ju and Dong (2026); Li et al. (2024) survey the area. 47

Flood and Harvest

Interestingness in automated discovery. The question of which true statements are worth stating has a long empirical history in automated mathematical discovery. Early systems such as AM and Eurisko treated discovery as heuristic search: the system did not merely prove given conjectures, but generated concepts, conjectures, and rules for deciding which directions were worth pursuing (Lenat, 1977, 1983). The later HR line made this agenda explicit in automated theory formation, where concept formation, conjecture generation, and theorem proving are coupled with measures of novelty, plausibility, and interestingness (Colton, 2002; Colton et al., 1999). In particular, Colton et al. (2000) study interestingness heuristics in automated mathematical discovery, emphasizing that mathematical output must be filtered not only for correctness but also for significance. More recent work revisits this issue in modern symbolic and learning-based settings: Tsoukalas et al. (2025) learn interestingness measures for automated mathematical theory formation, Herrmann and Schmidhuber (2026) connect interestingness to prospective compression progress, and Wernhard and Zombori (2025) analyze formal proof corpora through grammar compression. These works motivate the distinction that our model makes primitive: validity is not value. Our contribution is orthogonal to the design of interestingness heuristics. We do not define what makes a mathematical statement valuable; instead, we ask what coverage guarantees are possible when value is hidden, validity is checkable, and the generator must pay for unseen value with certified trivia.

H.2

Language generation in the limit

Density and topology. Kleinberg and Wei (2025) introduce the limit-set density that our coverage measure specializes, and Kleinberg and Wei (2026a) push to Banach density and a Cantor–Bendixsonrank dichotomy, a finer density geometry than the lower density our α/2-versus-1 − α/2 split lives in, which we flag as a caution for embedded instantiations. Structural and closure characterizations. Hanneke et al. (2025) show generation is not unionclosed (two generable collections can have a non-generable union), whereas our dichotomy holds inside a single nested collection and is unaffected; Charikar and Pabbaraju (2026) characterize Pareto-optimal non-uniform generation times, optimizing when breadth arrives rather than how much value is covered. Robustness variants. A cluster studies corrupted input: Raman and Raman (2025) and Li and Zhang (2026) on noisy examples, Li et al. (2026b) on contrastive examples, Mehrotra et al. (2026a) on infinite contamination, Mehrotra et al. (2026b) and Li et al. (2026c) on differential privacy. Our revealed core is clean but partial; the missing-value axis is orthogonal to the corrupted-value axis these papers isolate. The safety variant of Anastasopoulos et al. (2026) solves the geometric dual: avoiding a harmful sublanguage rather than covering a valuable one. Model extensions. Li et al. (2026a) move to metric spaces, Høgsgaard and Pabbaraju (2026) to the agnostic setting where the target need not lie in the collection, and Peale et al. (2025) ask outputs to be representative of the target; each enriches the single-language target, where we instead split target from ambient. Racca et al. (2026) study language generation with replay. Ganju et al. (2026) study time-sensitive language generation. Kleinberg et al. (2026a) study language generation in the limit under bounded memory. Kleinberg et al. (2026b) shifts the goal of generation away from the classical time-of-last-mistake measure of generative success toward a new notion of mistake-bounded generation. Computational barriers. Arenas et al. (2026) show generation can be computationally hard even when information-theoretically possible; our generators are arbitrary functions of the prefix, so whether the trivia dichotomy survives an efficiency constraint is open (Section 5).

48

Flood and Harvest

H.3

Classical inductive inference and language identification in the limit

Classical inductive inference. The classical theory of identification in the limit (Angluin, 1979, 1980; Gold, 1967), from the pattern-languages origin to the tell-tale condition, is surveyed in Angluin and Smith (1983); Lange et al. (2008) and the textbook of Jain et al. (1999). A later line studied learners with side information: membership and equivalence queries to the target (Angluin, 1987, 1988) and Turing-degree or query oracles (Gasarch and Pleszkoch, 1989; Stephan, 1998). All these oracles answer about the target; our verifier instead answers about an ambient superset, supplying negatives only outside F and none in the grey zone F \ H, which is exactly why it cannot move the Angluin boundary (Theorem 3.1), and none of these works treats breadth or density. Language identification in the limit with enriched observations. Recent work has revisited language identification in the limit by modifying the information available to the learner. Charikar et al. (2026) revisit the classic language identification problem in the setting where the learner is given the additional power of producing a list of guesses at each time step, while Peng et al. (2026) augment Gold’s model with computational traces of the accepting machine, yielding identifiability across the Chomsky hierarchy under varying corruption tolerances. Relatedly, Papazov and Flammarion (2025) extend Gold’s inductive-inference framework to computable functions under richer forms of observation, including time-bound and policy-trajectory observations, showing that computational side information or complexity restrictions can restore limit-learnability beyond what is possible from input-output data alone. Together, these works illustrate complementary mechanisms for circumventing Gold’s classical negative results by enriching the learner’s observations.

I

A Taxonomy of Generation in the Limit

Table 6 condenses the landscape walked in Section 1.4 and Section H into a single map, arranging the generation-in-the-limit literature along four axes: the structure of the target the adversary commits to, the side information available to the generator beyond the enumerated positives, the success measure, and the headline result. Three patterns organize the table. First, almost every entry enriches exactly one axis of the base model of Kleinberg and Mullainathan (2024) and keeps the others fixed; the table reads as a record of which axes have been explored. Second, every form of side information studied so far answers questions about the target or the collection — membership in the target, negatives of the target, membership in named collection members — and its power tracks whether it can supply a negative example inside the region of uncertainty. Third, the nested pair of this paper is the only entry whose target structure splits into two languages, one containing the other: the verifier answers about a fixed superset of the target, which is why it certifies validity yet cannot locate value (Theorem 3.1). The oracle axis alone is tabulated in finer grain in Section E (Table 2); the two tables are complementary.

49

Table 6: The generation-in-the-limit literature along four axes. Single unknown language from a countable collection, positive enumeration only, unless

stated. The nested pair of this paper is the only entry with an ambient strictly containing the target. Work

Target structure

Side information

Success measure

Main result

exact identification

identification fails beyond restricted classes

exact identification

tell-tale characterization of identifiability

Classical antecedents Gold (1967) Angluin (1980)

single language, full enumera- none tion single language none

Foundations of generation Kleinberg and Mul- single language lainathan (2024) Raman et al. (2025) single language

generation in the limit

union of two collections

every countable collection is generable; generation ̸= identification; breadth sacrificed uniform / non-uniform learning-theoretic landscape of generation none generation negative examples (variant) exact / approximate generation in the statistical model; breadth breadth iff Angluin; negatives restore breadth none exact / approximate the (weak) Angluin characterizations breadth member-queries are insufficient for breadth membership queries to col- breadth variants lection members same-level feedback; noise generation, breadth finite feedback adds nothing; infinite strictly helps none generation generation is not union-closed

single language

none

lower density of the positive density universally achievable limit set lower density tight 1/2 under full enumeration; tight α/2 under partial Banach density dichotomy by Cantor–Bendixson rank

Kalavasis et al. (2025)

single language

Kalavasis et al. (2026)

single language

Charikar and Pabbaraju single language (2025) Bai et al. (2026) single language Hanneke et al. (2025) The density line Kleinberg and Wei (2025)

Kleinberg and Wei (2026b) single language + revealed core none of density α Kleinberg and Wei (2026a) single language none Corrupted or constrained input Raman and Raman (2025) single language Li and Zhang (2026) single language Li et al. (2026b) single language Mehrotra et al. (2026a) Mehrotra et al. (2026b)

single language single language

noisy positives noisy positives contrastive (labeled) examples adversarial contamination none; privacy constraint

generation generation generation

noise-robust generation how much noise generation tolerates the power of contrastive examples

generation private generation

generability under infinite contamination differentially private generation

Flood and Harvest

50

none

Work

Target structure

Side information

Success measure

Main result

Li et al. (2026c)

single language

none; privacy constraint

private identification + differentially private generation in the agnosgeneration tic statistical model

none

safe generation

Enriched goals and ambient structure Anastasopoulos et (2026) Karbasi et al. (2025)

al. language + harmful sublanguage single language + a given generator single language

51 Resource bounds and richer protocols Kleinberg et al. (2026a) Kleinberg et al. (2026b)

generation mistake-bounded generation Arenas et al. (2026) single language none; efficiency constraint computable / efficient generation Botta et al. (2025) fixed known language (no un- process verifier (prefix query complexity of deknown target) queries) coding Charikar et al. (2026) single language none; list outputs list identification Peng et al. (2026) single language computational traces of the identification accepting machine Papazov and Flammarion computable function / learning time-bounded and policy- identification (2025) algorithm trajectory observations this paper

single language single language

none; bounded memory none

generation under memory constraints beyond time-of-last-mistake hard despite information-theoretic possibility cost of verifier-assisted constrained decoding characterization of list identification traces restore identifiability across the Chomsky hierarchy richer observations restore limit-learnability beyond input–output data

nested pair: ambient F ⊋ perfect verifier 1F (an- breadth; sound cov- verifier is not taste (fiber-wise Angluin); target H, core of density α swers about the super- erage; density cover- sound coverage iff verifier, in general; set) age trivia dichotomy α/2 vs. 1 − α/2, jump = unrecorded mass

Flood and Harvest

avoiding the sublanguage: dual of covering value none; variant with labeled hallucination detection impossible from positives; possible with lanegatives beled negatives Peale et al. (2025) none representative genera- outputs must represent the target tion Li et al. (2026a) single language in a metric none approximate generation generation up to metric approximation space Høgsgaard and Pabbaraju target may lie outside the col- none agnostic generation generation in the agnostic statistical model (2026) lection Charikar and Pabbaraju single language none non-uniform generation Pareto-optimal generation times (2026) time Ganju et al. (2026) single language none timeliness trade-off sparse hallucination beats mode collapse Racca et al. (2026) single language none; replay allowed generation with replay repetition changes the achievable set

Flood and Harvest

J

What This Says, and Does Not Say, to Prover Builders

The model is information-theoretic and the dichotomy is an asymptotic statement about guarantees, not a measurement of any deployed system. With that scope fixed, the questions below are the ones practitioners have asked us, with the short answers the theorems license. Our pipeline certifies 105 statements a day, almost all of them shallow. Is that a bug? Not by itself. If the system is to cover valuable statements that the literature has not recorded, an unbounded stream of certified trivia is the provably optimal shape of the generator, not a defect (Theorem 3.6(c)): every generator guaranteeing coverage beyond α/2 emits infinitely many trivia on some instance. What is optional is the rate: the same coverage is achievable with trivia vanishing as a fraction of output (Theorem 3.7). The engineering target licensed by the theory is “make the flood asymptotically negligible,” not “make it finite.” Does filtering trivia out of our published list violate the lower bound? No, but it relocates the guarantee. The dichotomy counts the statements a generator emits, and a published list that contains only finitely many trivia is, as a generator, confined to the α/2 regime (Theorem 3.6(b)). The resolution is to separate streams: an exploration archive that floods, and a curated view filtered from it. The archive carries the coverage guarantee; the view carries the readers. What is α for real mathematics? Unknown, and the results do not need it. α is the density of the recorded literature inside the valuable language, the dichotomy α/2 versus 1 − α/2 holds uniformly in α ∈ (0, 1), and the gap between the two regimes, 1 − α, is precisely the unrecorded mass. The model’s claim is not a value of α; it is that whatever α is, only a flooding generator can buy the unrecorded part. Why is the transition in count rather than rate? Because the adversary can wait. The race of Lemma 3.5 caps any generator at half of whatever the enumeration reveals, and a generator that has budgeted only finitely many probes outside the revealed core exhausts them at some finite time, after which it is locked inside the core forever (Theorem 3.6(b)). Any unbounded budget, however thin its schedule, eventually claims every never-enumerated valuable element (Theorem 3.7(i)). There is nothing in between: every g(N ) → ∞ buys the full 1 − α/2 (Section 5). Would a stronger verifier (a richer logic, a larger library) move the boundary? Not the value boundary. The verifier’s entire informational contribution is to identify the ambient fiber; within a fiber it adds nothing about which statements are valuable (Theorem 3.1), and the dichotomy of Section 3.3 already holds with the ambient fully known. What a verifier does buy is sound coverage, possible with it and impossible without it (Theorem 3.2): it relocates unavoidable errors from false to trivial. Selectivity has to come from examples of value, the enumerated core, not from more verification. Our system never hallucinates. Are we done? You are halfway, and the model says precisely which half. Zero hallucination is the verifier’s gift (Theorem 3.2); the remaining failure mode, triviality, is the one the verifier cannot see, and the dichotomy prices it. A system that never says anything false can still say almost nothing worth recording, and on the tight family it provably must choose between staying near the recorded core (α/2) and flooding toward the rest (1 − α/2). Our generator trains on its own certified output. Does the model cover that? The upper bounds do: our generators are arbitrary functions of the transcript, so every cap in Theorem 3.6 binds any self-improving pipeline a fortiori. The achievability side is information-theoretic and makes no

52

Flood and Harvest

computability claim; whether the dichotomy survives efficiency constraints is open (Section 5), and the complexity barriers of Arenas et al. (2026) suggest the computational story will be genuinely different.

K

Discernment, Selection: A Prehistory of Mathematical Taste

The claim that selection, not production, is the seat of mathematical creativity has a continuous documentary history. We collect it here because the paper’s results give it an edge it did not previously have: what was an aphorism is now the content of a theorem. We add two stations usually left out of the machine-mathematics conversation, Plato and Wittgenstein, because the model takes a side in neither dispute and yet, we will argue, gives each a sharper formulation than its own vocabulary allowed. Plato, or the problem stated. The oldest formulation of unseen value is not Poincaré’s but Plato’s. The paradox of inquiry in the Meno (80d–e) asks how one can search for what one does not know: either one knows it already and the search is idle, or one does not and could not recognize it upon finding it (Plato, 380 BC). Socrates answers with anamnesis: the soul has seen the Forms and inquiry is recollection. Read with modern eyes and without reverence, the paradox is the limit-learning problem stated twenty-three centuries before Gold (1967), and the theory of learning in the limit is its resolution: the dilemma is false because convergence without recognition is possible. A generator can come to produce only members of H while never being in a position to assert that it has identified H, and the separation between generation and identification (Kleinberg and Mullainathan, 2024) makes the gap between the two epistemic states a theorem rather than a confusion. Anamnesis, too, has an exact counterpart: what the recollecting soul contributes is, in our terms, the standing hypothesis that the target lies in a known countable collection H. Without some such prior acquaintance the paradox simply holds; with it, Meno’s challenge is answered not by knowing the answer in advance but by a convergence guarantee. Plato’s myth and the model’s hypothesis class do the same logical work, and it seems to us clarifying, in both directions, to say so. The Republic’s divided line (509d–511e) then supplies the older twin of our central theorem. Plato ranks the mathematician’s faculty, dianoia, reasoning downward from posited hypotheses, below noesis, the unhypothetical grasp of first principles, because the geometer’s certainty is conditional on starting points the method itself cannot interrogate (Plato, 375 BC). The verifier of our model is dianoia built as an interface: it answers exactly the conditional question, does this string follow from what was posited. Theorem 3.1 is the ranking made quantitative: within a fiber the oracle contributes nothing about which valid statements are valuable, so no accumulation of dianoia ascends to noesis, and the step from valid to valuable is not a longer derivation but a different faculty, which in the model is literally a different input channel. Plato placed mathematics below the Forms because its method cannot justify its own hypotheses; the dichotomy adds that the method cannot price its own products either. The modern arc. The modern statement begins with Poincaré (1914), in the 1908 lecture on mathematical invention from which this paper’s epigraph is taken. Producing true combinations “can be done by any one”; the combinations are infinite in number and almost all of them sterile; discovery is discernment, selection. Poincaré went further than the epigraph: he located the sieve in an aesthetic sensibility operating below consciousness, so that the sterile combinations never even present themselves to the inventor’s attention. In our terms he is describing a generator whose proposal distribution already concentrates on H, and asserting, remarkably, that no articulable criterion (no oracle) replaces it. Hardy (1940) made the criterion itself the object of study: a theorem is serious by virtue of the significance of the ideas it connects, unfolded into depth, generality, and unexpectedness, and “beauty is the first

53

Flood and Harvest

test: there is no permanent place in the world for ugly mathematics.” Hardy’s discussion is precisely a predicate on valid statements (his chess problems are genuine and correct mathematics that fails the test): an insistence that H ⊊ F , with the gap inhabited (Figure 1 is Hardy’s point, drawn). Thurston (1994) relocated the question from statements to communities: progress is not the accumulation of proved theorems but the advance of human understanding, and the definition–theorem–proof pipeline misdescribes what mathematicians do and want. Read against this paper, Thurston is a caution we accept in Section 5: the recorded core is an instrument of understanding, and coverage of H is a proxy for the harvest, not the harvest itself. Tao (2025) closes the arc in the machine age: proof assistants and machine collaboration are collapsing the cost of certifying validity, enabling mathematical work organized at scales where no single participant vouches for the whole, which sharpens, rather than retires, the question of what deserves the effort. The interestingness programs of automated discovery, from Lenat (1977) through Colton et al. (2000) to the compression-progress proposals of Herrmann and Schmidhuber (2026), are the engineering record of attempts to mechanize the sieve (Section H). Wittgenstein, or the model’s two channels. Wittgenstein stands on both sides of the model, once early and once late. The Tractatus grants the checker its entire epistemology: the propositions of mathematics are equations and hence pseudo-propositions (6.2) which express no thought (6.21), and “hence there can never be surprises in logic” (6.1251) (Wittgenstein, 1922). This is the membership oracle 1F described from the inside. By the checker’s lights every certified string is the same kind of nothing, which is why nothing in its verdict separates the ornamented 1 + 1 = 2 of the introduction from a theorem; the Tractatus files both under one heading, and the early Wittgenstein would have regarded Theorem 3.1 as obvious. What his doctrine cannot supply is the difference everyone feels between the two, and the later Wittgenstein supplies exactly the missing channel. In the Remarks on the Foundations of Mathematics, a proof does not report a pre-existing fact; it forges a new rule of description and deposits it in a practice (“the mathematician is an inventor, not a discoverer” (Wittgenstein, 1956)), so the meaning of a mathematical sentence is its use, and use is a fact about a community in time. If value is use, two consequences follow for any formal model, and the nested model embodies both. First, there can be no membership oracle for H: the use of a statement lies in the future of the practice, so no present interface can answer for it, and value can enter the model only as data about what the community has in fact taken up: an enumeration of the recorded literature. Second, value so construed is adversarial in exactly Gold’s sense: the modeler does not choose the order in which a practice reveals itself. The two input channels of the nested model, an oracle for F and an enumeration for C, are on this reading the early and the late Wittgenstein installed side by side in one machine: the calculus that can be asked, and the form of life that can only be watched. The dichotomy then has a Wittgensteinian paraphrase that we find arresting: a practice that intends to outgrow its own record must keep asserting sentences that, by its current lights, say nothing, and infinitely many of them (Theorem 3.6(c)). The same asymmetry, four vocabularies. Each generation restated one asymmetry in its own terms: Plato’s Forms beyond the hypotheses, Wittgenstein’s use beyond the calculus, Poincaré’s selection beyond production, Hardy’s seriousness beyond correctness. Production is cheap, verification is mechanizable, selection is neither. The results of this paper are that asymmetry made formal: the verifier certifies the world and cannot rank it (Theorem 3.1), and covering what the literature has not recorded is purchased only in certified trivia (Corollary 3.10). The theorems are metaphysically neutral: they bind whether H is an eternal Form or a moving practice, requiring only that value be a language the generator is never told. That is, perhaps, the most philosophical thing about them: the price of the harvest does not depend on what mathematics ultimately is. Poincaré’s sentence was an observation about human mathematicians; it turns out to be a theorem about all generators, Platonist, formalist, and pragmatist alike. 54