A perfect proof checker cannot replace taste: formal results show that to cover unrecorded valuable mathematics an AI must produce an infinite stream of certified but trivial statements, and generators face a sharp coverage jump — from α/2 to 1−α/2 — once they allow infinitely many trivia.

Main Finding

A perfect proof checker (verifier) cannot substitute for mathematical taste. When a generator must only emit strings inside a verifiable formal language F but seeks to recover as much of an unknown valuable language H ⊆ F as possible, there is a provable, sharp trade-off controlled by the amount and type of trivial (valid-but-worthless) output the generator is allowed. Concretely, for a revealed core C ⊆ H of lower density α (the recorded literature), generators that emit only finitely many trivia can at best cover α/2 of the valuable statements, while any generator that emits infinitely many trivia—even at vanishing rate—can attain coverage 1 − α/2. Thus an unbounded stream of certified trivia (the “flood”) is a theoretical necessity to harvest the unrecorded valuable mathematics (the “harvest”) beyond the α/2 barrier.

Key Points

• Model and objects

  • Ground set U (countable ordered strings). Two nested infinite languages: F (formal/verifiable; oracle membership available) and unknown H (valuable), with an adversary revealing a core C ⊆ H of lower density α (the literature).
  • Generator sees an adversarial enumeration of C over time and may query the oracle 1F. Outputs must be fresh strings; each output is either hallucination (/∈F), trivial (∈F \ H), or valuable (∈H \ seen).
  • Coverage measured by lower density of O ∩ H relative to H (limit-set density).

• Four principal theoretical results

• Verification is not taste (Theorem 3.1): Giving the generator a perfect membership oracle for F only identifies the ambient F; within F the oracle provides no information about H. Collections admitting breadth with a verifier are exactly those in the oracle-free model, characterized fiber-wise by Angluin’s tell‑tale condition. Taste must come from examples (the core), not the checker.
• Verifier → sound coverage (Theorem 3.2): The verifier enables “sound coverage” (cover every unseen valuable statement while never emitting non-F outputs). The exhaustive generator Gn = F \ Sn achieves this; without the oracle, some collections cannot be sound-covered. The verifier relocates unavoidable errors from false outputs (/∈F) to trivially valid but worthless outputs (F \ H), but cannot reduce their amount or locate value.
• Trivia phase transition / dichotomy (Lemma 3.5, Theorems 3.6–3.7, Corollary 3.10): For the tight family (canonical core presentation, C as candidate intersection) there is a two-regime optimality: - Finite-trivia generators: optimal coverage = α/2. - Any infinite-trivia generator (even with extremely sparse rate, e.g., O(N−1/2) trivia in first N rounds): optimal coverage = 1 − α/2. The transition depends on the count (finite vs infinite) of trivia, not on the asymptotic rate. The gap 1 − α between these optima equals the unrecorded mass of valuable statements (H \ C). Any generator exceeding α/2 must emit infinitely many trivia.

• Instantiation in a compression model (Theorem 4.1, Propositions 4.2–4.3): The dichotomy is realized in a concrete macro-dictionary/compression model (Aksenov et al., 2026). Structured (abelian refinement chains) regimes can avoid trivia entirely; free-monoid dictionary pairs realize the tight family for any rational α. The exhaustive generator’s precision is polynomially small in radius, while the “sweep” generator’s precision tends to 1.

• Mechanisms / proof ingredients

  • Fixed-advice relativization lets oracle-free characterizations transfer to each F-fiber.
  • Sandwich-exclusion lemma proves impossibility of sound-covering both a chain member and its union on the same seen-prefix.
  • Race lemma + sweep pointer: adversarial “race” enumeration of the core yields α/2 lower bounds for finite-trivia strategies; a sparse “sweep” schedule of candidate-intersection items attains 1 − α/2 when trivia are infinite.

• Robustness claims

  • The necessity of trivia is information-theoretic and combinatorial: the verifier cannot inform which valid statements are valuable.
  • The “infinite but asymptotically negligible” trivia stream is sufficient; in practice this means arbitrarily sparse certified trivia suffice provided they continue indefinitely.

Data & Methods

• Nature of the work: pure theory / formal modeling. No raw empirical datasets; appendices include numerical validation and worked examples for intuition.
• Model specifics
  • Countable universe U with canonical order; languages F and H infinite subsets of U.
  • Adversarial online protocol: adversary fixes (F, H) and enumerates a core C ⊆ H; the generator sees prefixes St and must output fresh elements.
  • Two generator types used in analysis: set-valued generators (breadth analyses, KMV conventions) and element-based generators (density / limit-set analyses, KW conventions).
  • Coverage measured by limit-set lower density (as in Kleinberg & Wei).
• Main analytical tools and constructions
  • Angluin’s tell-tale condition and its weak form used (relativized) to characterize breadth in fibers.
  • Constructions: exhaustive generator Gn = F \ Sn (sound, but imprecise); sweep generator that interleaves sparse targeted outputs (requires emitting infinitely many trivia).
  • Adversarial enumerations (“race”) that force generators to read the same prefix when truths differ, yielding coverage caps.
  • Instantiations inside a compression (macro-dictionary) model: abelian refinement chains and free-monoid pairs verifying the abstract conditions.
• Validation: mathematical proofs for all theorems (deferred proofs in appendices), plus numerical experiments and a worked miniature in appendices to illustrate the dichotomy.

Implications for AI Economics

• Verifier vs taste: where to invest?
  • A perfect verifier (proof checker) is necessary but insufficient for delivering economically valuable mathematical outputs. Investment in proof-checking infrastructure alone will not raise the “value per proof” produced by automated provers.
  • Value accrues from curated examples / taste signals (increasing the recorded core C or otherwise labeling which valid statements are valuable). Funding and economic incentives should prioritize creating, curating, and maintaining such labeled corpora.
• Cost structure and production strategies
  • Producing certified trivia is computationally cheap; generating useful but still-unknown valuable statements requires either curated exemplars or accepting an ever‑continuing stream of trivia.
  • Firms can cheaply “flood” consumers with verifiable but trivial outputs; because a sparse infinite stream of trivia suffices to achieve high coverage of unrecorded value, producers can minimize cost per valuable discovery by interleaving rare trivia among otherwise trivial certified outputs. This creates an asymmetry: marginal computational cost near-zero, while human attention and curation cost remain high.
• Market design and business models
  • There is an economic opportunity for “taste” services: human or ML modules that label, rank, or curate verifiable outputs. These services become scarce and valuable since they supply the information (taste) the verifier cannot.
  • Product design should separate verifier functionality (cheap, commoditized) from taste/curation (value-bearing, monetizable). Monetization could follow models akin to data curation, premium filters, or expert verification.
• Incentives and externalities
  • Generators incentivized only by verifiability may maximize trivially valid output, degrading downstream utility (attention costs, filtering burden). Platforms must design incentives (rewards, reputation, filtering penalties) to align producers toward producing genuinely valuable content or to compensate curators.
  • The required “flood” creates a persistent noise externality; markets or platforms that internalize this cost (e.g., charging for attention, rewarding curation) will be more efficient.
• Policy and public goods
  • Public funding for formalization and recording of valuable mathematics (increasing α) reduces the unrecorded mass and thus lowers the need for heavy exploration via trivia. Investments in shared labeled corpora are public good investments that improve the return on automated proving systems.
  • Standards and benchmarks should measure not only syntactic correctness but also coverage of unrecorded valuable content; new metrics could track limit-set coverage proxies or curate representative core exemplars to evaluate “harvest” performance.
• Practical takeaways for deployers
  • Expect systems that couple perfect checkers with generative models to produce many certified but low-value outputs; this is not a bug but a provable feature when taste is unavailable.
  • To scale economically useful discovery, combine (a) a verifier, (b) curated example corpora or taste models, and (c) selection/curation pipelines (human-in-the-loop or learned) that convert the flood into a usable harvest.
  • Sparse, ongoing injections of curated trivia or labeled interesting items are disproportionately valuable: they enable generators to leverage the flood economically while keeping additional production costs low.

Overall, the paper reframes an engineering puzzle (“too many worthless but correct theorems”) as an information‑theoretic economic one: verification enforces truth but not value; extracting the economic value of machine-generated mathematics requires investment in taste—curation, examples, and selection mechanisms—which should be central in AI economics planning, pricing, and platform design.