Paper Overview
Field: CL (Computation and Language) Authors: Xiaoyu Li, Andi Han, Dai Shi Published: 2026-06-12 arXiv: 2606.14688
English Translation of the Summary
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 authors 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, revealed only through an adversarial enumeration of a core C — a subset of H of exact density alpha (the literature). Every output is valuable (in H), trivial (in F \ H), or a hallucination (not in F).
The paper settles four questions:
1. The verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wise by the Angluin condition.
2. The verifier does buy reliable coverage: with it, coverage of all unseen valuable statements is possible while only asserting valid statements; without it, this is impossible. It repositions inevitable errors from false to trivial.
3. The central result — a sharp dichotomy on tight families: generators emitting finitely many trivial statements achieve optimal coverage alpha/2, whereas any infinite stream of trivial statements — even at a vanishing rate — jumps the optimum to 1 - alpha/2 (both bounds are tight for cores presenting as candidate intersections), and a single generator attains both endpoints. The transition lies in the *number* of trivial statements, not the rate; the gap 1 - alpha is the unarchived mass.
4. Both regimes are instantiated in mathematical compression models.
Conclusion: A perfect verifier is no substitute for taste — the unbounded stream of correct-but-unvaluable statements is not an engineering accident but a provable necessity, since covering unarchived valuable mathematics requires an infinite yet asymptotically negligible flood of certified trivial statements.
--- *Auto-collected on 2026-06-16*