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

Agentic theorem provers combine a reasoning model, retrieval, search, and a proof assistant verifier, yet it remains unclear which components actually improve finite-budget proof success and why they help on real mathematical workloads. We study this question through statistical provability: the probability of reaching a verified proof within a budget on a specified stream of theorem instances. We model formal proof search as a finite-horizon reachability MDP with deterministic verifier dynamics, and show that under a faithful state abstraction the optimal success probability coincides with ordinary syntactic provability. We then analyze a simple but practically important pipeline: depth-wise offline action-value regression followed by greedy test-time proving. Our main theorem bounds the provability gap between the learned prover and the optimal prover by an occupancy-weighted sum of uniform action-value errors; in the common uniform-error reading, the leading complexity multiplier is the learned prover's average truncated proof length. The error decomposes into approximation error, geometric coverage of the training distribution, and Monte Carlo label noise, and improves to a fast rate under an action-gap margin condition. The result gives a component-sensitive account of why verifier feedback, retrieval, representation geometry, and proof-shortening mechanisms help on biased theorem workloads, without contradicting classical worst-case hardness.

AI systems can now solve many math problems, but formal mathematics requires more than a plausible answer: the system must produce a proof that a proof assistant can check. Modern theorem provers combine a large language model with search, library retrieval, and a verifier, but it is not obvious why this works when proof search is very hard in the worst case. We study the practical question: on the kinds of theorem problems the system actually sees, how likely is it to find a checked proof before its compute budget runs out? We model proving as a step-by-step decision process in which every attempted proof step is checked by the verifier. Our theory shows that success depends on measurable quantities: score accuracy, coverage of the visited proof states, verifier-backed label noise, how clearly good steps beat bad ones, and how long proofs tend to be. The average proof length acts like a complexity multiplier: shorter typical proofs make local prediction errors less damaging. This explains why retrieval, better representations, verifier feedback, and proof-shortening methods can improve performance on structured theorem workloads without contradicting worst-case hardness.