专题：2025世界人工智能大会
世界人工智能大会
2025 年 7 月 26 日，上海世博展览馆迎来一场聚焦 “人工智能的数学边界与基础重构” 的高端论坛。作为世界人工智能大会（WAIC）的重要组成部分，这场由上海市普陀区人民政府与菲数中国主办、上海市人工智能行业协会和上海东浩兰生威客引力信息科技有限公司联合承办的盛会，正成为全球关注的焦点。当 AI 技术与数学研究进入深度交织的新阶段，WAIC 2025 的召开恰如一场及时雨，为二者的协同发展搭建了关键对话平台。
AI与数学为何成为全球智识焦点？
近年来，人工智能与数学的双向需求日益迫切，推动着这场论坛的诞生。一方面，当大模型参数突破万亿，传统基于经验的调参方法陷入瓶颈，模型的泛化能力、安全性、能耗控制等核心问题，亟待数学理论的系统性支撑 —— 大模型优化依赖凸优化与非凸优化理论，Transformer 架构的注意力机制根植于概率统计与信息论，机器学习安全涉及博弈论与密码学，多模态融合则需要拓扑学与流形学习的支撑。另一方面，AI 对数学的反哺效应愈发显著，DeepMind 的 AlphaGeometry 在证明欧几里得平面几何定理方面超越 IMO 参赛者平均水平，其核心正是将几何问题转化为 AI 擅长的符号推理任务，这种 “AI for Math” 的模式正在改写数学研究范式。
在此背景下， WAIC 2025的 “人工智能的数学边界与基础重构论坛” 亮点纷呈，全方位展现了 AI 与数学交叉领域的前沿动态与深度碰撞：
（一）来自菲尔兹奖得主的关注
两位菲尔兹奖得主的深度参与成为论坛最大亮点。普林斯顿大学的 Charles Fefferman 通过视频致辞，带领观众回溯数学与计算的发展历程，从早期机械验证到如今 AI 赋能的协同演进，为全球研究者指明攻坚方向。而著名数学家、菲尔兹奖首位华人得主丘成桐教授为论坛特别选题命题，题目由其团队联合欧洲、日本数学家精心遴选，聚焦几何与代数的交叉难题，直接考验 AI 的深层推理能力，由机器模型现场作答，屏幕实时展示 AI 推理过程。这种 “人类出题 — 机器作答” 的模式，既是对 AI 能力的检验，也是人机协同的一次生动演示，旨在通过顶尖数学家的 “问题嗅觉”，引导 AI 聚焦真正具有突破性的核心难点，避免技术算力的无效消耗。
（二）大模型现场解答数学题
丘成桐教授的命题引发 “人机对抗” 看点。上海人工智能实验室、商汤科技、阶跃星辰、MiniMax 四家机构的基础大模型现场解题，左侧屏幕实时展示 AI 推理过程。其中，上海人工智能实验室的 Intern-IMO 系统成功破解 2025 年国际数学奥林匹克竞赛首题，通过自然语言推理完成几何构型分析与归纳证明，获 IMO 官方打分员认可；阶跃星辰模型则在不等式证明中展现 “工具调用” 能力，当自身代数计算出错时，主动借助外部工具验证并修正思路，最终完成形式化验证；商汤 “日日新” 大模型更通过图文混合输入，分别以坐标计算与辅助线构造两种方法求解平面几何题，展现多路径推理能力。
（三）数学家与大模型的思维激荡
圆桌论坛上，数学家与大模型团队展开深度交锋。西班牙国家研究委员会研究员郑凡与上海人工智能实验室专家合作，展示 AI 对复杂几何题的分步拆解，模型通过分类讨论排除不可能情况，最终锁定阳光线数量规律；复旦大学印佳教授与商汤团队则呈现 AI 对学生错误解答的批改过程，模型不仅指出角度计算失误，还追溯逻辑漏洞源头。上海科技大学蔡明亮教授点评称，大模型在概率递推问题中展现的逻辑链完整性令人惊讶，但在需要 “反直觉” 构造的场景仍显不足，而这正是人类数学家的核心价值所在。
（四）数学与 AI 的握手：国际高校结对
论坛现场举行中外学生 “结对” 仪式，10 位来自牛津大学、剑桥大学、多伦多大学、慕尼黑工业大学等国际高校，与上海交大、复旦大学、同济大学等沿沪宁高校的数学与 AI 专业学生携手，象征数学与 AI 的跨域融合。中国科学院院士徐宗本、普陀区委副书记周艳等见证这一时刻。结对后，学生将围绕 “AI 辅助形式化证明”“ 数论问题的机器学习探索 ”等课题开展联合研究，形成“ 本土培育 + 国际交流 ” 的人才培养闭环，为全球数学智能领域储备青年力量。
（五）顶尖学者的主旨演讲
中国科学院院士徐宗本在《AI：无限维问题 vs 有限维技术》演讲中，直指 AI 架构设计的核心矛盾 —— 智能问题本质是无限维的，而技术实现却受限于有限参数，提出通过算子簇公共不动点理论设计深度架构，并以实验证明大模型存在 “冗余阈值”，为模型优化提供数学依据。徐院士提到，智能就是指有限的知识走向无限的知识所呈现的性质。无限维问题是本质，有限维技术是现实，设计它的架构一定要从无穷维出发，通过修正算子的性质才能构成一个可用的架构。欧洲科学院院士 Torsten Hoefler 则聚焦算力与推理进化，分析大语言模型从 “下一词预测” 到 “思维树推理” 的跃迁，提出通过量化压缩与稀疏激活提升效率，其团队研发的网络拓扑策略使 AI 算力利用率提升 10-15 倍。
（六）两大国际数学实验室首发
Hitchin–Ngo 实验室（聚焦代数几何与数学物理）与 Fefferman 实验室（深耕流体力学与纳维 - 斯托克斯方程）在沪揭牌，标志着国际顶尖数学研究力量落地上海。Hitchin–Ngo 实验室将攻关镜像对称等前沿问题，探索几何与物理的深层联系；Fefferman 实验室则致力于用 AI 破解流体力学奇异性难题，助力天气预报与湍流模拟。西班牙数学科学委员会代表与普陀区区长共同为实验室启动，未来将采用 “双基地” 模式，联动欧洲与上海的算力和数据资源。
（七）全球数学家的思辨对话
“数学突破是否通向 AGI 的钥匙” 双边对话中，菲尔兹数学科学研究院前院长 Kumar Murty 指出，AI 的 “幻觉” 或许是想象力的种子，而人类数学家的价值在于从反直觉中提炼真理；上海交大徐志钦教授则结合深度学习理论收缩现象，强调需建立类似 “牛顿定理” 的 AI 基础理论；法国学者 Mathieu Laurière 提出，多代理 AI 系统的社交智能进化，将是 AGI 突破的关键方向，而拓扑学等数学工具将在其中发挥核心作用。
整场论坛中，上海市委常委、副市长陈杰在致辞中明确提出：“要以数学的基础创新驱动 AI 技术迭代，赋能产业升级，面向全球征集‘AI + 数学’综合性解决方案，加快构建一流创新生态。” 普陀区委书记胡广杰也表示将 “主动服务沿沪宁产业创新带建设，推动‘AI + 数学’协同攻关，把普陀打造成为沿沪宁产业创新带的‘引力场、智汇源、孵化器和服务中心’”。这些表态勾勒出城市战略蓝图 —— 上海正通过建设数学与交叉学科研究院、算法创新研究院，推动 “AI + 数学” 从基础研究到产业应用的全链条突破。从菲尔兹奖得主的命题挑战到中外学子的携手同行，从实验室揭牌的长效布局到思维激荡的即时碰撞，这场盛会不仅展现了 AI 与数学融合的当下成果，更锚定了未来 “人机共演” 的智能图景。展望未来，随着双引擎在上海落地生根，这里有望成为全球数学智能理论的突破地、技术的策源地与产业的新高地，为智能时代贡献独特的 “上海方案”。
AI 如何重塑数学研究？从辅助工具到共创伙伴的演进
AI 对数学研究的影响并非一蹴而就，而是历经数十年演进，从早期的计算辅助逐步发展为具备协同能力的研究伙伴，每一步突破都与具体技术工具和学术实践紧密相关，深刻改变着数学研究的范式与边界。
（一）机械验证与形式化萌芽（1970s-2000s）
这一阶段的核心是将数学证明从 “纸面推理” 转化为 “机器可验证代码”，计算机开始承担起 “超级校对员” 的角色，其核心价值在于通过严格的形式化逻辑消除人类证明中可能存在的模糊性与疏漏。
1976 年，Appel 与 Haken 对四色定理的证明堪称里程碑 —— 这个困扰数学界百年的难题，要求证明 “任何平面地图只需四种颜色即可区分相邻区域”，其关键在于验证 1834 个 “可约构形” 的逻辑自洽性。由于人工计算难以完成如此庞大的工作量（仅单个构形的验证就需数页推导），研究者首次引入计算机进行批量验证：他们将每个构形转化为可计算的逻辑命题，机器则逐一检验其 “可约性” 与 “不可避免性”。但此时的机器仅能执行预设的计算步骤，核心的构形选择仍完全依赖人类直觉，Haken 的女儿 Dorothea Blostein 甚至需要手工核对数百页微缩胶片的计算结果，期间还发现了多处可修复的错误。这一突破引发学界激烈争议：哈佛大学数学家 Mackenzie 批评 “这更像工程验收而非数学证明”，而支持者则认为它开辟了新路径。
2005 年，Gonthier 使用 Coq 证明助手完成四色定理的形式化验证，标志着形式化方法的成熟。形式化的核心是将每一个数学概念（如 “自然数”“ 平方 ”“等式”）都转化为严格的逻辑定义，每一步推理都必须符合预设的规则。这种近乎苛刻的严谨性，让数学证明首次摆脱了 “人类直觉可能出错” 的隐患。正如研究指出的，形式化证明 “为争议性成果提供了极高的正确性保障，尤其适合那些因过于冗长而难以找到评审的复杂证明”。
这一时期的另一标志性项目是 “Flyspeck 计划”。1998 年，Hales 通过复杂计算证明了开普勒猜想（三维空间中最密的球体堆积方式为面心立方堆积，堆积密度约为 74%），但由于证明过程涉及数百万个几何构型的分析与优化，传统人工评审难以完全验证其正确性 —— 评审团在经过数年审查后仅能表示 “99% 确定证明正确”。为此，Hales 于 2003 年启动形式化验证项目，原计划需 20 年，最终在 21 位研究者协作下用 11 年完成。过程中，计算机不仅确认了原证明的正确性，还纠正了几处微小疏漏（如一个几何不等式的边界条件设定偏差）。Hales 感慨：“这就像用显微镜检查艺术品，虽繁琐却能发现肉眼遗漏的细节。” 这种 “人类提出框架 + 机器验证细节” 的模式，为后续更复杂的定理证明提供了可复用的范本。
（二）算法驱动的逻辑推理（2010-2020）
随着算法理论与算力的提升，机器开始处理超大规模逻辑推理，SAT（布尔可满足性问题）与 SMT（可满足性模理论）求解器成为核心工具，其能力远超人类手动计算极限，开始触及一些传统方法难以解决的数学问题。
2016 年，Marijn Heule 团队用 SAT 求解器解决 “布尔毕达哥拉斯三元组问题” 的成果登上《自然》杂志，引发学界广泛关注。团队通过计算机证明得出结论：N=7824 是满足条件的最大数，而 {1，．．．，7825} 则无法实现这样的划分。
这个证明堪称“暴力推理” 的典范：计算机耗费 4 CPU 年（单台电脑约 1460 天）运算，生成 200TB 原始数据，压缩后仍达 68GB。其创新之处在于采用 “分而治之” 的启发式策略 —— 将问题拆解为数千个子命题，用剪枝算法优先处理最可能成立的路径，最终找到满足条件的划分方式。普林斯顿大学教授 Conway 曾质疑：“人类永远读不完这样的证明，它还能算数学吗？” 但学界最终承认，这种方法拓展了数学证明的边界 —— 有些真理，或许只能通过机器才能触及。
同期，形式化证明工具的应用范围持续扩大，开始深入更抽象的数学领域。2019 年，数学家 Scholze 启动 “液体张量实验”，旨在形式化验证他与 Clausen 关于 “液体向量空间” 的重要定理。这个仅 10 页的人类证明，因涉及大量凝聚态数学的前置知识（如完美畴、固体向量空间等抽象概念），形式化过程异常复杂：研究者需要先将这些概念转化为 Lean 证明助手可理解的定义，再逐步验证定理的每一步推导。整个过程耗时 18 个月，集结了全球数学家协作完成，最终 Lean 确认了定理的正确性，同时也让这个抽象领域的逻辑框架更加清晰。参与项目的学者发现，形式化过程迫使他们重新定义每一个模糊的概念（如 “液体性” 的严格数学描述），这种 “慢思考” 反而让理论体系更坚固。
这一阶段的机器辅助证明已展现出明显的“协作性” 特征：人类负责提出核心猜想与证明框架，机器则处理规模化的逻辑验证，二者形成互补。例如在开普勒猜想的形式化中，研究者发现原证明中一个被认为 “显然成立” 的引理（关于某类多面体体积的不等式）其实需要更严格的推导，而机器的严格性恰好弥补了人类直觉的疏漏。
（三）深度学习与大模型时代（2020 至今）
2020 年以来，深度学习与大语言模型的发展使 AI 从 “验证工具” 升级为 “发现助手”，开始主动参与数学规律的挖掘与猜想的生成，这一转变彻底重塑了数学研究的范式，让机器从 “证明的执行者” 变为 “规律的探索者”。
在形式化证明领域，Lean 等工具与 AI 的融合催生了新工作模式，人机协同的深度进一步提升。陶哲轩团队 2023 年的实践颇具代表性：他们利用 Lean 对加法组合学中的一个定理进行形式化证明，33 页的人类证明经 20 位研究者三周协作完成转化。过程中，机器不仅发现原证明中一处引理的冗余性（该引理看似必要，实则可由其他条件推导得出），还通过对证明结构的分析，提炼出更通用的证明框架，可适用于更广泛的组合问题。陶哲轩在分享中提到，使用 Lean 初期让他的工作效率暂时下降了 25 倍（这一比例被称为 “de Bruijn 因子”），但这种 “被迫放慢的思考” 反而带来新洞察 —— 形式化迫使研究者拆解每一个模糊的步骤，重新审视证明的逻辑链条。他还观察到，随着 AI 辅助工具的完善（如自动引理推荐、证明路径预测），de Bruijn 因子正快速下降，未来有望降至 1 以下，这将彻底改变数学研究的效率。
AI 在规律发现与猜想生成上的能力也日益凸显，开始在数据中挖掘人类难以察觉的数学关联。Davies 团队在纽结理论中的研究堪称典范：纽结的 “signature 值”（一个刻画拓扑性质的整数）与双曲不变量（描述纽结补空间几何特征的参数，如双曲体积、陈省身不变量等）看似毫无关联，而他们用神经网络分析近 200 万个纽结数据后发现，仅三个参数（纵向平移、meridional 平移的实部与虚部）就决定了 signature 值的变化。通过显著性分析（一种衡量输入特征对输出影响的方法），研究者排除了其他 21 个无关参数，最终引导数学家证明：signature 值与这三个参数存在明确的解析关系（可表示为某个二次型）。这种 “机器发现规律 — 人类证明规律” 的模式，已在微分几何、表示论等领域广泛应用，其核心价值在于突破人类直觉的局限 —— 机器能从海量数据中识别出被噪声掩盖的深层关联。
大语言模型的加入进一步拓展了 AI 在数学研究中的应用场景，开始模拟人类的逐步推理过程。GPT-4 等模型在美国数学邀请赛（AIME）中的表现接近优秀高中生水平，能独立解决部分国际数学奥林匹克（IMO）试题。但同时，这些模型也暴露出 “幻觉” 缺陷 —— 例如在计算 “7×4+8×8” 时，曾先给出错误答案 120，随后又用正确步骤推导出 92，这种矛盾源于其 “模式匹配” 而非 “逻辑演绎” 的工作机制：模型更擅长模仿人类推理的表面形式，却难以掌握数学的深层逻辑。
不过，针对这些缺陷的改进方法正在涌现。2024 年，DeepMind 提出的 FunSearch 框架让大语言模型生成 Python 程序解决组合问题，在 Cap set 问题上超越人类构造的最好结果。其核心是 “生成 — 验证” 循环：LLM 提出候选程序，外部数学工具检验其正确性，优质结果反馈给模型优化下次生成，这种闭环有效抑制了 “幻觉”。同期，AlphaGeometry 结合符号推理与神经网络，在 IMO 试题中超越人类平均水平，其对 2004 年第 4 题的证明引入虚数坐标系，将几何问题转化为代数运算，这种跨界思路连资深几何学家都感到惊讶。
此外，AI 在构造数学对象上展现出独特优势。Wagner 用强化学习构造出极值图论的复杂反例，其结构复杂度远超人类手动构造水平；Fawzi 团队通过强化学习发现更快的矩阵乘法算法，打破了 decades-old 的纪录；AlphaEvolve 不仅解开 300 年悬而未决的 “接吻数问题”（三维空间中最多有 12 个等径球同时与一个中心球相切），还在 14 个数学任务上实现技术突破。这些案例印证了 AI 在 “构造性问题” 上的潜力 —— 通过海量试错与策略优化，机器能找到人类难以想到的特殊结构。
值得注意的是，当前 AI 的创新仍有明显局限。剑桥大学数学家 Kevin Buzzard 指出：“AI 能生成漂亮的证明步骤，却提不出 ‘ 朗兰兹纲领 ’ 这样的宏大理论。” 机器的突破多源于对海量数据的统计归纳，而人类数学家能从看似无关的领域中提炼出统一框架（如朗兰兹纲领将数论、代数几何与表示论联系起来），这种 “从 0 到 1” 的原创性，仍是 AI 尚未跨越的鸿沟。
上海：AI 与数学融合的天然沃土与实践路径
上海作为中国人工智能发展的高地与数学研究的重镇，在推动 AI 与数学融合发展上具备独特优势，正通过系统化布局打造全球标杆。
（一）立足城市基因：融合发展的先天优势
上海的科创基因与学术积淀为 AI 与数学交叉研究提供了沃土。在 AI 领域，上海拥有全国领先的算力基础设施 —— 华为 384 超节点真机等尖端设备性能领先全球，为大规模数学建模与 AI 训练提供强大支撑；张江人工智能岛聚集了数百家中外 AI 企业，形成从算法研发到产业应用的完整生态。在数学领域，复旦大学、上海交通大学等高校的数学学科长期位居全国前列，拥有多个国家重点实验室，在微分几何、组合数学等方向的研究实力雄厚，这种 “AI 产业集群 + 顶尖数学学科” 的双重优势，使上海成为探索二者融合的理想试验田。
更关键的是，上海作为国际大都市，具备吸引全球顶尖人才的独特魅力。菲尔兹奖得主丘成桐在沪设立的研究中心已聚集一批青年数学才俊，而 WAIC 的常年举办更让上海成为全球 AI 专家的 “会客厅”。这种人才集聚效应，为突破 AI 与数学融合的前沿难题提供了智力支撑。
（二）聚焦前沿方向：锚定数学与 AI 交叉的核心领域
上海正围绕数学与 AI 融合的三大前沿方向布局：
（三）构建支撑体系：从人才到生态的全链条保障
上海正逐步通过四大举措完善融合发展生态：
通过这些举措，上海正将 WAIC 的思想碰撞转化为持久动能，努力成为全球 AI 与数学融合研究的 “策源地” 与 “示范窗”。这座城市的实践表明，当顶尖数学思维遇上领先 AI 技术，不仅能推动基础理论突破，更能为产业升级注入深层动力 —— 这正是上海对智能时代的独特贡献。