Certified but Not Useful: An Information-Theoretic Ceiling on LLM-Based Mathematical Discovery

We prove an information-theoretic ceiling for verifier-mediated LLM agents: in any hidden-world, no-side-channel verifier model with disjoint success sets, no admissible policy—at any query budget—has equal-prior success probability above $(1+{\delta }_{\Gamma })/2$, where ${\delta }_{\Gamma }$ is the total-variation distance between the laws of the complete verifier signature. The ceiling depends on the interface and environment pair, not the agent; exact maxima meet it in all 423 finite ${\mathcal{G}}_3$ worlds. It is vacuous precisely when ${\delta }_{\Gamma }=1$, meaning that the complete signature distinguishes the environments almost surely; public input revealing the target is sufficient, but not necessary. A companion result gives a minimax $\Theta (d)$ checker-call separation between charged rebuilding and free frame restoration in an opaque marked-leaf model. A usefulness interpretation of the ceiling requires success sets that encode held-out utility. We define statistical discoverability as the probability that a research procedure returns an artifact that is both certified and useful on sealed theorems. Separately, we observe that installing a checker-certified library lowered held-out solve rate by $0.375$ (95% CI $[-0.50,-0.24]$; 10 of 12 paired cells negative, none positive; $b=16384$), and every added failure was a completed proof the checker rejected, not truncation or timeout. The measured harm is a post-freeze utility contrast on four worlds with a fixed solver, not an estimate of discoverability or a test of the ceiling; ${\delta }_{\Gamma }$ is unmeasured in these runs. Together, the framework opens a principled path for analyzing what LLM-based agents can and cannot formally guarantee in automated mathematics.