人工智能在数学领域取得重大突破——Anthropic公司研发的Claude系统成功完成费马大定理首个端到端形式化证明，这项耗时11天的工程创造了计算机辅助数学研究的新纪录。整个证明过程生成约1300万行Lean代码，产出30300个可验证定理，其中29500个中间结论被纳入最终证明，代码规模达到Lean核心数学库Mathlib的五倍以上。
与传统数学证明不同，形式化证明要求将人类可读的数学推导转化为计算机可逐行验证的严格逻辑程序。Anthropic团队采用多智能体协作架构，部署数十个Claude智能体并行工作，通过自主开发的Prove2Me协作平台将证明任务分解为有向无环图结构。不同智能体分别承担概念定义、引理证明和结果整合等任务，系统自动记录每个定理的自然语言说明并支持结论复用，有效解决了多智能体协作时的进度同步问题。
这项突破性成果源于对数学形式化长期挑战的回应。自1995年安德鲁·怀尔斯完成费马大定理证明以来，将129页的人类证明转化为计算机可验证的形式化版本始终是数学界的难题。传统数学论文中大量"显而易见"的推导步骤，在Lean等证明助手系统中需要完整展开每个逻辑链条，任何细微漏洞都会导致验证失败。2024年伦敦帝国理工学院启动的开源项目原计划耗时数年，而AI系统的介入使进度获得质的飞跃。
项目负责人彭天翼的学术背景为这项突破奠定基础。这位清华大学姚班毕业的信息学竞赛选手，在麻省理工学院取得量子计算博士学位后，转向大规模决策系统和强化学习研究。作为Cimulate.AI创始团队成员，他开发的CommerceGPT电商搜索系统已展示出工程化能力。目前兼任哥伦比亚大学商学院助理教授的彭天翼，带领团队将多智能体协作、强化学习与形式化工具研发相结合，开发出支持大规模数学证明的协作框架。
验证过程显示，Claude生成的证明严格遵循Lean的三条基础公理，经比较程序确认与Mathlib中的正式定义完全一致。虽然生成代码量庞大引发关于证明简洁性的讨论，但学术界普遍认为这标志着数学研究范式的转变。Google DeepMind专家评价称，自动化形式化将显著加速数学进展，使知识整理和结果验证等基础科研流程获得效率提升。
该成果揭示出人工智能在数学领域的角色演变。从解决特定猜想到参与知识体系构建，AI系统开始承担证明转写、逻辑校验等基础性工作。多智能体架构与形式化系统的结合，使大规模自动形式化从理论设想转变为可工程化落地的科研基础设施，为复杂数学理论的计算机验证开辟了新路径。
