假设约束的多智能体自动形式化用于渐近统计理论

渐近统计理论对于人工智能辅助形式化来说是一个具有挑战性的领域：其中心结果混合了收敛陈述、渐近展开、函数分析和正则性条件，与Lean 4 形式化中的现有基础设施存在很大差距。为了应对这些挑战，我们提出了一个由多个代理构建的受假设约束的Lean 4 形式化管道：一个协调七个专业角色的经理，用于证明规划、骨架脚手架、Mathlib 侦察、证明构建、集成、独立审查和审计。主要的方法论规则是由 Auditor 代理实施的假设纪律审计：每个主定理假设和概念层字段都必须锚定在源数学散文中，证明为Lean编码适配器，标记为源暗示，或拒绝为不受支持的强化。使用此工作流程，我们构建了渐近统计理论的系统形式化，特别是参数和半参数模型的渐近分布和效率结果。由此产生的Lean开发是公理干净和源忠实的，对核心参数和半参数定理进行了Lean检查和人工审核的证明，以便将与定理无关的基础设施和统计概念定义与特定定理的组装分开。形式化结果可在 https://github.com/junwei-lu/Lean-Asymptotic-Statistical-Theory 获取。