Overview
arXiv: 2606.14688 — Xiaoyu Li, Andi Hall (Andi Han), Dai Shi
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. The paper models 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, revealed only through an adversarial enumeration of a core C ⊂ H of exact density alpha (the literature). Every output is valuable (in H), trivial (in F \ H), or a hallucination (not in F).
Key Results
1. The verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wise by Angluin-type conditions.
2. The verifier does buy reliable coverage: with a verifier, coverage of all unseen valuable statements is possible while asserting only valid statements; without it, this is impossible. The verifier relocates unavoidable errors from falsehoods to trivialities.
3. Sharp dichotomy (core contribution): on tight families, a generator emitting a finite amount of trivial statements achieves optimal coverage alpha/2, while any unbounded stream of trivial statements—even at a vanishing rate—jumps the optimum to 1 − alpha/2. Both bounds are tight, and a single generator can attain both endpoints. The transition lies in the *amount* of trivial output, not the rate; the gap 1 − alpha is unrecorded quality.
4. Instantiation: both regimes are realized in models of mathematical compression.
Takeaway
A perfect verifier cannot substitute for taste: an unbounded stream of correct-but-worthless statements is not an engineering accident but a provable necessity, since covering unrecorded valuable mathematics requires an infinite yet asymptotically negligible flood of certified trivial statements.
---
*Auto-collected 2026-06-16*