Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit
- URL: http://arxiv.org/abs/2606.14688v1
- Date: Fri, 12 Jun 2026 17:52:24 GMT
- Title: Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit
- Abstract summary: We model the generation of valuable mathematics as nested language generation in the limit.<n>Every output is valuable ($in H$), trivial ($in F set H$), or a hallucination ($notin F$)
- Score: 42.15597840680038
- License: http://creativecommons.org/licenses/by/4.0/
- 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 \in \mathcal{H}$ revealed only through an adversarial enumeration of a core $C \subseteq H$ of exact density $α$ (the literature). Every output is valuable ($\in H$), trivial ($\in F \setminus H$), or a hallucination ($\notin F$). We settle four questions. First, the verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wise by Angluin's condition. Second, the verifier does buy sound coverage, covering all unseen valuable statements while asserting only valid ones: possible with it, impossible without it; it relocates unavoidable errors from false to trivial. Third, and centrally, a sharp dichotomy on the tight family: generators emitting finitely many trivia achieve optimal coverage $α/2$, while any infinite trivia allowance, even at vanishing rate, jumps the optimum to $1-α/2$ (both tight, for cores presented as the candidate intersection), and one generator attains both ends. The transition is in trivia count, not rate; the gap $1-α$ is the unrecorded mass. Fourth, both regimes instantiate in a compression model of mathematics. A perfect verifier cannot substitute for taste: the unbounded stream of correct-but-worthless statements is not an engineering accident but a provable necessity, since covering unrecorded valuable mathematics requires an infinite, but asymptotically negligible, stream of certified trivia.
Related papers
- Optimal entanglement-assisted source coding under a balanced-difference promise [0.0]
Entanglement can reduce the communication required for coding tasks, but establishing the minimum achievable cost is essential to understanding its limits.<n>We address this question in a zero-error source-coding task where Alice receives a word and Bob knows an unordered pair of candidates containing it.<n>We prove that the task requires exactly $n$ messages when $(q-1)ell$ is even and two messages when it is odd.
arXiv Detail & Related papers (2026-09-14T15:43:27Z) - Signed Sensitivity of Expected Hitting Time to Mutation Rate in the (1+1) EA: Per-State Sign Theorems and Verifiable Certificates for Non-Lumpable Families [0.0]
We study the sensitivity of the expected hitting time $H_p=mathbbE_x T$ to the mutation rate.<n>Two fitness functions share the entire one-step success-rate curve, yet their expected hitting times are two different exact rational numbers.
arXiv Detail & Related papers (2026-09-11T07:14:28Z) - The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
In [AS21], Axiotis and Sviridenko conjectured that the linear dependence on the restricted condition number in convex optimization cannot be improved by a sparse-time algorithm.<n>We establish their conjectured lower bound for least-squares objectives, conditional on the randomized exact-volume Small-Set Expansion Hypothesis.
arXiv Detail & Related papers (2026-08-03T17:57:01Z) - Reading Without a Reader: Large Language Models Collapse Reading and Writing into a Single Entangled Code [0.0]
We show that a decoder-only large language model drives both from one autoregressive path optimized on text.<n>We ask how entangled it is, comparing an input-side reading code'' $mathbfW_E$ with an output-side writing code'' $mathbfW_U$.<n>For minimal pairs the alexia analogue is empty by theorem; greedy production implies a vocabulary-wide argmax, so it wins the pairwise ranking.
arXiv Detail & Related papers (2026-07-02T16:21:41Z) - Odds Law: The Decomposition Algebra On How Intelligence Organizes Itself to Solve Difficult Problems Reliably [0.5414847001704247]
We show that reliability is bought with independent information arranged by composition, and bounded by the verifier.<n>In short, reliability is neither free nor magical: it is bought with independent information, arranged by composition, and bounded by the verifier.
arXiv Detail & Related papers (2026-06-14T09:53:11Z) - Quantum Colorings of Spheres [0.0]
We show that if $Sn-1$ is quantumly $n$-colorable, then either $n=2$ or $n$ is a multiple of 4, and show that the converse holds whenever a Hadamard matrix of order $n$ exists.<n>It also follows from this equivalence that $Sn-1$ admits a rank-one quantum $n$-coloring if and only if $n in 2,4,8$, thereby settling a conjecture of Zeng and Zhang.
arXiv Detail & Related papers (2026-06-09T13:49:08Z) - Scale-Sensitive Shattering: Learnability and Evaluability at Optimal Scale [54.65053906803857]
We study the optimal scale at which real-valued function classes exhibit uniform convergence and learnability.<n>Our main result establishes a scale-sensitive generalization of the fundamental theorem of PAC learning.<n>We also highlight several open questions on quantitative sample complexity and evaluability.
arXiv Detail & Related papers (2026-05-13T15:41:30Z) - $k$-server-bench: Automating Potential Discovery for the $k$-Server Conjecture [4.29490433621832]
We introduce a code-based challenge for automated, open-ended mathematical discovery based on the $k$-server conjecture.<n>The task is to discover a potential function satisfying a large graph-structured system of simple linear inequalities.<n>Our results suggest that the task is challenging but plausibly within reach of current methods.
arXiv Detail & Related papers (2026-04-08T16:06:43Z) - Hardness of High-Dimensional Linear Classification [58.29089693778071]
We establish new exponential in dimension lower bounds for the Maximum Halfspace Discrepancy problem.<n>Both are fundamental problems in computational geometry and machine learning in their exact and approximate forms.
arXiv Detail & Related papers (2026-03-19T15:53:41Z) - Language Generation and Identification From Partial Enumeration: Tight Density Bounds and Topological Characterizations [1.6203023551115867]
We study the framework of emphlanguage generation in the limit, where an adversary enumerates strings from an unknown language.<n>We show that generation in the limit remains achievable, and if $C$ has lower density $alpha$ in $K$, the algorithm's output achieves density at least $alpha/2$.<n>We characterize when identification in the limit is possible -- when hypotheses $M_t$ eventually satisfy $C subseteq M subseteq K$.
arXiv Detail & Related papers (2025-11-07T14:56:04Z) - Burau representation, Squier's form, and non-Abelian anyons [53.92822954974537]
We introduce a frequency-tunable, two-dimensional non-Abelian control of operation order constructed from the Burau representation of the braid group $B_3$.<n>The sign change of $Delta(omega)$ across the Squier positivity window reveals alternating constructive and destructive interference of causal orders.<n> Numerical simulations confirm both enhancement and suppression regimes, establishing a minimal $B_3$ braid control.
arXiv Detail & Related papers (2025-10-21T00:25:21Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
arXiv Detail & Related papers (2025-06-05T03:16:08Z) - The Aldous--Lyons Conjecture II: Undecidability [3.8370118222043694]
We show that given a tailored non-local game $G$, it is undecidable to distinguish between the case where $G$ has a special kind of perfect strategy, and the case where every strategy for $G$ is far from being perfect.<n>Using a reduction introduced in the companion paper [BCLV24], this undecidability result implies a negative answer to the Aldous--Lyons conjecture.
arXiv Detail & Related papers (2024-12-30T22:59:56Z) - Matrix hypercontractivity, streaming algorithms and LDCs: the large alphabet case [3.729242965449096]
We consider streaming algorithms for approximating the value of Unique Games on a hypergraph with $t$-size hyperedges.
We show that every streaming algorithm in the adversarial model achieving an $(r-varepsilon)$-approximation of this value requires $Omega(n1-2/t)$ quantum space.
arXiv Detail & Related papers (2021-09-06T16:56:19Z) - Quantum double aspects of surface code models [77.34726150561087]
We revisit the Kitaev model for fault tolerant quantum computing on a square lattice with underlying quantum double $D(G)$ symmetry.
We show how our constructions generalise to $D(H)$ models based on a finite-dimensional Hopf algebra $H$.
arXiv Detail & Related papers (2021-06-25T17:03:38Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.