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

Tingzhou Wei, Zeyu Zheng, Ethan X. Fang, Junwei Lu

arXivarxiv/2606.20642Jun 3, 2026cs.AIscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2606.20642
curl -X POST /api/v1/records/arxiv/2606.20642/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.20642/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'