围绕现代数学中体量最大的证明工程之一“有限单群分类”，FormaTheoria 团队提出一套 AI 辅助工作流，从原始文献梳理依赖、构建形式化证明，再交由 Lean 核验。截至 2026 年 8 月，项目已完成 4 个关键定理的形式化，累计产出超过 99.4 万行代码、850 多个文件，并构建出包含 30298 个数学声明的证明网络。论文还记录了系统在文献中发现的多类定义冲突、条件遗漏和排版错误。

OpenAI启动秘密项目“水星”，以时薪150美元招募超100名前高盛、摩根士丹利等投行精英，训练AI构建财务模型，旨在替代华尔街分析师繁重的Excel建模工作，加速AI金融应用商业化。