这次我们来看一个不是“又发布了新模型”而是实打实改变数学研究方式的话题传奇的 Erdős 问题集正在一个接一个地被 AI 攻克。Erdős 问题集来自 20 世纪数学家 Paul Erdős 和他的合作者们里面包含大量数论、组合学、图论、概率论和集合论问题。很多问题表述只有几行字甚至高中生都能读懂但几十年没人能解出来。过去这类问题主要靠数学家长期“泡”出来的直觉现在情况发生了变化大语言模型负责“猜”形式化证明工具负责“验”强化学习和搜索算法负责“找路径”。这种组合让一批原本极难推进的问题开始松动。这篇文章不打算讲太多故事而是直接拆解三件事AI 攻克 Erdős 问题的技术原因到底是大模型“聪明了”还是验证工具“顺手了”如果你想复现这类实验需要准备什么环境、跑什么流程哪些场景适合让 AI 介入哪些地方容易出现幻觉、假证明和不可复现的结果。如果你关心 AI 数学推理、自动定理证明、Lean 形式化验证或者只是想知道“现在 AI 到底能不能做数学研究”这篇可以直接收藏。1. AI 数学推理核心能力速览先把大家最关心的能力项列出来。这里不针对某个具体开源项目而是综合当前常见技术路线整理成一张可对照的速查表。能力项说明研究对象Erdős 问题以及其它数学未解问题、竞赛题、组合反例搜索常见 AI 方法大语言模型生成候选猜想、强化学习搜索证明路径、形式化证明器验证关键数学基础设施Lean、Coq 等证明助手SMT 求解器暴力和枚举脚本硬件门槛使用 API 方案时无需本地 GPU本地微调或推理需按模型规模准备显卡显存占用需实测启动方式API 调用 / Python 脚本 / Lean 工具链 / 本地模型推理是否支持批量任务支持可批量生成候选思路批量验证批量搜反例输出可靠性单独依赖大模型输出不可靠必须配合形式化或程序化验证适合场景数学研究辅助、猜想筛选、反例搜索、证明思路探索、教学演示不适合场景直接把模型输出当作正式证明、忽视授权和学术规范的生搬硬套从表格能看到这不是“一个模型解决所有问题”而是“生成器 验证器 搜索器”的工程闭环。理解这一点后面所有内容都好接了。2. 为什么传奇的 Erdős 问题会落到 AI 手里2.1 Erdős 问题为什么难很多 Erdős 问题难就难在“没有路标”。它们通常是大量小条件叠加在一起给定一个看似简单的集合或图要求你证明存在某种结构或者反过来证明不存在。这类问题的共同点是搜索空间巨大但局部规律非常稀疏。过去数学家解决这类问题依赖的是两个能力一是对已有定理的深刻理解二是针对具体问题的“手感”。手脚麻利的数学家可以在几十个特殊情形里试错凭经验知道哪些方向会碰壁。但这种经验通常是私有的、碎片化的很难迁移。AI 介入之后这套逻辑发生了变化。大模型可以从海量论文和题目里提取“这种结构之前在哪里出现过”快速生成候选方向程序化搜索可以在一秒内枚举人工需要几天的特殊情况形式化工具则能把“看起来对”的证明转成机器可检查的严格推导。2.2 大模型解决的是“从哪个方向试”大模型不是直接写出最终证明。它更擅长的是面对一个陌生问题时给出一个可能成立的中间引理、一个构造性想法或者一个值得验证的小规模例子。举个例子如果题目问“是否存在一组正整数使得任意两个数之差的绝对值都是合数”模型可能会说“先看连续区间里筛掉素数间隔的结构”。这个想法不一定对但确实缩小了搜索范围。接下来用程序枚举小规模情形把结果不符合的假设删掉保留还能继续的假设。这就是“AI 推动 Erdős 问题”的第一层原因搜索方向的初筛成本被大幅降低。2.3 形式化验证让“猜想”变成“可执行语句”光靠“想”不够。过去论文审稿人要花大量时间检查推理链现在用 Lean、Coq 这类证明助手可以把数学命题写成形式化语句机器逐行检查。一旦证明脚本通过几乎不存在“隐藏假设讲不清”的问题。AI 和形式化验证结合后流程变成大模型输出一个候选证明思路人将思路拆成若干步用证明助手逐步实现某些步骤如果太繁琐可以交给大模型生成证明助手报错人就根据报错修正或放弃该思路。这不是“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 软件清单组件用途Python 3.9 及以上编写调用脚本和暴力枚举脚本requests 或 openai SDK调用大模型 API也可使用本地模型服务Lean 4 / Coq形式化验证候选证明可选本地显卡与 CUDA仅当本地运行大模型时需要代码编辑器首选 VS Code配合 Lean 插件体验较好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 requests4.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_KEYyour-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: fBearer {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, jsonpayload, headersheaders, timeout60) 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_numnorm_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, temperature0.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, retries3): for i in range(retries): try: return ask_model(prompt) except Exception as e: print(f第{i1}次失败: {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. 常见问题与排查方法下面把最容易遇到的问题整理成排查表。问题现象可能原因排查方式解决方案模型输出与题目无关prompt 太模糊缺少上下文检查 prompt 中是否明确给出定义、条件和目标增加 few-shot 示例要求输出具体结构模型输出看似合理但验证失败模型幻觉中间结论无依据把输出拆成小步骤单独验证每步只保留能通过程序验证的部分重新迭代API 调用超时请求太长接口负载高查看日志中的耗时和错误码缩短 max_tokens增加重试批量任务卡住没有限流服务端拒绝查看任务列表状态增加 sleep设置最大重试次数Lean 报错目标未关闭证明步骤缺失或语法错误查看 Lean 信息窗口的当前目标用更原子化的引理逐步证明本地模型显存不足模型量级超过显存运行nvidia-smi观察占用换量化版本减小 batch缩减上下文结果不可复现采样温度过高固定随机种子或 temperature0设置模型参数保留日志验证脚本解析失败模型输出格式不符合预期打印原始输出prompt 中强制要求 JSON 或数组格式9. 最佳实践与使用建议9.1 把 AI 当作“猜想加速器”正式结论必须由验证器或人工证明确认。AI 的价值在于扩大搜索范围降低试错成本。不要因为模型给出了“看起来严谨”的证明就直接采用。9.2 保留完整的实验记录对于每一个问题建议维护一条记录包含问题编号和完整表述使用的模型名称、版本、温度、promptAI 输出全文或摘要验证脚本和运行结果最终结论通过 / 失败 / 待进一步验证。这样可以复现实验也能避免重复提问。9.3 小问题先跑通第一次做 AI 数学推理不要一上来就进军几十年的未解问题。从一个可以暴力枚举的小型组合问题开始让模型生成候选程序验证跑通后再逐步提高难度。9.4 注重版权与学术诚信使用 AI 辅助研究时如果使用了第三方论文、代码或私有数据必须先确认授权。在论文中如实说明 AI 使用情况。不发布无法验证的证明不把其他研究者的未发表思路搬进自己的结论里。9.5 接口服务要控制访问范围如果自己搭建 API 服务建议设置访问令牌、限速、日志记录。避免把服务直接暴露在不安全网络环境防止批量调用导致资源耗尽。10. 总结与下一步Erdős 问题被 AI 攻克本质不是一个模型单打独斗而是“大模型猜方向、程序验证结果、证明助手查逻辑”的工程体系越来越成熟。对普通人来说最有价值的不是等着新成果发布而是立刻用这套流程跑通一个小问题。建议先做三件事装好 Python 环境跑通一个简单的模型对话请求选一个可以暴力枚举的小型数论题让模型生成候选构造用脚本或 Lean 验证模型输出记录一份“生成-验证”实验日志。最容易踩的坑是把大模型的输出直接当成答案。只要你坚持“先验证后采信”这套方法论就是安全且有效的。接下来如果你想深入可以直接学 Lean 4尝试把一个已知数论引理形式化。这不是为了立刻解决大问题而是为了理解机器验证的价值。等你习惯了这种节奏再回头看那些传奇的 Erdős 问题就会明白为什么 AI 开始一个个撬动它们了。