AI 中文总结
本研究提出AI辅助工作流FormaTheoria，应用于有限单群分类定理的形式化，构建了经机器检查的Lean开发项目，验证了深度依赖的有限群理论，为推进该定理的形式化奠定基础。
AI 中文摘要
高级数学的大规模形式化不仅需要翻译单个陈述，还必须重构分布在异构来源中的连贯理论。这一过程带来四项挑战：发现隐式依赖、修正源缺陷、保持语义保真度、协调跨源不一致。我们提出FormaTheoria，这是一种端到端的AI辅助工作流，可协调源获取、形式化、证明构造、递归依赖发现、独立审核与协调，同时保留来源并保护已核准声明。共享智能体框架通过工具使用、上下文压缩、审核门控终止、章节级源上下文及依赖感知的批量并行化，支持长时程执行。将FormaTheoria应用于有限单群分类定理（CFSG）的主要组件，我们构建了经机器检查的Lean开发项目，其涵盖本德尔-铃木定理，包含费特-汤普森奇阶定理、格劳伯曼Z*定理与布劳尔-铃木定理。该开发验证了大量深度依赖的有限群理论，为推进CFSG形式化提供基础。对代码与记录的构建过程的实证分析，支持所识别挑战的实际相关性，并阐明对应工作流组件的作用。这些结果共同证明，AI辅助工作流可通过结合语言模型智能体、形式验证、结构化审核与显式依赖管理，从分布式文献中重构具有数学意义的形式理论。
英文摘要
Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sources. This process raises four challenges: discovering implicit dependencies, correcting source defects, preserving semantic fidelity, and reconciling cross-source misalignments. We present FormaTheoria, an end-to-end, AI-assisted workflow that coordinates source acquisition, formalization, proof construction, recursive dependency discovery, independent review, and reconciliation, while preserving provenance and protecting approved declarations. A shared agent framework supports long-horizon execution through tool use, context compaction, review-gated termination, section-level source context, and dependency-aware batch parallelization. Applying FormaTheoria to major components of the Classification of Finite Simple Groups (CFSG), we construct a machine-checked Lean development extending through the Bender--Suzuki theorem and encompassing the Feit--Thompson Odd Order Theorem, Glauberman's $Z^*$ theorem, and the Brauer--Suzuki theorem. This development verifies an extensive body of deeply interdependent finite-group theory while providing a foundation for continuing the CFSG formalization. An empirical analysis of the code and recorded construction process supports the practical relevance of the identified challenges and illustrates the roles of the corresponding workflow components. Together, these results demonstrate how AI-assisted workflows can reconstruct mathematically significant formal theories from distributed literature by combining language-model agents with formal verification, structured review, and explicit dependency management.
