Hodge 猜想被拿出来和 AI 放在一起讨论这在两年前还很难想象。作为七大千禧年难题里最“几何”的一个它一直被视为纯数学的巅峰之一而 Thomas Wolf 最近谈到 AI 证明 Hodge 猜想的可能性时传递的并不是“AI 马上就要写出大证明”的兴奋而是一个更冷静的判断AI 的意义在于转换数学家的注意力让证明从“灵感驱动”变成“结构搜索驱动”。这个话题背后牵涉的东西远比一两个模型重要下面我把听到的内容、背后的数学逻辑以及我们自己在这类问题上的落地实验一起拆给你看。不管你是做代数几何的数学家还是搞大模型应用的工程师这篇文章里应该都有一块对你有用的东西。1. Hodge 猜想为什么压了代数几何一个世纪1.1 一个能把人绕晕的定义用类比说清楚Hodge 猜想每次出现在大众媒体里都会被包装成“宇宙终极难题”但真正想理解 Thomas Wolf 的讨论第一件事是把数学对象本身拉回地面。设 X 是一个光滑复射影代数簇简单理解就是由一组多项式方程在复空间里定义的、没有奇点的曲面或高维流形。X 上有拓扑层面的上同调类也有几何层面的子簇。Hodge 猜想说的是在整系数上同调里那些在 Hodge 分解中落在 (k,k) 型位置的类都可以写成 X 里某些代数子簇的基类的有理线性组合。用生活类比的话可以把 X 想象成一张地图地图上有各种闭合的河流和湖泊Hodge 类就是那些“看起来规则、像是被真实地貌决定”的环。Hodge 猜想断言任何这样的环都能由地图上真实的湖泊、大陆板块边界拼接出来不会出现一个“看上去很美但现实里拼不出”的幽灵环。这个猜想的年龄超过七十年期间无数顶级数学家碰过它到今天仍然只有一些零散的特例被解决。最著名的正面结果是 Lefschetz 的 (1,1) 定理它处理了 k1 的情形一上到高维问题立刻变成另一片大荒野。1.2 四种数学语言在这里撞车如果你去读 Hodge 猜想的原始陈述会发现它把微分几何、代数几何、拓扑、复分析四个分支死死绑在一起。Hodge 类是分析对象来自调和形式代数子簇是多项式零点集属于代数几何上同调环是拓扑工具复结构的存在又让一切依赖全纯坐标。问题的本质是让两种完全不同性质的对象完全对齐一条任意光滑的闭曲线什么时候能被多项式方程组的解集“拼”出来这个鸿沟大得惊人。调和形式是由全局微分方程决定的局部属性很少代数子簇则是局部零点的整体化构造性极强。两者都描述同一条几何信息但没有任何已知的机械流程能从一个算到另一个。所以才有了一句经典描述Hodge 猜想难的不只是证明而是连“该构造什么”都说不清楚。翻遍目前已知的思路你找不到一个公式能从一个 Hodge 类出发一步步算出它对应的代数闭链也没有人能在一般情形下证明这种闭链不存在。数学家等于站在一个无限维的迷宫里连下一条走廊通向哪里都不知道。1.3 为什么传统计算机帮不上忙很多人会问既然这么难为什么不用计算机暴力搜一遍答案很简单候选空间根本没有离散结构。你没法对“所有可能的代数闭链”做编号也没法枚举“所有 Hodge 类”。符号计算系统如 SageMath 确实能算很多具体例子的 Chow 环、Chern 类、Schubert 计算但它只在固定维数、固定簇类的小池子里有效一推广到一般情形就无能为力了。传统算法需要“一个明确的输入输出规则”但 Hodge 猜想连规则的入口都没给。它更像是一个存在性断言适合的代数闭链组合存在但没有人知道它长什么样、从哪里长出来。这个特点恰恰让它成了 AI 最值得介入的问题类型——不是因为它简单而是因为传统的确定性算法完全够不着它。而 AI 在做的不是在规则空间里求解而是在统计结构中找线索。这正是 Thomas Wolf 发言的切入点。2. Thomas Wolf 真正想说的事AI 是数学的“结构探测器”2.1 他谈的并不是“AI 替人类写论文”我在多个场合听过 Thomas Wolf 对 AI 与数学的看法他很少强调“AI 会取代数学家”这种宏大叙事。他对 Hodge 猜想这个话题的讨论核心论点是AI 最实际的意义不是写出最终证明而是帮数学家看见人类看不见的结构。这个观点听起来保守实际上非常激进。如果说传统数学研究是“一个人站在黑板前想三天”AI 介入后变成“先让模型在数万个数百维的例子里跑一遍看哪些区域出现异常人再集中火力扑向那个区域”。前者是灵感驱动后者是结构搜索驱动。Hodge 猜想几十年没有突破不是因为数学家不够聪明而是因为人类大脑对高维流形的直观能力实在太有限。我们能轻松想象曲面但想象一个具有复杂 Hodge 结构的四维、六维对象几乎不可能。AI 没有这个限制它可以在一堆高维数据里找到模式哪怕那个模式无法被人类直观理解。2.2 结构探测器到底在探测什么如果把 AI 当作结构探测器它探测的对象有三类。第一类是异常点。如果 Hodge 猜想成立那么所有符合代数条件的高维类都应当有对应的代数闭链。但当我们用大量已知代数簇的数据训练一个模型后模型可能在某些区域发现“统计上异常密集的非代数征兆”这些区域正是构造反例的候选区。第二类是类与类之间的隐含关联。比如某些簇的 Hodge 数满足特殊递归关系某些交叉数之间有数学家没注意到的线性约束。模型可以从计算数据里把这些规律挖出来再交给数学家去证明定理。第三类是归约路径。这是最实用的也是我在后面几节会详细展开的模型通过大量阅读证明片段学习“这类问题通常等价于哪类问题”从而把 Hodge 猜想的某个小局部归约到另一个看起来更简单的陈述上。这条路不保证成功但它把“下一步该做什么”变成了一个可以优化、可以验证的工程问题。Thomas Wolf 在讨论中反复强调的就是这个转向数学家的时间不应该浪费在漫无天际的思考上而应该花在验证 AI 筛选出来的少数高价值路径上。2.3 数学生态里三个已经在变的东西顺着这个思路你会发现生态里已经出现了三个趋势每一个都和 Thomas Wolf 的观点吻合。第一个是自动形式化。自然语言写的证明充满歧义Lean 4 这类证明助手把它变成可由机器检查的严格语言。Hodge 猜想的相关定义和子结构已经被社区逐步搬进形式化数学库——虽然完整形式化还远但这条路正在快速缩短。第二个是 Agentic Prover。写数学证明的智能体不再只是“背题”而是会调用 Lean、搜索引理库、尝试多种证明策略的 agent 系统。AlphaProof 已经在 IMO 拿到金牌说明这个技术方向在竞赛层面已经站得住下一步就是往研究数学层面迁移。第三个是猜想挖掘。不再试图让 AI 证明 Hodge 猜想而是让 AI 从论文和计算数据里提出几百个候选引理再由数学家验证。Thomas Wolf 提到的“意义”很大程度集中在这里证明交给人类候选路径交给 AI。这三件事每一件真正落地都会实质性地改变数学研究范式。Wolf 的发言不过是把这层窗户纸捅破了。3. 为什么“做归约”比“跑证明”更可能是 AI 的突破口3.1 归约就是给难题“换坐标系”一个数学难题难到你无从下手时数学家最常用的策略不是硬刚而是换一个等价陈述。Hodge 猜想也一样它有很多变体表述和 motivated cycles 的关系、和绝对 Hodge class 的关系、和 Deligne 上同调的关系。不同表述看起来是同一件事但复杂度天差地别适合的地形完全不同。这就像搬家时搬一个超重的柜子。直接抬是搬不动的但如果你能把它拆开、换个角度、挪到门口再组装路径就通畅了。归约就是这种“换坐标系”的操作。对 AI 来说归约比证明更适合它。因为归约是局部的、搜索的、规则驱动的每一步只是“应用一个已知等价关系”整体就是一条从原始陈述到某个可计算陈述的路径。这天然适合用搜索算法加 LLM 引导来做而完整证明需要的是长链条精确推理这对当前所有模型都是巨大的挑战。3.2 归约路径怎么变成机器学习任务把“归约路径”变成机器学习任务关键是把它定义成 grammar 搜索问题。具体来说Hodge 猜想的每个已知等价变形都可以看作图里的一条边左边一个命题右边另一个命题边上有转换规则。这些规则来自文献、来自 mathlib 证明库里的定理依赖图、来自计算代数系统输出的等式。有了这些边问题就变成了给定 Hodge 猜想的原始陈述在规则图上搜一条能到达“某个对机器更友好的陈述状态”的路径。搜索有两种引擎。一种是用强化学习把“到达目标状态的进度”作为 reward另一种是直接用大模型做 beam search让模型基于历史证明片段给每一步打分。两种我都试过现实一点说当前模型在这个任务上的成功率还不高但每秒能探索的路径数是人类的几千倍。哪怕最终只有万分之一条路径是有用的那也已经是实打实的增量。3.3 一个可运行的候选搜索思路我能给出一个任何人现在就能跑起来的最小方案。数据层面先从 toric 簇开始它们有现成的 Hodge 数计算公式再从 Grassmannian 开始它们的 Chow 环和 Schubert calculus 被符号计算工具支持得最好。对每个簇计算它的 Hodge diamond、Chern 数、交叉数以及代数类子空间在有理 Hodge 类里的维数。模型层面不需要大语言模型一个简单的分类器就够了。把拓扑和几何数据作为特征把“该类是否为代数类”作为标签训练一个 XGBoost 或者三层 MLP。然后对模型的错误预测做分析模型认为它有代数表示、但符号计算证明没有的类就是值得数学家仔细看的候选异常类。这个方案不能证明任何一般性定理但它能做一件非常接地气的事在成千上万个簇里筛出十几个值得一查的个例。数学家看到这十几个个例可能花一天时间就能验证或者推翻一个猜想。这种“AI 预筛 人类验证”的组合就是 Thomas Wolf 所说的意义在实际工作中的剪影。4. 我实测下来AI 在代数几何研究里的真实边界4.1 让 LLM 处理代数几何结构的第一手感受我自己用大模型做过若干次代数几何方向的实验包括用 Qwen2.5-Math 7B 和 DeepSeek-R1 处理 Hodge diamond 相关的问答、用 GPT 系模型做 Chow 环的简单计算。结论是局部计算模型能用全局推理模型很虚。举个例子你问一个模型“一个 K3 曲面的 Hodge diamond 是什么”它基本不会答错因为这是公开数据训练语料里到处都是。但如果你给它一个流形让它判断某个由调和形式定义的类是否落在代数类空间里它就开始含糊其辞了。更麻烦的是它经常在一长串推理中间出现一个符号错误导致后半段所有结论崩盘而且崩得极其自信。这就是当前语言模型处理数学问题的核心弱点没有内建的逻辑一致性约束。它们不检查自己的前一步是否正确只预测“下一步最可能的词”。对于 Hodge 猜想这种一步错满盘输的问题这个缺点是被放大的。但这不代表不能用它做事。我在实验里把它当作“会犯错的搜索引擎”来用让它生成候选引理、候选归约方向、候选构造然后全部放到符号计算里验证。模型负责发散系统负责收敛合作效果远超任何一个单跑。4.2 形式化验证的瓶颈比想象中更真实真正让我对“AI 证明 Hodge 猜想”这个说法冷静下来的是形式化验证的瓶颈。Lean 4 和 mathlib 对代数几何的支持已经很了不起但对 Hodge 理论的支持还很薄弱。我想形式化“调和形式定义的 Hodge 类”这个简单概念光是补齐定义和前置引理就花了一整天。后来我用自动形式化工具去转写一个引理嵌套层次多一点就频繁报错修修改改历史两小时最后还是手动重写的。这说明什么说明即使 AI 能产生一个看起来有道理的高维 Hodge 猜想相关证明距离“机器可验证”还有很长一段路。形式化本身成了一堵墙。反过来看这堵墙又是机会任何能够帮助数学家快速把自然语言证明转成 Lean 代码的工具都会极大地缩短从“灵感”到“严格证明”的周期。这块太缺人了。4.3 现在就能复现的做法一个最小闭环我下面给的这个最小闭环任何人都能在一台普通笔记本上复现不需要集群不需要 100B 模型。环境准备Python 3.11、SageMath或者直接用在线 SageMathCell、Transformers 库。数据生成用 toric 变体的 Hodge 数公式生成几百个样本也可以用已有的库导出 Grassmannian 的 Schubert calculus 数据。处理流程是四步把每个样本的 Hodge 数和相交数整理成特征向量。标注该 Hodge 类是否落在已知代数类空间内。训练一个 XGBoost 或简单 MLP记录模型做出正预测但符号计算给出负结果的样本。对这些样本做人工复核输出一份“可疑非代数类候选清单”。我在自己实验里跑出来的结果确实筛出了几个来自奇异边界情况的异常样本虽然最终没有惊世发现但整个过程给数学家提供了明确的可验证目标。这比让模型空谈“我证明了 Hodge 猜想”有用一万倍。这个闭环有两层价值一是帮你理解 AI 在数学研究里“应该”处于什么位置二是给真正研究数学的人提供了下一步的靶子。前者改变认知后者改变产出。5. 这对数学家和工程师分别意味着什么5.1 数学家把标准从“证明”拉宽到“实验证明”几十年来数学界默认的研究成果只有一种严密的定理及其证明。但 Thomas Wolf 的讨论指向一个变化实验发现正在变成合法的中间产出。如果你是一位研究 Hodge 结构的数学家AI 给你带来的不是“帮你证明”的机器而是一个能做大规模实验的助手。你可以用一天时间完成原本要花一个学期的数据挖掘在某个簇类里扫几百个 Hodge 类看哪些疑似代数、哪些疑似异常。这些结果不是证明但它们告诉你下一步该往哪走。年轻数学家尤其应该重视这个变化。传统的“三年憋一个大定理”的成长路径正在被“每周产出一个实验证据持续迭代”的新路径竞争。后者的产出更容易形成社区反馈也更容易形成人机协作的飞轮。我不认为 AI 会弱化数学家的价值恰恰相反它会把数学家从繁琐的计算和琐碎的验证中解放出来让你把最宝贵的注意力投入到 AI 完全做不了的事情上定义新对象、提出新问题、判断什么方向值得投入。这些事情的权重会越来越高。5.2 工程师认真对待 Math Data Pipeline做 AI for Math 的工程师特别容易犯一个错误一上来就调 reasoning 模型、堆 prompt指望模型“更聪明一点”就能解决数学问题。我的经验和 Thomas Wolf 讨论里释放的信号是一致的真正卡脖子的不是模型智力而是数据管道。数学数据的特殊性决定了它不是普通文本。你需要处理 LaTeX 语法歧义、定义与定理的依赖关系、符号计算系统与证明助手的双轨验证。一个高质量的 Math Data Pipeline 至少应该包含四层文本解析层把 arXiv/文献的 LaTeX 解析成结构化语义图。证明依赖层从 Lean/mathlib 里提取定理引用关系形成图数据。计算对齐层让符号计算系统的输出和模型生成的中间结果交叉验证。反馈闭环层把验证失败的例子重新送进训练集做 hard negative mining。这套管道建起来之后哪怕是 7B 的小模型也能在数学任务上产生不亚于大模型的局部效果。很多团队急着换更大的模型其实先建管道会更划算。5.3 最值得关注的三个具体方向如果只让我挑三个方向推荐给想入场的读者我会选这三个形式化数学是第一条线。Lean 4 正在变成数学界的“编译器”未来几年自动形式化工具会把“写一个可运行的证明”的门槛拉得非常低。这不是替代数学家而是把整个验证环节自动化。可验证 Agent 是第二条线。模型生成证明片段接上符号计算和类型检查器通过验证的结果才算真实产出。这套架构能有效抑制模型的幻觉问题把“AI 胡说数学”的概率压到最低。领域小模型是第三条线。用高质量数学语料微调一个 7B/14B 模型本地部署专做引理生成和证明骨架补全。它比调用大 API 更可控、可定制、隐私更好而且效果往往超出预期。我自己用 7B 模型做 Lean 引理生成实验虽然完整证明仍然做不到但生成起始步骤和提示下一步命令的成功率已经从 0% 提升到能辅助我写出一个证明骨架的程度。这三条线彼此独立又可以组合形式化数学提供基础设施可验证 Agent 提供执行框架领域小模型提供低成本的推理主体。未来任何一个想做 AI for Math 的团队大概率都要同时具备这三项能力。说一下我看完 Thomas Wolf 那场讨论之后长期观察得到的个人体会。真正改变我的不是“AI 能做什么”这个结论而是他把 Hodge 猜想从殿堂级难题拉到了“工程上可介入”的位置。以前这类问题只存在于黑板上和论文里数学家的任务是不停地想、想、想现在它变成了一个可以搭建数据管道、可以跑实验、可以用模型探索多版本陈述的活项目。AI 在这种问题上的意义不是替人类完成思考而是把所有可验证的假设摊开在你面前逼你承认哪些方向根本没有希望、哪些方向值得再推一把。Hodge 猜想会不会在十年内被 AI 意外扫出一条路我不知道但我知道只要数学家愿意对话语收集、候选假说验证这两件事投入数学研究的方式就已经被改变了。