Erdős厄多什难题一直是数学界的一种特殊存在它由传奇数学家 Paul Erdős 在数十年间随手抛出悬赏金额不大却死死卡住了一代又一代人的思路。最近越来越多的报道开始用“Erdős Problems Are Falling to AI”这类标题暗示 AI 正在攻克这些世纪难题。如果你只把这些当新闻看很容易误判两件事一是高估 AI 的推理能力二是低估形式化验证在其中的真正作用。作为一名写代码的工程师我更关心的问题是AI 到底用什么方式在啃这类硬骨头这种方式能不能复用到我自己的工作流里答案其实比“AI 又行了”要有意思得多——真正的变化不是大模型突然变聪明了而是数学研究的流程从“直觉 纸笔”变成了“猜想生成 机器验证”。这篇文章会用通俗的方式拆解这个变化并给出一个你可以直接上手实践的“AI 数学工作台”搭建方案用 LLM 生成猜想、用 Python 暴力搜索找反例、用 Lean 完成形式化证明。读完这篇文章你会对两个问题有清晰的判断第一AI 在数学上到底突破了什么、还没突破什么第二作为一个开发者现在就可以用哪些工具参与这场变革。1. 这篇文章真正要解决的问题先说痛点。很多开发者看到“AI 攻克数学难题”的新闻时第一反应是“这跟我有什么关系”。但实际上AI 做数学和 AI 写代码面对的是同一个核心问题机器生成的结论不可信。LLM 可以非常流利地写出一段看似严谨的证明但它在数学上和写代码时一样会“幻觉”——编造不存在的引理跳过关键步骤甚至给出完全错误但语气自信的答案。Erdős 难题之所以成为 AI 数学能力的试金石恰恰因为它把“不可信”这个问题放到了显微镜下。一道题有没有被解决答案是唯一的要么有完整证明要么没有。没有“差不多对了”没有“看起来像能跑”。因此AI 要真正攻破这类难题就必须解决验证问题。这篇文章要讲清楚三件事Erdős 难题是什么为什么它天然适合 AI 介入。AI 做数学的两条路线自然语言证明生成与形式化证明它们各自解决了什么、又有什么坑。如何从零搭建一个“LLM 生成猜想 Python 暴力验证 Lean 形式化证明”的最小工作台并实际跑通三个示例。如果你是刚接触 AI 应用开发的工程师这篇文章比看 10 篇“AI 颠覆数学”的新闻更有用——因为你会看到一条完整的技术链路而不是一个被夸大的结论。2. Erdős 难题是什么数学家留下的“悬赏题库”先补充背景。Paul Erdős 是 20 世纪最传奇的数学家之一一生发表了超过 1500 篇论文合作者超过 500 人以至于学术界专门发明了一个概念叫“Erdős 数”——你和 Erdős 之间的合作距离。他常年背着一个行李箱奔波于世界各地住在同行家里一边写论文一边提出新问题然后给问题标上悬赏金额。这些悬赏金额通常不大从 25 美元到 1000 美元不等但含金量极高。Erdős 本人对问题的判断力非常准他提出的问题大多来自组合数学、数论、图论、概率论等离散数学领域表述简洁但难度极高。有些问题到今天已经挂了半个多世纪奖金依然无人领取。这里需要注意Erdős 难题不是铁板一块。有些已经被人类数学家解决了。比如著名的 Erdős 差异问题Erdős Discrepancy Problem2015 年由陶哲轩完成证明那是一个纯人类智慧的成果。还有一些问题始终悬而未决恰恰是这类问题现在成了 AI 系统试身手的舞台。为什么 AI 偏偏看上了 Erdős 难题有三个原因第一问题陈述足够精确。AI 系统最怕模糊的任务而 Erdős 难题往往用“是否存在”“是否对所有 n 成立”这样清晰的逻辑陈述可以直接转化为可验证的形式化目标。第二大量问题属于组合数学。这类问题的本质是在有限的离散结构里找规律、找反例、找构造非常适合算法和搜索方法发挥作用。暴力验证一个小规模情形往往能给整个问题带来关键线索。第三小规模验证与完整证明之间存在一条明确的晋升路径。AI 可以先对 n3、n4 的情形做计算验证找到模式再尝试把模式推广成一般性证明。这种“从小到大、从计算到证明”的路径恰好是现有 AI 系统相对擅长的事。所以“Erdős 难题正在被 AI 攻克”这类标题背后并不是某个单一模型的灵光一现而是一整套工具链的成熟。3. AI 做数学的两种路线直觉生成与形式化验证要理解 AI 在数学上的真实进展必须先分清两条完全不同的技术路线。第一条路线是“自然语言证明生成”。你把一道题抛给 LLM它用人类可读的自然语言写出解法。优点很明显门槛低速度快推理过程可读。但缺点也很致命缺少强制性检查。大模型生成数学证明时幻觉率远高于写普通文本。它可能错误调用一个不存在的定理可能在上一步到下一步之间偷偷改变条件甚至可能用一句“显然可得”掩盖整个推导的断裂。更麻烦的是在数学里一个看起来无懈可击的证明可能只在第 17 行有一个符号错误就导致整个结论崩塌。人类读者很难发现这种错误AI 自己也意识不到。因此纯自然语言路线在严谨数学中只能作为“启发式工具”不能作为“判定工具”。第二条路线是“形式化证明”。这不是让 AI 用自然语言写证明而是让证明变成机器可以逐条检查的形式化推导。代表工具是 Lean、Coq、Isabelle 这类证明助手Proof Assistant。在这种路线里每一处推理都必须调用明确的规则每一个中间结论都必须能被机器验证。AI 可以参与生成证明步骤但最终裁判是证明验证器——它不会因为“语气自信”而放过任何错误。两条路线的差异可以这样理解自然语言证明像 AI 给你拍胸脯保证“这件事我查过了没问题”形式化证明像 AI 把每一张单据、每一笔流水都摊开给你由独立审计员逐条核对。前者解决“快不快”的问题后者解决“对不对”的问题。一个成熟的 AI 数学系统通常是把两者结合用 LLM 提供“这个方向可能可行”的直觉判断再用证明助手和搜索算法强行完成验证。这也是为什么近两年大家的关注点逐渐从“大模型会不会做小学数学题”转向“形式化数学库建得够不够大”。4. 为什么形式化证明是 AI 攻破数学难题的关键上一节提到的证明助手 Lean 4是目前 AI-for-Math 领域最受关注的工具之一。它背后是数学社区维护的 mathlib 库——一个被形式化验证过的庞大数学知识库。这意味着 AI 在 Lean 里做证明时可以调用大量已经被证明的定理而不必从零开始。这个设计非常关键。在旧工作流里AI 生成一个证明人类得花大量时间去人工检查而在 Lean 工作流里AI 生成证明脚本Lean 负责检查每一步是否合法。如果 AI 的某个步骤引用了不存在的定理Lean 立刻报错如果两个条件不能同时成立Lean 立刻拒绝。也就是说形式化证明天然隔离了 LLM 的幻觉。近年来的一些成果也印证了这条路线。2024 年Google DeepMind 的 AlphaProof 在 IMO国际数学奥林匹克赛题上达到了银牌水平它解决的问题里既有自然语言生成也有 Lean 形式化验证的环节。更早一些的 AlphaGeometry 则结合语言模型和符号引擎在几何题上超过了人类金牌选手的平均水平。此外开源社区也出现了 DeepSeek-Prover 这类专门面向定理证明的模型目标就是生成能被 Lean 检查的证明代码。但这里必须给一个冷静的判断从“AI 能在竞赛题和部分研究级问题上辅助证明”到“AI 独立攻破一个流传几十年的 Erdős 难题”中间还有很长的距离。新闻报道里说的“falling to AI”更准确的理解是AI 系统正在越来越多地参与这些难题的子问题——验证特例、寻找反例、构造辅助引理、缩小搜索空间。这些工作过去完全依赖人类耐心现在可以由 AI 半自动完成。对工程师来说这里有一个值得注意的类比形式化验证证明的是“数学证明正确”而类型系统、静态分析验证的是“代码行为正确”。两者的底层思想完全一致——用机器可检查的规则替代人的记忆和直觉。所以学习 Lean 不只是为了玩数学它对你理解类型系统和编译原理也有直接帮助。5. 环境准备搭建你自己的 AI 数学验证工作台下面进入实操。我们从零搭建一个最小可用的“AI 数学验证工作台”包含三部分Lean 4形式化验证、Python暴力搜索、LLM API猜想生成。版本信息请以官方文档为准这里演示的是通用流程。5.1 安装 Lean 4Lean 4 官方推荐的安装方式是通过 elan 这个版本管理工具类似 Rust 的 rustup。在 macOS 或 Linux 终端执行# 安装 elan curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh国内网络环境访问 GitHub 可能不稳定如果安装失败请参考 Lean 官方社区镜像或稍后重试。安装完成后重新打开终端确认版本elan --version然后用 VS Code 安装 Lean 4 扩展它会自动识别 elan 安装的 Lean 工具链。创建项目时使用带 mathlib 的模板# 创建 Lean 4 mathlib 项目 mkdir ai-math-lab cd ai-math-lab lake new ai_math_lab math cd ai_math_lab lake update mathlib项目创建后用 VS Code 打开目录等待 mathlib 编译或下载缓存。第一次构建可能耗时较长这也正常。5.2 准备 Python 环境Python 负责计算验证和调用 LLM API。建议创建独立虚拟环境python3 -m venv .venv source .venv/bin/activate # Windows 用户执行 .venv\Scripts\activate pip install openai sympyopenai是官方 SDK用于调用兼容 OpenAI 接口的大模型服务sympy用于符号计算本文的示例里不是必需但后续做数学实验时很常用。5.3 配置 LLM API把 API Key 放到环境变量里不要写进代码或提交到仓库。这是最基本的安全习惯export LLM_API_KEY你的API Key export LLM_BASE_URLhttps://api.openai.com/v1 export LLM_MODELgpt-4o-mini不同服务商的地址和模型名不同以实际订阅的服务文档为准。6. 完整示例从猜想生成到机器验证这一节我们用同一个数学场景——K_n 完全图的 2 染色问题——走完三个环节LLM 生成猜想、Python 暴力搜索找反例、Lean 形式化证明。这个场景本身出自 Erdős 最热爱的 Ramsey 理论很适合演示。6.1 用 LLM 生成候选猜想先写一个脚本让 LLM 针对一个问题提出可验证的猜想。文件路径# hypothesis_gen.py import os from openai import OpenAI client OpenAI( api_keyos.getenv(LLM_API_KEY), base_urlos.getenv(LLM_BASE_URL, https://api.openai.com/v1), ) prompt 你是一位组合数学研究者。针对下面的问题给出一个可以用代码做小规模验证的候选猜想。 要求猜想必须能用暴力搜索在 n 较小的情况下快速检验并解释它为什么可能与原问题相关。 问题在 n 个顶点的完全图 K_n 中将每条边染成红色或蓝色。 定义单色三角形为三个顶点之间三条边颜色完全相同的三角形。 请猜想单色三角形数量的最小值随 n 如何变化给出一个可检验的下界表达式。 resp client.chat.completions.create( modelos.getenv(LLM_MODEL, gpt-4o-mini), messages[{role: user, content: prompt}], temperature0.7, ) print(resp.choices[0].message.content)这一步明确体现了 AI 的角色它负责给出“可能的答案”而不是“确定的结论”。它的输出下面必须经过验证。6.2 用 Python 暴力搜索找反例Erdős 风格的问题第一步永远是小规模计算。下面的脚本枚举 K_n 的所有 2 染色检查是否存在不含任何单色三角形的染色方案。如果存在就说明某个下界猜想在 n 这个值上被推翻了。# ramsey_check.py import itertools def has_mono_clique(vertices, edges_set, k): 判断 vertices 中是否存在 k 个顶点使得两两之间的边都在 edges_set 里。 for combo in itertools.combinations(vertices, k): if all(tuple(sorted(pair)) in edges_set for pair in itertools.combinations(combo, 2)): return True return False def check_k_n(n, k3): vertices list(range(n)) all_edges [tuple(sorted(e)) for e in itertools.combinations(vertices, 2)] for mask in range(1 len(all_edges)): red {all_edges[i] for i in range(len(all_edges)) if (mask i) 1} blue set(all_edges) - red if not has_mono_clique(vertices, red, k) and not has_mono_clique(vertices, blue, k): print(fn{n}: 找到反例存在不含单色三角形的 2 染色。) return False print(fn{n}: 验证通过任意 2 染色都存在单色三角形。) return True if __name__ __main__: check_k_n(5) # 期望找到反例 check_k_n(6) # 期望验证通过这里有个细节值得停下来看check_k_n(5)应该找到反例而check_k_n(6)应该验证通过。这正对应 Ramsey 理论中著名的结论 R(3,3)65 个顶点时可以构造一个不含单色三角形的染色6 个顶点时不可能。这个结果本身就很符合 Erdős 题目的气质——临界点清晰构造和反例同样重要。6.3 用 Lean 完成形式化证明跑通暴力搜索之后你得到的是“n6 时所有 2 染色都被穷举验证过了”但这还不是数学意义上的证明因为枚举 2^15 种染色只是检查了 K_6 这个具体情形。Erdős 难题需要的是对任意 n 成立的证明或者至少是某个关键定理的严格证明。形式化证明工具在这里发挥真正价值。把下面的代码保存为 Lean 项目中的Test.leanimport Mathlib -- 例 1自然数加法的结合律 -- 这是最基础的形式化证明练习验证 Lean 环境是否正常工作 theorem add_assoc_example (a b c : ℕ) : (a b) c a (b c) : by rw [Nat.add_assoc] -- 例 2任何整数的平方非负 -- 这种看似显然的命题Lean 依然要求你引用正确的定理或策略 theorem square_nonneg_example (n : ℤ) : 0 ≤ n ^ 2 : by exact sq_nonneg n第一个证明使用了rw [Nat.add_assoc]把左边重写为右边第二个证明直接调用数学库里的sq_nonneg定理。这两个例子很简单但足以让你感受 Lean 的工作方式目标会被逐步化简直到变成一个恒等式或一个可由已知定理直接解决的问题。看完基础例子可以尝试更有 Erdős 风格的命题。比如证明“任何整数的平方加 1 恒大于 0”-- 例 3n^2 1 ≥ 1等价于 n^2 ≥ 0 theorem square_add_one_pos (n : ℤ) : 1 ≤ n ^ 2 1 : by nlinarith [sq_nonneg n]这里nlinarith是处理非线性整数算术的策略sq_nonneg n提供了0 ≤ n^2这个关键前提。可以看到Lean 的证明思路和人类差不多先找到一个已知结论再把它整合进目标里。顺带说明把 K_6 的 Ramsey 结论完整形式化需要定义图、染色、三角形、完全图这些概念工作量比上面三个例子大很多但它正是 mathlib 社区每天都在做的那种事。真正研究级的 AI 数学系统就是在这种基础设施之上构建证明的。7. 运行结果与验证方法各环节跑完如何判断结果是否正常Python 暴力搜索的运行方式python ramsey_check.py预期输出大致是n5: 找到反例存在不含单色三角形的 2 染色。 n6: 验证通过任意 2 染色都存在单色三角形。如果n5没有找到反例或者n6反而找到反例说明代码实现有 bug优先检查all_edges的生成和has_mono_clique的边匹配逻辑。Lean 的验证方式更直观在 VS Code 中打开Test.lean如果代码没有红色波浪线Lean 扩展右下角显示正常就表示所有定理都被机器接受。命令行验证方式如下lake env lean Test.lean如果命令没有任何输出就直接结束说明文件中的所有证明都通过了。如果出现unsolved goals或错误信息就按错误提示定位到对应行。这里需要强调一个验证原则LLM 生成的内容不管输出多漂亮都必须经过 Python 代码或 Lean 验证后才算“可信”。在整个工作流中LLM 是提出者Python 是初步检查员Lean 是最终裁判。裁判说不行的东西再动听也不算数。8. 常见误区与排查思路实际跑这套流程时新手会踩到一些典型的坑整理成表格方便对照排查问题现象可能原因排查方式解决方案LLM 给出的证明看起来没问题但用 Lean 验证失败LLM 幻觉引用了不存在的定理或跳步把 LLM 输出和 Lean 报错对照定位第一个不被接受的步骤把证明拆成更小的引理逐条验证或者让 LLM 参考 mathlib 中已有的定理名称Lean 文件报unknown identifier没有正确导入对应的 Mathlib 模块查看报错信息里的标识符检查import Mathlib是否在最顶部确保文件第一行是import Mathlib如果仍不行执行lake update mathlib首次lake build非常慢mathlib 体积大需要全量编译观察 VS Code 下方的进度提示耐心等待后续再次编译会走缓存速度大幅提升暴力搜索在 n7 时运行极慢染色方案数为 2^(C(n,2))指数爆炸检查循环次数和时间复杂度用剪枝、SAT/SMT 求解器或改用随机搜索先找反例openai调用报 401API Key 或base_url配置错误检查环境变量是否在当前终端生效确认 API Key 有效不要硬编码在代码里换个已知可用的服务商误以为“小规模验证通过”等于“问题已解决”混淆计算验证与数学证明回头看问题是针对具体 n 还是所有 n只有对所有 n 成立的证明才算解决计算验证只作为启发线索从这张表可以看到大多数问题都源于工具链使用不当或对验证边界的误解而不是某个环节“不够聪明”。正确的工作流能把这些坑提前暴露。9. 对工程师的启示与最佳实践这套 AI 数学工作流本质上和 AI 辅助编程是同一套方法论。如果你平时用 LLM 辅助写代码下面几条最佳实践可以直接迁移。第一把 AI 当成“方案生成器”而不是“答案判定器”。无论是写代码还是做数学LLM 的价值在于快速给出候选方案而质量检查必须交给编译器、测试和形式化工具。不要因为模型语气笃定就跳过验证。第二所有验证过程必须可复现、可追溯。记录输入问题、模型版本、Prompt、验证命令和输出结果。数学工作尤其如此——一个无法复现的“证明”没有任何价值。写代码时同理把requirements.txt、lakefile.toml、环境变量清单都纳入版本管理。第三小步快跑先验证最小情形。不要一上来就试图证明一个大的 Erdős 难题。先从 n3、n4 这类情形开始用暴力搜索找规律把问题拆成若干个小引理再逐步证明。这个策略和软件工程里的“先跑通最小可行产品”完全一致。第四注意安全界。API Key 只通过环境变量注入不要提交到仓库Lean 项目依赖的第三方库要检查来源AI 生成的内容应用到正式场景前必须有独立验证。本文涉及的所有操作都是常规开发工具的使用但在真实项目中依然要遵循最小权限原则。第五正视工具边界。截至本文写作时间AI 在数学上的公开成果还集中在竞赛题、验证子问题和小规模定理证明层面。看到“AI 攻克某难题”的报道时先看两个东西有没有同行评审、有没有可复现的形式化证明。这两个问题能帮你过滤掉 90% 的夸张宣传。10. 总结与后续学习方向回到文章开头的问题Erdős 难题真的在被 AI 攻破吗更准确的说法是AI 正在成为数学家的新工具而真正让这个说法有分量的不是大模型的“聪明”而是形式化验证系统的成熟。Erdős 艰难题在传播中被简化为一个口号但技术工作者应该看到口号背后的工程细节LLM 负责直觉搜索算法负责探索Lean 负责审计人类负责设定方向和解释结果。如果你对这条路线感兴趣建议按下面的顺序继续深入先跑通本文三个示例确认 Lean 环境和 Python 环境都正常。学习 Lean 基础语法尝试把一些简单数学命题形式化例如“奇数的平方是奇数”“质数有无穷多个”。后者的完整证明在 mathlib 中已有高质量范本可以直接对着学习。关注 mathlib 社区和 AI-for-Math 方向的开源项目例如 DeepSeek-Prover 这类面向定理证明的模型。挑一个自己感兴趣的组合猜想的退化情形用“LLM 提猜 Python 找反例 Lean 证引理”的流程做一轮实验体会完整工作流带来的节奏感。下一次你再看到“传奇 Erdős 难题正在被 AI 攻破”的标题可以先别急着转发。打开 Lean把标题里的宣称变成一个可以证明的命题然后用机器验证它。这个过程本身就是 AI 时代工程师参与数学最脚踏实地的方式。 AI攻破Erdős难题？用LLM+Python+Lean搭建形式化验证工作台
Erdős厄多什难题一直是数学界的一种特殊存在它由传奇数学家 Paul Erdős 在数十年间随手抛出悬赏金额不大却死死卡住了一代又一代人的思路。最近越来越多的报道开始用“Erdős Problems Are Falling to AI”这类标题暗示 AI 正在攻克这些世纪难题。如果你只把这些当新闻看很容易误判两件事一是高估 AI 的推理能力二是低估形式化验证在其中的真正作用。作为一名写代码的工程师我更关心的问题是AI 到底用什么方式在啃这类硬骨头这种方式能不能复用到我自己的工作流里答案其实比“AI 又行了”要有意思得多——真正的变化不是大模型突然变聪明了而是数学研究的流程从“直觉 纸笔”变成了“猜想生成 机器验证”。这篇文章会用通俗的方式拆解这个变化并给出一个你可以直接上手实践的“AI 数学工作台”搭建方案用 LLM 生成猜想、用 Python 暴力搜索找反例、用 Lean 完成形式化证明。读完这篇文章你会对两个问题有清晰的判断第一AI 在数学上到底突破了什么、还没突破什么第二作为一个开发者现在就可以用哪些工具参与这场变革。1. 这篇文章真正要解决的问题先说痛点。很多开发者看到“AI 攻克数学难题”的新闻时第一反应是“这跟我有什么关系”。但实际上AI 做数学和 AI 写代码面对的是同一个核心问题机器生成的结论不可信。LLM 可以非常流利地写出一段看似严谨的证明但它在数学上和写代码时一样会“幻觉”——编造不存在的引理跳过关键步骤甚至给出完全错误但语气自信的答案。Erdős 难题之所以成为 AI 数学能力的试金石恰恰因为它把“不可信”这个问题放到了显微镜下。一道题有没有被解决答案是唯一的要么有完整证明要么没有。没有“差不多对了”没有“看起来像能跑”。因此AI 要真正攻破这类难题就必须解决验证问题。这篇文章要讲清楚三件事Erdős 难题是什么为什么它天然适合 AI 介入。AI 做数学的两条路线自然语言证明生成与形式化证明它们各自解决了什么、又有什么坑。如何从零搭建一个“LLM 生成猜想 Python 暴力验证 Lean 形式化证明”的最小工作台并实际跑通三个示例。如果你是刚接触 AI 应用开发的工程师这篇文章比看 10 篇“AI 颠覆数学”的新闻更有用——因为你会看到一条完整的技术链路而不是一个被夸大的结论。2. Erdős 难题是什么数学家留下的“悬赏题库”先补充背景。Paul Erdős 是 20 世纪最传奇的数学家之一一生发表了超过 1500 篇论文合作者超过 500 人以至于学术界专门发明了一个概念叫“Erdős 数”——你和 Erdős 之间的合作距离。他常年背着一个行李箱奔波于世界各地住在同行家里一边写论文一边提出新问题然后给问题标上悬赏金额。这些悬赏金额通常不大从 25 美元到 1000 美元不等但含金量极高。Erdős 本人对问题的判断力非常准他提出的问题大多来自组合数学、数论、图论、概率论等离散数学领域表述简洁但难度极高。有些问题到今天已经挂了半个多世纪奖金依然无人领取。这里需要注意Erdős 难题不是铁板一块。有些已经被人类数学家解决了。比如著名的 Erdős 差异问题Erdős Discrepancy Problem2015 年由陶哲轩完成证明那是一个纯人类智慧的成果。还有一些问题始终悬而未决恰恰是这类问题现在成了 AI 系统试身手的舞台。为什么 AI 偏偏看上了 Erdős 难题有三个原因第一问题陈述足够精确。AI 系统最怕模糊的任务而 Erdős 难题往往用“是否存在”“是否对所有 n 成立”这样清晰的逻辑陈述可以直接转化为可验证的形式化目标。第二大量问题属于组合数学。这类问题的本质是在有限的离散结构里找规律、找反例、找构造非常适合算法和搜索方法发挥作用。暴力验证一个小规模情形往往能给整个问题带来关键线索。第三小规模验证与完整证明之间存在一条明确的晋升路径。AI 可以先对 n3、n4 的情形做计算验证找到模式再尝试把模式推广成一般性证明。这种“从小到大、从计算到证明”的路径恰好是现有 AI 系统相对擅长的事。所以“Erdős 难题正在被 AI 攻克”这类标题背后并不是某个单一模型的灵光一现而是一整套工具链的成熟。3. AI 做数学的两种路线直觉生成与形式化验证要理解 AI 在数学上的真实进展必须先分清两条完全不同的技术路线。第一条路线是“自然语言证明生成”。你把一道题抛给 LLM它用人类可读的自然语言写出解法。优点很明显门槛低速度快推理过程可读。但缺点也很致命缺少强制性检查。大模型生成数学证明时幻觉率远高于写普通文本。它可能错误调用一个不存在的定理可能在上一步到下一步之间偷偷改变条件甚至可能用一句“显然可得”掩盖整个推导的断裂。更麻烦的是在数学里一个看起来无懈可击的证明可能只在第 17 行有一个符号错误就导致整个结论崩塌。人类读者很难发现这种错误AI 自己也意识不到。因此纯自然语言路线在严谨数学中只能作为“启发式工具”不能作为“判定工具”。第二条路线是“形式化证明”。这不是让 AI 用自然语言写证明而是让证明变成机器可以逐条检查的形式化推导。代表工具是 Lean、Coq、Isabelle 这类证明助手Proof Assistant。在这种路线里每一处推理都必须调用明确的规则每一个中间结论都必须能被机器验证。AI 可以参与生成证明步骤但最终裁判是证明验证器——它不会因为“语气自信”而放过任何错误。两条路线的差异可以这样理解自然语言证明像 AI 给你拍胸脯保证“这件事我查过了没问题”形式化证明像 AI 把每一张单据、每一笔流水都摊开给你由独立审计员逐条核对。前者解决“快不快”的问题后者解决“对不对”的问题。一个成熟的 AI 数学系统通常是把两者结合用 LLM 提供“这个方向可能可行”的直觉判断再用证明助手和搜索算法强行完成验证。这也是为什么近两年大家的关注点逐渐从“大模型会不会做小学数学题”转向“形式化数学库建得够不够大”。4. 为什么形式化证明是 AI 攻破数学难题的关键上一节提到的证明助手 Lean 4是目前 AI-for-Math 领域最受关注的工具之一。它背后是数学社区维护的 mathlib 库——一个被形式化验证过的庞大数学知识库。这意味着 AI 在 Lean 里做证明时可以调用大量已经被证明的定理而不必从零开始。这个设计非常关键。在旧工作流里AI 生成一个证明人类得花大量时间去人工检查而在 Lean 工作流里AI 生成证明脚本Lean 负责检查每一步是否合法。如果 AI 的某个步骤引用了不存在的定理Lean 立刻报错如果两个条件不能同时成立Lean 立刻拒绝。也就是说形式化证明天然隔离了 LLM 的幻觉。近年来的一些成果也印证了这条路线。2024 年Google DeepMind 的 AlphaProof 在 IMO国际数学奥林匹克赛题上达到了银牌水平它解决的问题里既有自然语言生成也有 Lean 形式化验证的环节。更早一些的 AlphaGeometry 则结合语言模型和符号引擎在几何题上超过了人类金牌选手的平均水平。此外开源社区也出现了 DeepSeek-Prover 这类专门面向定理证明的模型目标就是生成能被 Lean 检查的证明代码。但这里必须给一个冷静的判断从“AI 能在竞赛题和部分研究级问题上辅助证明”到“AI 独立攻破一个流传几十年的 Erdős 难题”中间还有很长的距离。新闻报道里说的“falling to AI”更准确的理解是AI 系统正在越来越多地参与这些难题的子问题——验证特例、寻找反例、构造辅助引理、缩小搜索空间。这些工作过去完全依赖人类耐心现在可以由 AI 半自动完成。对工程师来说这里有一个值得注意的类比形式化验证证明的是“数学证明正确”而类型系统、静态分析验证的是“代码行为正确”。两者的底层思想完全一致——用机器可检查的规则替代人的记忆和直觉。所以学习 Lean 不只是为了玩数学它对你理解类型系统和编译原理也有直接帮助。5. 环境准备搭建你自己的 AI 数学验证工作台下面进入实操。我们从零搭建一个最小可用的“AI 数学验证工作台”包含三部分Lean 4形式化验证、Python暴力搜索、LLM API猜想生成。版本信息请以官方文档为准这里演示的是通用流程。5.1 安装 Lean 4Lean 4 官方推荐的安装方式是通过 elan 这个版本管理工具类似 Rust 的 rustup。在 macOS 或 Linux 终端执行# 安装 elan curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh国内网络环境访问 GitHub 可能不稳定如果安装失败请参考 Lean 官方社区镜像或稍后重试。安装完成后重新打开终端确认版本elan --version然后用 VS Code 安装 Lean 4 扩展它会自动识别 elan 安装的 Lean 工具链。创建项目时使用带 mathlib 的模板# 创建 Lean 4 mathlib 项目 mkdir ai-math-lab cd ai-math-lab lake new ai_math_lab math cd ai_math_lab lake update mathlib项目创建后用 VS Code 打开目录等待 mathlib 编译或下载缓存。第一次构建可能耗时较长这也正常。5.2 准备 Python 环境Python 负责计算验证和调用 LLM API。建议创建独立虚拟环境python3 -m venv .venv source .venv/bin/activate # Windows 用户执行 .venv\Scripts\activate pip install openai sympyopenai是官方 SDK用于调用兼容 OpenAI 接口的大模型服务sympy用于符号计算本文的示例里不是必需但后续做数学实验时很常用。5.3 配置 LLM API把 API Key 放到环境变量里不要写进代码或提交到仓库。这是最基本的安全习惯export LLM_API_KEY你的API Key export LLM_BASE_URLhttps://api.openai.com/v1 export LLM_MODELgpt-4o-mini不同服务商的地址和模型名不同以实际订阅的服务文档为准。6. 完整示例从猜想生成到机器验证这一节我们用同一个数学场景——K_n 完全图的 2 染色问题——走完三个环节LLM 生成猜想、Python 暴力搜索找反例、Lean 形式化证明。这个场景本身出自 Erdős 最热爱的 Ramsey 理论很适合演示。6.1 用 LLM 生成候选猜想先写一个脚本让 LLM 针对一个问题提出可验证的猜想。文件路径# hypothesis_gen.py import os from openai import OpenAI client OpenAI( api_keyos.getenv(LLM_API_KEY), base_urlos.getenv(LLM_BASE_URL, https://api.openai.com/v1), ) prompt 你是一位组合数学研究者。针对下面的问题给出一个可以用代码做小规模验证的候选猜想。 要求猜想必须能用暴力搜索在 n 较小的情况下快速检验并解释它为什么可能与原问题相关。 问题在 n 个顶点的完全图 K_n 中将每条边染成红色或蓝色。 定义单色三角形为三个顶点之间三条边颜色完全相同的三角形。 请猜想单色三角形数量的最小值随 n 如何变化给出一个可检验的下界表达式。 resp client.chat.completions.create( modelos.getenv(LLM_MODEL, gpt-4o-mini), messages[{role: user, content: prompt}], temperature0.7, ) print(resp.choices[0].message.content)这一步明确体现了 AI 的角色它负责给出“可能的答案”而不是“确定的结论”。它的输出下面必须经过验证。6.2 用 Python 暴力搜索找反例Erdős 风格的问题第一步永远是小规模计算。下面的脚本枚举 K_n 的所有 2 染色检查是否存在不含任何单色三角形的染色方案。如果存在就说明某个下界猜想在 n 这个值上被推翻了。# ramsey_check.py import itertools def has_mono_clique(vertices, edges_set, k): 判断 vertices 中是否存在 k 个顶点使得两两之间的边都在 edges_set 里。 for combo in itertools.combinations(vertices, k): if all(tuple(sorted(pair)) in edges_set for pair in itertools.combinations(combo, 2)): return True return False def check_k_n(n, k3): vertices list(range(n)) all_edges [tuple(sorted(e)) for e in itertools.combinations(vertices, 2)] for mask in range(1 len(all_edges)): red {all_edges[i] for i in range(len(all_edges)) if (mask i) 1} blue set(all_edges) - red if not has_mono_clique(vertices, red, k) and not has_mono_clique(vertices, blue, k): print(fn{n}: 找到反例存在不含单色三角形的 2 染色。) return False print(fn{n}: 验证通过任意 2 染色都存在单色三角形。) return True if __name__ __main__: check_k_n(5) # 期望找到反例 check_k_n(6) # 期望验证通过这里有个细节值得停下来看check_k_n(5)应该找到反例而check_k_n(6)应该验证通过。这正对应 Ramsey 理论中著名的结论 R(3,3)65 个顶点时可以构造一个不含单色三角形的染色6 个顶点时不可能。这个结果本身就很符合 Erdős 题目的气质——临界点清晰构造和反例同样重要。6.3 用 Lean 完成形式化证明跑通暴力搜索之后你得到的是“n6 时所有 2 染色都被穷举验证过了”但这还不是数学意义上的证明因为枚举 2^15 种染色只是检查了 K_6 这个具体情形。Erdős 难题需要的是对任意 n 成立的证明或者至少是某个关键定理的严格证明。形式化证明工具在这里发挥真正价值。把下面的代码保存为 Lean 项目中的Test.leanimport Mathlib -- 例 1自然数加法的结合律 -- 这是最基础的形式化证明练习验证 Lean 环境是否正常工作 theorem add_assoc_example (a b c : ℕ) : (a b) c a (b c) : by rw [Nat.add_assoc] -- 例 2任何整数的平方非负 -- 这种看似显然的命题Lean 依然要求你引用正确的定理或策略 theorem square_nonneg_example (n : ℤ) : 0 ≤ n ^ 2 : by exact sq_nonneg n第一个证明使用了rw [Nat.add_assoc]把左边重写为右边第二个证明直接调用数学库里的sq_nonneg定理。这两个例子很简单但足以让你感受 Lean 的工作方式目标会被逐步化简直到变成一个恒等式或一个可由已知定理直接解决的问题。看完基础例子可以尝试更有 Erdős 风格的命题。比如证明“任何整数的平方加 1 恒大于 0”-- 例 3n^2 1 ≥ 1等价于 n^2 ≥ 0 theorem square_add_one_pos (n : ℤ) : 1 ≤ n ^ 2 1 : by nlinarith [sq_nonneg n]这里nlinarith是处理非线性整数算术的策略sq_nonneg n提供了0 ≤ n^2这个关键前提。可以看到Lean 的证明思路和人类差不多先找到一个已知结论再把它整合进目标里。顺带说明把 K_6 的 Ramsey 结论完整形式化需要定义图、染色、三角形、完全图这些概念工作量比上面三个例子大很多但它正是 mathlib 社区每天都在做的那种事。真正研究级的 AI 数学系统就是在这种基础设施之上构建证明的。7. 运行结果与验证方法各环节跑完如何判断结果是否正常Python 暴力搜索的运行方式python ramsey_check.py预期输出大致是n5: 找到反例存在不含单色三角形的 2 染色。 n6: 验证通过任意 2 染色都存在单色三角形。如果n5没有找到反例或者n6反而找到反例说明代码实现有 bug优先检查all_edges的生成和has_mono_clique的边匹配逻辑。Lean 的验证方式更直观在 VS Code 中打开Test.lean如果代码没有红色波浪线Lean 扩展右下角显示正常就表示所有定理都被机器接受。命令行验证方式如下lake env lean Test.lean如果命令没有任何输出就直接结束说明文件中的所有证明都通过了。如果出现unsolved goals或错误信息就按错误提示定位到对应行。这里需要强调一个验证原则LLM 生成的内容不管输出多漂亮都必须经过 Python 代码或 Lean 验证后才算“可信”。在整个工作流中LLM 是提出者Python 是初步检查员Lean 是最终裁判。裁判说不行的东西再动听也不算数。8. 常见误区与排查思路实际跑这套流程时新手会踩到一些典型的坑整理成表格方便对照排查问题现象可能原因排查方式解决方案LLM 给出的证明看起来没问题但用 Lean 验证失败LLM 幻觉引用了不存在的定理或跳步把 LLM 输出和 Lean 报错对照定位第一个不被接受的步骤把证明拆成更小的引理逐条验证或者让 LLM 参考 mathlib 中已有的定理名称Lean 文件报unknown identifier没有正确导入对应的 Mathlib 模块查看报错信息里的标识符检查import Mathlib是否在最顶部确保文件第一行是import Mathlib如果仍不行执行lake update mathlib首次lake build非常慢mathlib 体积大需要全量编译观察 VS Code 下方的进度提示耐心等待后续再次编译会走缓存速度大幅提升暴力搜索在 n7 时运行极慢染色方案数为 2^(C(n,2))指数爆炸检查循环次数和时间复杂度用剪枝、SAT/SMT 求解器或改用随机搜索先找反例openai调用报 401API Key 或base_url配置错误检查环境变量是否在当前终端生效确认 API Key 有效不要硬编码在代码里换个已知可用的服务商误以为“小规模验证通过”等于“问题已解决”混淆计算验证与数学证明回头看问题是针对具体 n 还是所有 n只有对所有 n 成立的证明才算解决计算验证只作为启发线索从这张表可以看到大多数问题都源于工具链使用不当或对验证边界的误解而不是某个环节“不够聪明”。正确的工作流能把这些坑提前暴露。9. 对工程师的启示与最佳实践这套 AI 数学工作流本质上和 AI 辅助编程是同一套方法论。如果你平时用 LLM 辅助写代码下面几条最佳实践可以直接迁移。第一把 AI 当成“方案生成器”而不是“答案判定器”。无论是写代码还是做数学LLM 的价值在于快速给出候选方案而质量检查必须交给编译器、测试和形式化工具。不要因为模型语气笃定就跳过验证。第二所有验证过程必须可复现、可追溯。记录输入问题、模型版本、Prompt、验证命令和输出结果。数学工作尤其如此——一个无法复现的“证明”没有任何价值。写代码时同理把requirements.txt、lakefile.toml、环境变量清单都纳入版本管理。第三小步快跑先验证最小情形。不要一上来就试图证明一个大的 Erdős 难题。先从 n3、n4 这类情形开始用暴力搜索找规律把问题拆成若干个小引理再逐步证明。这个策略和软件工程里的“先跑通最小可行产品”完全一致。第四注意安全界。API Key 只通过环境变量注入不要提交到仓库Lean 项目依赖的第三方库要检查来源AI 生成的内容应用到正式场景前必须有独立验证。本文涉及的所有操作都是常规开发工具的使用但在真实项目中依然要遵循最小权限原则。第五正视工具边界。截至本文写作时间AI 在数学上的公开成果还集中在竞赛题、验证子问题和小规模定理证明层面。看到“AI 攻克某难题”的报道时先看两个东西有没有同行评审、有没有可复现的形式化证明。这两个问题能帮你过滤掉 90% 的夸张宣传。10. 总结与后续学习方向回到文章开头的问题Erdős 难题真的在被 AI 攻破吗更准确的说法是AI 正在成为数学家的新工具而真正让这个说法有分量的不是大模型的“聪明”而是形式化验证系统的成熟。Erdős 艰难题在传播中被简化为一个口号但技术工作者应该看到口号背后的工程细节LLM 负责直觉搜索算法负责探索Lean 负责审计人类负责设定方向和解释结果。如果你对这条路线感兴趣建议按下面的顺序继续深入先跑通本文三个示例确认 Lean 环境和 Python 环境都正常。学习 Lean 基础语法尝试把一些简单数学命题形式化例如“奇数的平方是奇数”“质数有无穷多个”。后者的完整证明在 mathlib 中已有高质量范本可以直接对着学习。关注 mathlib 社区和 AI-for-Math 方向的开源项目例如 DeepSeek-Prover 这类面向定理证明的模型。挑一个自己感兴趣的组合猜想的退化情形用“LLM 提猜 Python 找反例 Lean 证引理”的流程做一轮实验体会完整工作流带来的节奏感。下一次你再看到“传奇 Erdős 难题正在被 AI 攻破”的标题可以先别急着转发。打开 Lean把标题里的宣称变成一个可以证明的命题然后用机器验证它。这个过程本身就是 AI 时代工程师参与数学最脚踏实地的方式。