TY  - RPRT
TI  - FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups
AU  - Tianjiao Nie
AU  - Ao Zhang
AU  - Yusen Tang
AU  - Damiano Testa
AU  - Shing-Tung Yau
AU  - Peng Li
AU  - Yuan Zhou
PY  - 2026
UR  - https://arxiv.org/abs/2608.10894
ID  - 2608.10894
ER  -