Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
06:00 · June 23, 2026 · arXiv cs.AI RSS
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.
Summary
A multi-agent system developed for Lean 4 addresses the formalization of asymptotic statistical theory, a domain whose proofs combine convergence statements, asymptotic expansions, functional analysis, and regularity conditions that sit far from existing Mathlib infrastructure. The pipeline is orchestrated by a manager agent that assigns tasks to seven specialist roles covering proof planning, skeleton scaffolding, Mathlib reconnaissance, proof construction, integration, independent review, and audit. Work proceeds through isolated git worktrees and reviewed merges onto a buildable trunk, allowing reconnaissance and reusable infrastructure to be separated from theorem-specific assembly.
The central control mechanism is a hypothesis-disciplined audit performed by a dedicated Auditor agent. For every main theorem and each field in the supporting concept definitions, the Auditor records a classification together with a verbatim excerpt and page reference from the chosen source text, typically van der Vaart’s Asymptotic Statistics. Hypotheses may be accepted only when they are directly anchored in the prose, explicitly justified as Lean encoding adapters, or marked as source-implied; unsupported strengthenings are rejected before they propagate. This discipline prevents two common failure modes: hypothesis laundering, in which missing proof obligations are quietly added to theorem signatures, and definition drift, in which they are hidden inside layered concept definitions.
The resulting open-source library separates theorem-agnostic probability and analysis components from statistical concept definitions such as differentiability in quadratic mean, score functions, and Fisher information. It supplies Lean-checked and human-audited proofs of five cornerstone results on asymptotic distributions and efficiency bounds for both parametric and semi-parametric models. The repository is structured so that later formalization efforts can reuse both the mathematical bricks and the multi-agent workflow itself.
Why it matters
This research is highly relevant for Dutch AI researchers specializing in formal methods, logic, and statistical learning. The multi-agent approach to automated theorem proving in Lean 4 offers actionable methodologies for academic institutions and R&D centers in the Netherlands focused on transparent and verifiable AI.
