AI 行业资讯 - FormaTheoria

AI辅助数学验证新进展：FormaTheoria完成四个关键定理Lean形式化

由清华大学求真书院领军班学生与丘成桐数学科学中心、智能产业研究院及华威大学团队联合推进的FormaTheoria项目，截至2026年8月已成功将四条核心定理转化为Lean证明语言，构建起超过99.4万行环环相扣的代码化数学体系，为有限单群分类这一宏大证明工程的机器验证写下关键里程碑。对研究者而言，这意味着未来可借助交互式定理证明工具逐步拆解复杂数学结构，降低人工推导的疏漏风险。