{"id":"arxiv/2606.20642","url":"https://arxiv.org/abs/2606.20642","tags":["cs.AI","cs.LG","cs.LO","math.ST"],"score":0,"title":"Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory","domain":"cs.AI","source":"arxiv","authors":["Tingzhou Wei","Zeyu Zheng","Ethan X. Fang","Junwei Lu"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-03","reactions":{}}