AI攻克Erdős问题：大模型与形式化验证如何革新数学研究

这次我们来看一个不是“又发布了新模型”，而是实打实改变数学研究方式的话题：传奇的 Erdős 问题集，正在一个接一个地被 AI 攻克。

Erdős 问题集来自 20 世纪数学家 Paul Erdős 和他的合作者们，里面包含大量数论、组合学、图论、概率论和集合论问题。很多问题表述只有几行字，甚至高中生都能读懂，但几十年没人能解出来。过去这类问题主要靠数学家长期“泡”出来的直觉，现在情况发生了变化：大语言模型负责“猜”，形式化证明工具负责“验”，强化学习和搜索算法负责“找路径”。这种组合让一批原本极难推进的问题开始松动。

这篇文章不打算讲太多故事，而是直接拆解三件事：

1. AI 攻克 Erdős 问题的技术原因，到底是大模型“聪明了”，还是验证工具“顺手了”；
2. 如果你想复现这类实验，需要准备什么环境、跑什么流程；
3. 哪些场景适合让 AI 介入，哪些地方容易出现幻觉、假证明和不可复现的结果。

如果你关心 AI 数学推理、自动定理证明、Lean 形式化验证，或者只是想知道“现在 AI 到底能不能做数学研究”，这篇可以直接收藏。

1. AI 数学推理核心能力速览

先把大家最关心的能力项列出来。这里不针对某个具体开源项目，而是综合当前常见技术路线，整理成一张可对照的速查表。

从表格能看到，这不是“一个模型解决所有问题”，而是“生成器 + 验证器 + 搜索器”的工程闭环。理解这一点，后面所有内容都好接了。

2. 为什么传奇的 Erdős 问题会落到 AI 手里

2.1 Erdős 问题为什么难

很多 Erdős 问题难就难在“没有路标”。

它们通常是大量小条件叠加在一起，给定一个看似简单的集合或图，要求你证明存在某种结构，或者反过来证明不存在。这类问题的共同点是：搜索空间巨大，但局部规律非常稀疏。

过去数学家解决这类问题，依赖的是两个能力：一是对已有定理的深刻理解，二是针对具体问题的“手感”。手脚麻利的数学家可以在几十个特殊情形里试错，凭经验知道哪些方向会碰壁。但这种经验通常是私有的、碎片化的，很难迁移。

AI 介入之后，这套逻辑发生了变化。大模型可以从海量论文和题目里提取“这种结构之前在哪里出现过”，快速生成候选方向；程序化搜索可以在一秒内枚举人工需要几天的特殊情况；形式化工具则能把“看起来对”的证明转成机器可检查的严格推导。

2.2 大模型解决的是“从哪个方向试”

大模型不是直接写出最终证明。它更擅长的是：面对一个陌生问题时，给出一个可能成立的中间引理、一个构造性想法，或者一个值得验证的小规模例子。

举个例子，如果题目问“是否存在一组正整数，使得任意两个数之差的绝对值都是合数”，模型可能会说“先看连续区间里筛掉素数间隔的结构”。这个想法不一定对，但确实缩小了搜索范围。接下来用程序枚举小规模情形，把结果不符合的假设删掉，保留还能继续的假设。

这就是“AI 推动 Erdős 问题”的第一层原因：搜索方向的初筛成本被大幅降低。

2.3 形式化验证让“猜想”变成“可执行语句”

光靠“想”不够。过去论文审稿人要花大量时间检查推理链，现在用 Lean、Coq 这类证明助手，可以把数学命题写成形式化语句，机器逐行检查。一旦证明脚本通过，几乎不存在“隐藏假设讲不清”的问题。

AI 和形式化验证结合后，流程变成：

1. 大模型输出一个候选证明思路；
2. 人将思路拆成若干步，用证明助手逐步实现；
3. 某些步骤如果太繁琐，可以交给大模型生成；
4. 证明助手报错，人就根据报错修正或放弃该思路。

这不是“AI 凭空证明”，而是“AI 生成 + 机器验证 + 人工修正”。这个流程比纯人工试错快很多，也是近期进展集中的原因。

2.4 强化学习负责“在证明树里找路”

还有一类方法不用大模型直接写证明，而是把数学问题建模成搜索问题。模型通过大量尝试学习“哪一步更有可能通向证明”，类似下棋 AI 的蒙特卡洛树搜索。这种方法特别适合证明树较深的问题：每一步都有很多选择，但只有少数选择能通向结果。

这类系统需要大量算力做训练，但推理时可以刻意控制搜索深度和宽度。对于 Erdős 问题这种“中间步骤很少但选择极多”的类型，强化学习搜索比暴力枚举更聪明。

可以说，AI 解决 Erdős 问题的本质，不是用一个更聪明的“大脑”替代数学家，而是把“读文献、猜方向、写细节、检查错误”这四个环节，分别用不同的工具自动化了一部分。

3. 适用场景与使用边界

3.1 适合谁

• 数学系学生：用 AI 快速生成一个问题的反例猜想，再用程序验证，训练数学直觉。
• 数学研究者：让 AI 帮忙搜索某些极端构造，减轻琐碎工作。
• AI 应用开发者：把数学推理能力作为大模型效果的测评基准。
• 竞赛选手：让模型生成解题方向，再人工检查细节。

3.2 能解决什么问题

• 小规模反例搜索：组合题中是否存在一个 10 以内的反例，用暴力枚举最快。
• 证明路径探索：给出一个目标命题，让模型提出多个不同的证明方向。
• 引理补齐：主证明已经写到只剩一个繁琐不等式，让模型生成证明草稿。
• 形式化翻译：把自然语言命题改写成 Lean 语法，加速形式化过程。

3.3 不适合什么

• 不能直接输入“帮我证明 Erdős 第 X 题”就期待输出可靠证明。
• 不能把大模型生成的证明当作最终答案直接投稿。
• 不能在有严格审稿、研究伦理和保密要求的场景里，把未经验证的 AI 输出当事实使用。
• 涉及未公开数据、私有资料、他人未发表成果时，必须先确认授权。

3.4 版权、隐私与学术规范边界

使用 AI 辅助数学研究时，需要明确记录哪些内容由 AI 生成、哪些由人验证。如果最终发表论文，应按照期刊或机构规定声明 AI 使用情况。不要用 AI 伪造证明过程，不要拿未验证的结论去干扰他人研究。数学研究同样存在学术诚信问题，这一点和代码、文本生成没有区别。

4. 复现 AI 数学推理实验的环境准备与前置条件

如果你想自己跑一个类似“AI 提出猜想 + 程序验证”的小实验，不需要很强的硬件。下面给一套通用环境准备方案。

4.1 软件清单

4.2 GPU 和显存

如果你只是调用远程 API，本地只需要一个普通 CPU 环境。若是想在本地跑 7B 级别模型，一般需要 6G 以上显存，但具体占用取决于量化方式、上下文长度和并发数量。想观察显存，推荐在推理时另开一个终端运行：

nvidia-smi -l 2

这个命令每 2 秒刷新一次显存信息。不要把固定数字当结论，要以自己机器上的实测值为准。

4.3 安装 Python 环境

python -m venv venv source venv/bin/activate # Windows 下执行 venv\Scripts\activate pip install requests

4.4 安装 Lean 4 工具链（可选）

如果你希望做形式化验证，可以安装 Lean 4。Lean 官方推荐通过 elan 管理工具链：

curl -fsSL https://get.elan-lang.org | bash source "$HOME/.elan/env" lean --version

安装完成后，在 VS Code 里安装 Lean 插件，新建一个.lean文件即可开始。具体安装版本以 Lean 官方文档为准。

4.5 准备接口 Key

调用商业大模型 API 时需要准备 API Key，并且不要硬编码在公开仓库里。建议放在环境变量中：

export MATHAI_API_KEY="your-key-here"

如果使用本地模型，则不需要 Key，但需要配置模型服务地址和端口。

5. 功能测试与效果验证

下面用一套可执行的流程，测试“大模型生成思路 + 程序验证 + 形式化验证”三个环节。这里的代码是通用模板，你可以替换成实际问题。

5.1 测试 1：让大模型生成候选猜想

假设我们要研究一个组合问题：是否存在一个长度为 10 的整数集合，使任意两个数的差都大于 1 且其中至少有一个数是合数。这个例子本身并不复杂，但足以验证 AI 是否能提出可检查的构造。

先写一个调用大模型接口的函数。以兼容 OpenAI 格式的 API 为例：

import os import requests API_URL = "https://api.example.com/v1/chat/completions" # 替换为实际服务地址 API_KEY = os.getenv("MATHAI_API_KEY") def ask_model(prompt: str, temperature: float = 0.2) -> str: headers = { "Authorization": f"Bearer {API_KEY}", "Content-Type": "application/json" } payload = { "model": "your-model-name", # 替换为实际模型名 "messages": [ { "role": "system", "content": "你是一个数学猜想生成器。请给出具体、可验证的候选构造或证明思路。" }, { "role": "user", "content": prompt } ], "temperature": temperature, "max_tokens": 500 } response = requests.post(API_URL, json=payload, headers=headers, timeout=60) response.raise_for_status() return response.json()["choices"][0]["message"]["content"] prompt = "请给出一个长度为10的整数集合，要求集合中任意两个数的差都大于1，并且每个数都是合数。" result = ask_model(prompt) print(result)

输出可能是一组数，也可能是一个构造思路。判断是否成功，不是看它是否“像样”，而是看后续能否通过独立程序验证。

5.2 测试 2：用 Python 暴力验证

将模型给出的候选集合保存到列表，写一个校验函数：

from itertools import combinations def is_composite(n: int) -> bool: if n < 2: return False for d in range(2, int(n ** 0.5) + 1): if n % d == 0: return True return False def verify_candidates(candidates): if len(candidates) != 10: return False, "集合长度不等于10" if len(set(candidates)) != 10: return False, "存在重复元素" for a, b in combinations(candidates, 2): if abs(a - b) <= 1: return False, f"差过小: {a}, {b}" for n in candidates: if not is_composite(n): return False, f"不是合数: {n}" return True, "验证通过" candidate_set = [] # 填入模型输出中的数 ok, msg = verify_candidates(candidate_set) print(ok, msg)

这样就把“AI 生成”和“结果验证”分开了。模型输出只是假设，验证结果才是结论。

5.3 测试 3：用 Lean 验证一个简单数学命题

正式场景下可以用 Lean 写证明。例如验证一个基础算术等式：

theorem add_two_two : 2 + 2 = 4 := by norm_num

norm_num是 Lean 自带的数值计算策略，可以直接处理这类等式。在 VS Code 中保存为.lean文件后，可以查看 Lean 的反馈窗口。如果通过，会看到No goals；如果失败，会显示未完成的目标。

对于复杂的 Erdős 问题，你不需要一口气写完证明，而是先把目标拆分成许多小引理，每一条用 Lean 检查。大模型可以帮忙生成候选引理，但最终是否通过，由 Lean 决定。

5.4 测试 4：反例搜索

很多数论问题可以先猜“不存在”，然后写程序找反例。比如检查某个范围内的数是否满足某个性质，用暴力搜索可能比数学推导更快。

def search_counterexample(limit: int = 100): found = [] for n in range(2, limit): # 这里替换成实际问题中的条件 if n % 2 == 0 and n % 3 > 0: found.append(n) return found[:10] print(search_counterexample(100))

这只是一个模板，实际使用时要把条件替换成你正在研究的问题。搜索到反例后，再让模型解释为什么这个反例成立，形成“生成-验证-解释”闭环。

5.5 判断是否成功

每个功能测试都要有明确的成功标准：

• 大模型输出：只要包含可操作的具体构造或步骤，就算初步成功。
• Python 验证：程序运行时无异常，返回结果符合目标，才算通过。
• Lean 验证：Lean 不再报告未完成目标，才算通过。
• 反例搜索：发现问题中目标对象，但需要人工确认条件与题意一致。

如果失败，最常见的两个原因是：大模型输出太抽象、无法转成代码；或者提议的构造在边界条件下被证伪。解决方式是修改 prompt，要求输出“具体的数字/字符串/表达式”，而不是解释概念。

6. 接口 API 与批量任务：批量验证候选答案

真实研究里不会只让模型答一次。更常见的做法是批量生成候选答案，再统一验证。下面给出一个批量任务的框架。

6.1 批量生成候选

prompts = [ "请给出问题 A 的构造", "请给出问题 B 的候选证明思路", "请改进以下构造: ..." ] results = [] for i, p in enumerate(prompts): try: answer = ask_model(p, temperature=0.5) results.append({"task_id": i, "prompt": p, "answer": answer, "status": "success"}) except Exception as e: results.append({"task_id": i, "prompt": p, "answer": str(e), "status": "failed"})

这里把每次调用的任务 ID、问题和结果都记录下来，方便后续验证和复盘。批量生成时要注意接口频率限制，必要时增加延时：

import time import random for i, p in enumerate(prompts): ... time.sleep(random.uniform(0.5, 1.5))

6.2 批量验证

验证环节可以单独写成脚本：

def batch_verify(answers): for item in answers: if item["status"] != "success": continue # 假设答案里包含候选数字集合，需要按实际格式解析 candidates = parse_answer(item["answer"]) ok, msg = verify_candidates(candidates) item["valid"] = ok item["verify_message"] = msg return answers

这里的parse_answer需要根据模型输出格式单独写。强烈建议在 prompt 中要求模型输出纯 JSON 或列表，方便解析。例如：

请只输出一个数组，不要额外解释，例如 [10,12,14,...]

这样可以减少解析失败。

6.3 失败重试

API 调用超时、限流、模型返回空内容是常见问题。实现重试时要避免无限循环，建议最多重试 3 次，且每次等待时间递增：

def ask_model_with_retry(prompt, retries=3): for i in range(retries): try: return ask_model(prompt) except Exception as e: print(f"第{i+1}次失败: {e}") time.sleep(2 ** i) raise RuntimeError("请求失败次数过多")

批量任务的核心不是“让模型答得快”，而是“每条结果都有状态、可检验、可重跑”。这样遇到失败时不至于从头再来。

7. 资源占用与性能观察

7.1 接口方案

使用 API 时，本地 CPU 占用很低，主要资源消耗是 token 和网络请求时间。观察项包括：

• prompt 长度：越长，耗时和费用越高。
• max_tokens：设置过大时会增加等待时间。
• 并发数量：并发太高会被限流。
• 输入输出字符数：可用于估算成本。

建议每次请求都打印耗时和 token 数：

start_time = time.time() response = requests.post(...) elapsed = time.time() - start_time usage = response.json().get("usage", {}) print(f"耗时 {elapsed:.2f}s, 用量 {usage}")

7.2 本地模型方案

如果本地运行大模型，显存占用主要取决于模型参数量、量化位数、推理批大小和上下文长度。可以用nvidia-smi观察。重要判断是：稳定运行时的占用量，而不是加载瞬间的峰值。

降低显存常见方法：

• 选用量化版本模型；
• 把 batch_size 降到 1；
• 限制 max_new_tokens；
• 关闭不用的缓存；
• 使用流式输出，避免一次性申请整段显存。

7.3 推理时间与问题难度

推理时间会更直接地影响体验。数学问题往往需要长输出，长回答意味着 GPU 计算时间越长。如果只是验证某个候选构造是否可行，优先让模型输出短结构，而不是长篇证明。这样可以显著降低等待时间和资源占用。

8. 常见问题与排查方法

下面把最容易遇到的问题整理成排查表。

9. 最佳实践与使用建议

9.1 把 AI 当作“猜想加速器”

正式结论必须由验证器或人工证明确认。AI 的价值在于扩大搜索范围，降低试错成本。不要因为模型给出了“看起来严谨”的证明就直接采用。

9.2 保留完整的实验记录

对于每一个问题，建议维护一条记录，包含：

• 问题编号和完整表述；
• 使用的模型名称、版本、温度、prompt；
• AI 输出全文或摘要；
• 验证脚本和运行结果；
• 最终结论（通过 / 失败 / 待进一步验证）。

这样可以复现实验，也能避免重复提问。

9.3 小问题先跑通

第一次做 AI 数学推理，不要一上来就进军几十年的未解问题。从一个可以暴力枚举的小型组合问题开始，让模型生成候选，程序验证，跑通后再逐步提高难度。

9.4 注重版权与学术诚信

使用 AI 辅助研究时，如果使用了第三方论文、代码或私有数据，必须先确认授权。在论文中如实说明 AI 使用情况。不发布无法验证的证明，不把其他研究者的未发表思路搬进自己的结论里。

9.5 接口服务要控制访问范围

如果自己搭建 API 服务，建议设置访问令牌、限速、日志记录。避免把服务直接暴露在不安全网络环境，防止批量调用导致资源耗尽。

10. 总结与下一步

Erdős 问题被 AI 攻克，本质不是一个模型单打独斗，而是“大模型猜方向、程序验证结果、证明助手查逻辑”的工程体系越来越成熟。对普通人来说，最有价值的不是等着新成果发布，而是立刻用这套流程跑通一个小问题。

建议先做三件事：

1. 装好 Python 环境，跑通一个简单的模型对话请求；
2. 选一个可以暴力枚举的小型数论题，让模型生成候选构造；
3. 用脚本或 Lean 验证模型输出，记录一份“生成-验证”实验日志。

最容易踩的坑，是把大模型的输出直接当成答案。只要你坚持“先验证，后采信”，这套方法论就是安全且有效的。

接下来如果你想深入，可以直接学 Lean 4，尝试把一个已知数论引理形式化。这不是为了立刻解决大问题，而是为了理解机器验证的价值。等你习惯了这种节奏，再回头看那些传奇的 Erdős 问题，就会明白为什么 AI 开始一个个撬动它们了。