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 Problem），2015 年由陶哲轩完成证明，那是一个纯人类智慧的成果。还有一些问题始终悬而未决，恰恰是这类问题，现在成了 AI 系统试身手的舞台。
为什么 AI 偏偏看上了 Erdős 难题？有三个原因：
第一，问题陈述足够精确。AI 系统最怕模糊的任务，而 Erdős 难题往往用“是否存在”“是否对所有 n 成立”这样清晰的逻辑陈述，可以直接转化为可验证的形式化目标。
第二，大量问题属于组合数学。这类问题的本质是在有限的离散结构里找规律、找反例、找构造，非常适合算法和搜索方法发挥作用。暴力验证一个小规模情形，往往能给整个问题带来关键线索。
第三，小规模验证与完整证明之间存在一条明确的晋升路径。AI 可以先对 n=3、n=4 的情形做计算验证，找到模式，再尝试把模式推广成一般性证明。这种“从小到大、从计算到证明”的路径，恰好是现有 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 4
Lean 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_URL="https://api.openai.com/v1" export LLM_MODEL="gpt-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_key=os.getenv("LLM_API_KEY"), base_url=os.getenv("LLM_BASE_URL", "https://api.openai.com/v1"), ) prompt = """你是一位组合数学研究者。针对下面的问题，给出一个可以用代码做小规模验证的候选猜想。 要求：猜想必须能用暴力搜索在 n 较小的情况下快速检验，并解释它为什么可能与原问题相关。 问题：在 n 个顶点的完全图 K_n 中，将每条边染成红色或蓝色。 定义单色三角形为三个顶点之间三条边颜色完全相同的三角形。 请猜想：单色三角形数量的最小值随 n 如何变化？给出一个可检验的下界表达式。""" resp = client.chat.completions.create( model=os.getenv("LLM_MODEL", "gpt-4o-mini"), messages=[{"role": "user", "content": prompt}], temperature=0.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, k=3): 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(f"n={n}: 找到反例！存在不含单色三角形的 2 染色。") return False print(f"n={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)=6：5 个顶点时可以构造一个不含单色三角形的染色，6 个顶点时不可能。这个结果本身就很符合 Erdős 题目的气质——临界点清晰，构造和反例同样重要。
6.3 用 Lean 完成形式化证明
跑通暴力搜索之后，你得到的是“n=6 时所有 2 染色都被穷举验证过了”，但这还不是数学意义上的证明，因为枚举 2^15 种染色只是检查了 K_6 这个具体情形。Erdős 难题需要的是对任意 n 成立的证明，或者至少是某个关键定理的严格证明。
形式化证明工具在这里发挥真正价值。把下面的代码保存为 Lean 项目中的Test.lean：
import 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”：
-- 例 3：n^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预期输出大致是：
n=5: 找到反例！存在不含单色三角形的 2 染色。 n=6: 验证通过，任意 2 染色都存在单色三角形。如果n=5没有找到反例，或者n=6反而找到反例，说明代码实现有 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 下方的进度提示 | 耐心等待；后续再次编译会走缓存，速度大幅提升 |
| 暴力搜索在 n=7 时运行极慢 | 染色方案数为 2^(C(n,2))，指数爆炸 | 检查循环次数和时间复杂度 | 用剪枝、SAT/SMT 求解器，或改用随机搜索先找反例 |
openai调用报 401 | API Key 或base_url配置错误 | 检查环境变量是否在当前终端生效 | 确认 API Key 有效；不要硬编码在代码里；换个已知可用的服务商 |
| 误以为“小规模验证通过”等于“问题已解决” | 混淆计算验证与数学证明 | 回头看问题是针对具体 n 还是所有 n | 只有对所有 n 成立的证明才算解决；计算验证只作为启发线索 |
从这张表可以看到，大多数问题都源于工具链使用不当或对验证边界的误解，而不是某个环节“不够聪明”。正确的工作流能把这些坑提前暴露。
9. 对工程师的启示与最佳实践
这套 AI 数学工作流，本质上和 AI 辅助编程是同一套方法论。如果你平时用 LLM 辅助写代码，下面几条最佳实践可以直接迁移。
第一，把 AI 当成“方案生成器”，而不是“答案判定器”。无论是写代码还是做数学，LLM 的价值在于快速给出候选方案，而质量检查必须交给编译器、测试和形式化工具。不要因为模型语气笃定就跳过验证。
第二，所有验证过程必须可复现、可追溯。记录输入问题、模型版本、Prompt、验证命令和输出结果。数学工作尤其如此——一个无法复现的“证明”没有任何价值。写代码时同理：把requirements.txt、lakefile.toml、环境变量清单都纳入版本管理。
第三，小步快跑，先验证最小情形。不要一上来就试图证明一个大的 Erdős 难题。先从 n=3、n=4 这类情形开始，用暴力搜索找规律，把问题拆成若干个小引理，再逐步证明。这个策略和软件工程里的“先跑通最小可行产品”完全一致。
第四，注意安全界。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 时代工程师参与数学最脚踏实地的方式。
