Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao
We prove that to cover all valuable mathematics verified by a formal proof checker, one must generate infinitely many trivial but true statements.
AI systems coupled to proof assistants now generate formal mathematics at scale, but the gap between what a checker can verify and what a mathematician would value has become the binding constraint. This work theoretically models the relationship between verifiability and value to reveal the inevitable limits in generating valuable mathematics.
Borrowing the concept of language generation in the limit, we define a verifiable formal language F and a valuable language H, with a core C ⊆ H given as the literature. The generator outputs only statements in F, classified as valuable (H), trivial (F\H), or hallucination (outside F). We formalize and prove four questions: (1) the verifier cannot substitute for taste, (2) the verifier enables sound coverage, (3) optimal coverage sharply depends on the number of trivial statements (finite: α/2, infinite: 1-α/2), and (4) both regimes are instantiable in a compression model.
We theoretically prove a fundamental gap between verifiability and value, showing that even a perfect verifier requires infinitely many trivial statements to cover all valuable mathematics. This suggests that 'useless' outputs in AI mathematics generation are not an engineering accident but an inevitable phenomenon.