{"id":"arxiv/2608.10894","url":"https://arxiv.org/abs/2608.10894","tags":["cs.LO","math.GR"],"score":0,"title":"FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups","domain":"cs.LO","source":"arxiv","authors":["Tianjiao Nie","Ao Zhang","Yusen Tang","Damiano Testa","Shing-Tung Yau","Peng Li","Yuan Zhou"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-11","reactions":{}}