Agentic theorem provers -- pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, 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 time-bounded MDPs. Exploiting Bellman structure, we prove existence of optimal policies under mild regularity, derive 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.

翻译：智能定理证明器——将数学推理模型与库检索、子目标分解/搜索规划器以及证明辅助验证器相结合的流水线——最近取得了显著的实证成功，然而，究竟是哪些组件驱动了性能，以及为何此类系统能够在证明搜索这一经典难题中发挥作用，目前仍不清楚。我们提出一种分布视角，引入**统计可证性**，其定义为在实例分布上平均的、在有限时域内达到已验证证明的成功概率，并将现代定理证明流水线形式化为时间有界的马尔可夫决策过程。利用贝尔曼结构，我们在温和的正则性条件下证明了最优策略的存在性，通过次/超解不等式推导出可证性证书，并从近似误差、序列统计复杂度、表示几何（度量熵/倍增结构）以及动作间隙尾部分布等方面，界定了分数引导规划（贪婪/前k/束搜索/滚动）的性能差距。综合而言，我们的理论为智能定理证明器何时以及为何能在有偏的真实世界问题分布上取得成功，提供了一个原则性的、对组件敏感的解释，同时阐明了其在最坏情况或对抗性机制下的局限性。