# Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory

arXiv: https://arxiv.org/abs/2606.20642 · HTML: https://mlsanity.com/paper/2606.20642/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 35 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Builds on (most cited first, 20 of 20)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://mlsanity.com/paper/2510.08988/) (2025)
- [A formally verified proof of the Central Limit Theorem](https://mlsanity.com/paper/1405.7012/) (2014)
- [Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning](https://mlsanity.com/paper/2604.19459/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral](https://mlsanity.com/paper/2503.19605/) (2025)

## Built on by (most cited first, 1 of 1)

- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)

## Abstract (arXiv)

Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large gap from existing infrastructure in Lean 4 formalization. To address these challenges, we propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents: a manager that coordinates seven specialist roles for proof planning, skeleton scaffolding, Mathlib reconnaissance, proof construction, integration, independent review, and audit. The main methodological discipline is the hypothesis-disciplined audit, implemented by the Auditor agent: every main-theorem hypothesis and concept-layer field must be anchored in the source mathematical prose, justified as a Lean encoding adapter, marked as source-implied, or rejected as an unsupported strengthening. Using this workflow, we build a systematic formalization of asymptotic statistical theory, especially the parametric and semi-parametric models' asymptotic distribution and efficiency results. The resulting Lean development is axiom-clean and source-faithful, with Lean-checked and human-audited proofs of core parametric and semi-parametric theorems organized so that theorem-agnostic infrastructure and statistical concept definitions are separated from theorem-specific assembly. The formalization results are available at https://github.com/junwei-lu/Lean-Asymptotic-Statistical-Theory.