Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models

Agentic theorem provers---pipelines that couple a mathematical reasoning model with library retrieval, decomposition/search, and a proof assistant verifier---have recently achieved striking empirical success, yet it remains unclear which components drive performance and why such systems work at all despite classical hardness of proof search. We propose a distributional viewpoint and introduce \textbf{statistical provability}, defined as the finite-horizon success probability of reaching a verified proof, averaged over an instance distribution, and formalize modern theorem-proving pipelines as \textbf{time-bounded reachability MDPs}. Exploiting Bellman structure, we prove existence of optimal policies under mild regularity, derive \textbf{provability certificates} via sub-/super-solution inequalities, and bound the performance gap of score-guided planning (greedy/top-(k)/beam/rollouts) in terms of approximation error, sequential statistical complexity, representation geometry (metric entropy/doubling structure), and action-gap margin tails. Together, our theory provides a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions, while clarifying limitations in worst-case or adversarial regimes.