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

> Statopia's prover-library ecosystem achieves 100% first-run formal proof discovery on 83 statistics benchmarks at $0.57 per problem.

- **Source:** [arXiv](https://arxiv.org/abs/2611.11110)
- **Published:** 2026-11-14
- **Permalink:** https://picx.dev/p/07A7b4
- **Whiteboard:** https://picx.dev/p/07A7b4/image

## Summary

# 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):

| Proof procedure | Problems | Lean lines | Mean min. | Mean USD | USD/line |
|---|---|---|---|---|---|
| Single file | 41 | 5,192 | 32.81 | 0.22 | 0.00174 |
| Dynamic DAG | 42 | 32,510 | 89.80 | 0.90 | 0.00117 |
| **Combined** | **83** | **37,702** | **61.65** | **0.57** | **0.00125** |

- **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):

| Task | Time (min.) | Lean lines | USD | USD/line | Reference Time (min.) |
|---|---|---|---|---|---|
| Problem 1 | 37.63 | 720 | 0.88 | 0.00122 | 24 |
| Problem 2 | 264.93 | 4,410 | 12.90 | 0.00293 | 360 |
| Problem 3 | 292.68 | 7,680 | 10.89 | 0.00142 | 869 |
| Problem 4 | 36.03 | 549 | 0.41 | 0.00074 | 39 |
| Problem 5 | 23.61 | 402 | 0.28 | 0.00069 | 65 |
| Problem 6 | 50.54 | 1,214 | 0.81 | 0.00067 | 139 |
| **Total** | **705.42** | **14,975** | **26.17** | **0.00175** | **1,496** |

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

### 5.2 Statistical Paper Developments

| Target | Files | Lines | Tasks (pass/total) | External citations |
|---|---|---|---|---|
| Gaussian approximation (Lopes et al., 2020), Thm. 3.1 | 88 | 15,047 | 6/6 | 3 |
| CCK comparison (Chernozhukov et al., 2015), Thm. 2 | 78 | 12,223 | 6/6 | 1 |
| Dynamic matrix recovery (Chen et al., 2024), Thm. 1 | 28 | 4,827 | 2/2 | 0 |
| DCF test (Xue & Yao, 2020), Thm. 1 | 164 | 41,336 | 5/5 | 1 |
| Residual spectral matching (Chen & Yao, 2024), Thm. 4.1 | 329 | 71,973 | 5/5 | 5 |
| Repeated deep regression (Yan et al., 2025), Thm. 2.1 | 44 | 8,774 | 4/4 | 2 |
| Nonparametric prior learning (Jia et al., 2026), Thm. 2.4 | 43 | 8,159 | 1/1 | 1 |
| ProTrans (Chen et al., 2026), Thm. 1 | 88 | 11,643 | 10/10 | 0 |
| DP clustering (Ascolani et al., 2023), Thm. 1 | 218 | 34,932 | 16/16 | 0 |
| HulC (Kuchibhotla et al., 2024), Thm. 1 | 15 | 1,397 | 2/2 | 0 |
| EILLS (Fan et al., 2024), Thm. 4.2 | 11 | 2,079 | 1/1 | 0 |
| HMC (Livingstone et al., 2019), Thm. 2.2(i–ii) & Thm. 5.14 | 73 | 7,214 | 8/8 | 1 |

**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.

---

_Markdown view of https://picx.dev/p/07A7b4, served by PicX — AI-generated visual whiteboard summaries of research papers._