Statopia: A Prover–Library Ecosystem for Automated Formalization and Proof Discovery in Statistics

Summary (Overview)

• Statopia is a co-designed ecosystem consisting of Statopia Prover (a full-stack, self-contained agent for formalizing and proving results in statistics and machine learning) and Statlib (a Lean 4 library built with the prover and organized for automated use).
• The prover operates independently of general-purpose coding agents (e.g., Claude Code, Codex), implementing its own agent loop, context management, proof state, tool execution, and acceptance checks.
• Statopia supports both formal proof discovery (proving statements without supplied proofs) and proof checking (verifying existing natural-language proofs), with Lean 4 as the verification backend.
• The system uses dynamic proof dependency graphs (DAGs) and task groups to enable parallel, resumable proof development at scale.
• Evaluation results show 100% first-run success on 83 statistics benchmark problems and 6 guided IMO 2026 tasks, with paper-scale developments spanning up to 16 tasks and 71,973 Lean lines.

---

Introduction and Theoretical Foundation

Motivation

Theoretical results in statistics and machine learning—such as consistency, convergence rates, coverage guarantees, and generalization bounds—often rely on long, technically delicate proofs. Errors can survive peer review; for example, a typographical error in Livingstone et al. (2019) on the geometric ergodicity of Hamiltonian Monte Carlo left a gap in a corollary proof, later identified by Gruffaz et al. (2026) and corrected in a 2026 corrigendum.

With LLMs now generating statistical arguments at scale, the risk of fluent but incorrect proofs is amplified. Formal verification offers a stronger standard: statements and proofs are expressed in a formal language, and a proof assistant (Lean) checks proofs through a small trusted kernel.

Three Demands Beyond General Mathematics

Statistical results place three additional demands on automated formalization:

1. Faithful formalization requires reconstructing the full statistical setting—data-generating mechanisms, estimators, distributional assumptions, regularity conditions, and asymptotic quantifiers—scattered throughout source materials.
2. Domain-level infrastructure (concentration inequalities, empirical process results, risk decompositions) is needed beyond Mathlib's general foundations.
3. Long proof chains combine probabilistic, analytic, optimization, and matrix reasoning; provers must construct these chains when proofs are incomplete or absent.

Key Design Principle: Reciprocal Development

"Statlib provides the mathematical vocabulary and reusable interfaces needed by the prover, while actual proof development provides evidence for improving the library."

---

Methodology

3.1 Architecture

Statopia Prover is a desktop application (macOS/Windows) with a five-step workflow:

1. Submit — Create workspace, add papers/theorems/Lean developments (proofs optional).
2. Review formal target — Statopia proposes a Lean statement with reconstructed assumptions; user approves or clarifies.
3. Prove locally or in cloud — Lean runs with Mathlib and Statlib on user's machine or cloud host.
4. Monitor and resume — Progress tracked per task; developments can pause and resume from checkpoints.
5. Inspect result — Results marked "Proved" only if the locked statement builds without sorry, passes integrity checks, and uses no prohibited axioms.

3.2 Preparation and Formalization

• Specialized agents formalize target theorems and supporting definitions, compile statements, and review correspondence with sources.
• The formal target is locked after review—proof agents cannot weaken the theorem.
• A natural-language proof guide is developed (from source proofs or devised independently).
• Citation inputs are kept as external nodes by default (deliberate design choice): results from literature are stated in Lean as citation inputs rather than proved, keeping developments manageable and making dependencies explicit. Users can opt for fully self-contained proofs.

3.3 Parallel Proof Development with Proof DAGs

• Nodes = target theorem + intermediate lemmas; edges = proof dependencies.
• External nodes include Statlib theorems (verified), results of other tasks, and citation inputs.
• Separate agents work on different nodes in parallel, each with bounded obligations.
• The DAG is dynamic: new helper lemmas can be added; unsound lemmas revised/withdrawn (with review); only dependent work is redone.

3.4 Task Groups

Four nested organizational levels:

• Workspace → project holding sources, instructions, verified results
• Task group → per target theorem; main task + sub-tasks for supporting results
• Task → complete proof problem with formal target, proof guide, recorded progress
• Proof DAG → remaining proof obligations within each task

4. Statlib Library Design

• Layered architecture: Mathlib (foundations) → statistical vocabulary → operational/bridge lemmas → reusable theorem families → topic/application modules.
• Vocabulary layer: Shared predicates/structures for i.i.d. assumptions, sparsity, smoothness, risks, estimators, etc.
• Naming conventions: PascalCase for structures/classes (e.g., IsSubGaussianVector), snake_case for theorems (e.g., subexp_mgf_le_of_bounded).
• Prover-native retrieval: Search index generated from Lean source; approximate queries with curated statistical synonyms; declarations mechanically checked before use.
• Library evolution: Proof DAGs organized into Statlib source files via reviewed promotion; usage evidence guides interface refinement.

---

Empirical Validation / Results

5.1 Individual Theorem Tasks

Statistics benchmark (83 problems, 12 branches of MSC area 62):

• 100% first-run success rate (83/83) — no proofs supplied, pure formal proof discovery.
• 266 verified DAG nodes (42 main + 224 auxiliary).
• Paired timing comparison with Archon (Codex): Statopia took 9.94% less total elapsed time on 35 problems.

IMO 2026 (6 guided tasks, with natural-language guidance):

• 100% first-run success (6/6) in guided setting.

5.2 Statistical Paper Developments

Key case: CCK comparison — The final covariance-only bound reuses 21 distinct Statlib theorems from 8 modules (29 theorems from 12 modules across the full development). Anti-concentration uses Statlib's Nazarov theorem via a local bridge:

$$\operatorname{Pr}(t < M_Y \leq t + \varepsilon) \leq \frac{\sqrt{2 \log p} + 2}{\underline{\sigma}} \varepsilon, \qquad \varepsilon > 0$$

for centered Gaussian $Y = (Y_1, \ldots, Y_p)$ with $p \geq 2$ and $\operatorname{Var}(Y_j) \geq \underline{\sigma}^2$ for all $j$.

Key case: HMC — Proved corrected Theorem 5.14 (fixed leapfrog steps) with no citation inputs; Theorem 2.2(i–ii) uses one. KAPPA's comparison run located the same gap but left Theorem 2.2 unfinished due to an encoding error.

5.3 Neural Network Approximation → Statlib

A completed proof development formalizing Kohler & Langer (2021) was organized into 7 Statlib modules (55,922 lines) under Statlib/Nonparametric/. The final theorem:

For dimension $d > 0$, integer $r \geq 0$, exponent $0 < \beta \leq 1$, $s = r + \beta$, there exist constants such that for every integer $M \geq M_0$ and Hölder-smooth $f$ on $[0,1]^d$, a ReLU network with depth $L_M = (D_{\text{block}} + 1)M^d$, width ≤ $W_0$, satisfies:

$$|g(x) - f(x)| \leq c_{\mathrm{State}} M^{-2s}, \qquad x \in [0,1]^d$$

Equivalently, in terms of depth:

$$|g(x) - f(x)| \leq C_{\mathrm{rate}}(L_M W_0^2)^{-2s/d}, \qquad x \in [0,1]^d$$

with $C_{\mathrm{rate}} = c_{\mathrm{State}}((D_{\mathrm{block}} + 1)W_0^2)^{2s/d}$.

---

Theoretical and Practical Implications

Contributions to Automated Formalization

1. Native proving runtime: Statopia demonstrates that a purpose-built proving system (rather than a general coding-agent harness) can effectively manage the unique demands of statistical proof development—context management, tool scheduling, Lean verification, and recovery.

2. Co-designed ecosystem: The reciprocal development principle—where the library supports proving and proving drives library evolution—provides a model for sustainable formalization infrastructure.

3. Proof discovery without proofs: The 100% success rate on 83 benchmark problems with no supplied proofs demonstrates that automated provers can develop mathematical arguments independently, not merely check existing ones.

4. Parallel proof development: Dynamic proof DAGs with parallel agents, resumable checkpoints, and task-group coordination offer a practical architecture for long-horizon formalization.

Practical Implications for Statistics and ML

• Verification of published results: The HMC case shows the system can identify and formally address gaps in published proofs (including corrigenda).
• Reusable infrastructure: Statlib's layered design (vocabulary → operational/bridge lemmas → theorem families) enables composition of results across developments (e.g., 21 distinct Statlib theorems reused in the CCK proof).
• Cost-effectiveness: Mean cost of $0.57 per benchmark problem and $0.00125 per Lean line make formal verification economically feasible at scale.

---

Conclusion

Statopia connects formal library construction with automated formalization and proving in statistics and machine learning. Key achievements:

• Statopia Prover: Full-stack agent with own agent loop, proof state, and acceptance checks; supports proof discovery and checking; parallel development via dynamic proof DAGs.
• Statlib: Substantial Lean 4 library (1,807 theorems, 1,035 lemmas, 470 files as of Nov 2026) covering high-dimensional, nonparametric, and other statistical areas; organized for agent retrieval and reuse.
• Cross-platform application: Interactive workspace for local or cloud execution with resumable tasks.

Limitations

• Formalization and proof construction can still require substantial time.
• Some tasks may remain unresolved due to missing infrastructure or undetectable proof routes.
• Repeated retrieval, interface adaptation, and iterative repair can prolong execution.

Future Directions

1. Optimize workflow: Better proof route selection, reduced redundant retrieval/repair, more effective parallel coordination.
2. Expand Statlib coverage: Additional foundational infrastructure and reusable results from new formalization projects.
3. Scale platform: Server/cluster deployments with distributed execution, task scheduling, and resource management for concurrent users and larger workloads.