如果只看标题你可能会觉得这又是一条“AI无所不能”的科技新闻GPT-5.6和Fable联手解决了一道悬了25年的数学难题。但如果你一直在关注大模型和定理证明器的发展真正值得注意的并不是“AI能做题了”而是这一条链路大模型负责“猜”形式化证明工具负责“证”。猜错可以证错不行。这才是这两年AI辅助数学研究里最重要的变化。本文不打算对“GPT-5.6和Fable解决25年难题”这则消息做真伪认定而是想借这个引子把技术组合拆开讲清楚为什么单靠大模型无法给出可信证明形式化验证在中间扮演什么角色普通人能不能自己把“大模型生成证明 验证器校验”这个闭环跑通如果你正准备尝试用LLM辅助数学证明或者想知道Lean、Coq这类定理证明器到底怎么接入AI工作流这篇文章会给你一个可以直接上手的最小实现。1. 为什么“AI解数学难题”总是被质疑过去几年大模型在数学题上的表现并不差。尤其在“AMC”“AIME”这类竞赛题上模型已经能给出不错的解题步骤。但数学家和工程师仍然普遍持怀疑态度原因很简单大模型给出的证明人类很难逐行验证而且它自己经常“一本正经地胡说八道”。这个问题在解决“悬了25年的难题”时会被无限放大。长期未解决的数学问题通常有几种特征涉及的构造非常长人工检查成本高。需要在大量分支中做情况分析很容易漏掉某个边界条件。证明过程依赖前人结果引用链极长某个环节出错会让整个证明失效。即使结果是正确的自然语言写出的证明也可能因为表述含糊导致无法复现。换句话说如果单纯让大模型输出一段自然语言证明哪怕它写得再有道理我们也没法确定这段话是不是“看起来正确”。数学证明需要的不是“可信度”而是“确定性”。大模型在这方面的天然劣势正是它不受数学家信任的原因。所以当我们听到“GPT-5.6和Fable联手解决数学难题”时重点不应该落在“GPT-5.6变强了”而应该落在“它不再需要人类去逐行验证它的结论因为Fable这类验证器替人做了这件事”。2. GPT-5.6和Fable一个负责“猜”一个负责“证”从材料看GPT-5.6更可能指代新一代具备更强推理能力的大语言模型而Fable在这里更像是一个形式化证明工具或协作框架的代称。具体实现可能不是唯一的但技术分工非常有代表性。大模型的角色是“直觉引擎”。它能根据问题描述生成一个可能的证明方向把复杂的推理拆成小步写出形式化语句。它也很擅长做“类比”比如看到某个结构与某个已知引理相似就会尝试把引理套进去。但问题是它的每一步输出本质上都是概率预测没有真正的逻辑保证。形式化工具的角色是“正确性引擎”。它会把证明变成一种可被机器检查的符号运算。就像编译器检查类型一样验证器会逐条检查每个推理步骤是否合法。如果推理错了工具会报错并且告诉你具体哪一行出了问题。它不会因为“这个思路看起来没问题”就放行。两者结合后工作流就变成了这样大模型根据数学命题生成一段Lean/Coq代码试图搭建证明框架。形式化工具接收这段代码并进行机械验证。如果验证失败工具把错误信息返回给大模型。大模型读入错误信息调整策略重新生成代码。重复该循环直到验证通过。在这个过程中大模型可以犯无数次错误因为错误会被验证器拦截。最终被接受的证明是经过机械检查的而不是“大模型觉得自己对了”。角色擅长不擅长最终产出GPT-5.6大模型产生思路、编写形式化代码、根据错误反馈修改保证每一步推理绝对正确可提交的证明草稿Fable验证器检查推理步骤、定位错误、保证证明可复现主动生成复杂证明思路通过验证的证明文件所以真正的“主角”其实不是单独哪一个而是这套“猜—证—反馈—再猜”的闭环。3. 基础概念从自然语言证明到形式化证明要理解这个组合必须先理解什么是“形式化证明”。在传统数学中证明是用自然语言写的。比如“因为A成立且A能推出B所以B成立”。这种写法人类能看懂但机器很难验证。语言歧义、隐含假设、逻辑跳跃都会让机器无法判断对错。即便由人类审稿也很容易出现评审意见不一致的情况。形式化证明则不同。它会用严格的逻辑语言把命题和推理步骤全部表达出来。你可以把它想成是“数学证明的编程语言”。在Lean 4、Coq、Isabelle这类定理证明器中命题本身就是一个表达式证明就是构造一个满足该表达式的对象。这句话背后的核心是一个叫做“Curry-Howard对应”的思想证明即程序命题即类型。如果我们要证明一个命题 P实际就是构造一个类型为 P 的程序。验证器会检查这个程序是否真的符合 P 的类型。如果检查通过那么证明就是正确的不需要人类再逐行阅读。举个例子在Lean 4中自然数加法结合律可以写成import Mathlib theorem add_assoc_example (a b c : Nat) : (a b) c a (b c) : by ring这段代码的意思是对于任意自然数 a、b、c(a b) c等于a (b c)。ring是一个智能策略它知道自然数加法的基本性质能够自动完成证明。这就是形式化工具的价值所在。它不关心你的证明“看起来像不像数学”它只关心你的每一步变换是否有据可循。哪怕你自己都不知道为什么能成立只要验证器接受它就是可复现的事实。而大模型在其中做的事就是生成这类形式化代码。它不需要直接编写人类可读的论文式证明而是编写机器可读的证明脚本。在这个脚本里一切歧义都被消除。4. 环境准备与前置条件要跑通“大模型生成证明 验证器校验”的最小闭环我们需要准备以下环境操作系统Linux、macOS或WSL均可Windows原生环境建议使用WSL。Python 3.10。Lean 4与Lake构建工具。一个可用的LLM API本地运行或云端API均可。文本编辑器推荐VS Code并安装Lean4插件。Lean 4的安装方式在官方文档中维护得比较及时最常用的方法是通过elan作为版本管理工具。这里给出一个大致流程具体版本号以官方文档为准# 1. 安装 elanLean 版本管理工具 # 参考官方文档https://lean-lang.org/ curl -sL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh bash elan-init.sh # 2. 安装 stable 工具链 elan toolchain install stable # 3. 初始化一个新的 Lean 项目 lake new demo_proof cd demo_proof # 4. 将 Mathlib 添加到依赖示例 # lakefile.toml 中配置依赖或使用 lake update安装完成后确认版本lean --version lake --version如果Lean和Lake都能正常输出版本号说明环境已经可用。对于大模型部分我们接下来会用Python写一个最简单的调用脚本。为了不依赖某个具体厂商SDK我使用OpenAI兼容接口的方式。只要你的模型服务提供/chat/completions接口都可以复用这个套路。5. 完整示例从“猜”到“证”的最小闭环这一节我们做一个最简实践让大模型生成“自然数加法结合律”的Lean证明然后用Lean验证器去检查它是否正确。如果验证失败我们再把错误信息回传给大模型让它修改直到通过。5.1 在Lean中建立项目骨架先创建一个最小Lean项目。在项目目录下打开lakefile.toml确保包含Mathlib依赖。如果你使用lake new demo_proof生成的模板通常已经有默认配置只需再执行lake update即可拉取依赖。然后在demo_proof/目录下新建文件Proof/Basic.lean写入我们需要验证的命题import Mathlib theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by ring这个文件暂时还不能证明任何难题只是一个用来验证“验证器能不能跑通”的最小例子。5.2 编写Python脚本调用LLM生成Lean代码接下来我们写一个Python脚本它负责两件事调用大模型接口让模型生成一段Lean证明。把生成的代码写入临时Lean文件然后调用lean命令检查它是否能通过。为了不把API Key硬编码在代码里我们通过环境变量读取。# 文件路径scripts/llm_lean_demo.py import os import re import subprocess import requests API_KEY os.environ[LLM_API_KEY] BASE_URL os.environ.get(LLM_BASE_URL, https://api.openai.com/v1) MODEL os.environ.get(LLM_MODEL, gpt-4o) def extract_lean_code(raw_output: str) - str: 从模型输出中提取Lean代码块如果不在代码块中则原样返回。 pattern rlean\n(.*?) matches re.findall(pattern, raw_output, re.DOTALL) if matches: return matches[-1].strip() return raw_output.strip() def generate_lean_proof(statement: str) - str: 让大模型生成Lean证明。 prompt ( 请用Lean4语言证明下面的数学命题。\n 只输出Lean代码不要输出任何解释。\n lean\n f命题{statement}\n \n ) resp requests.post( f{BASE_URL}/chat/completions, headers{Authorization: fBearer {API_KEY}}, json{ model: MODEL, messages: [ {role: system, content: 你是一个擅长Lean4形式化证明的助手。}, {role: user, content: prompt}, ], temperature: 0.2, }, timeout120, ) resp.raise_for_status() return extract_lean_code(resp.json()[choices][0][message][content]) def verify_lean(source: str, project_dir: str) - tuple[bool, str]: 调用Lean验证代码返回(是否通过, 错误信息)。 tmp_file os.path.join(project_dir, Proof, Generated.lean) with open(tmp_file, w, encodingutf-8) as f: f.write(source) result subprocess.run( [lake, env, lean, tmp_file], cwdproject_dir, capture_outputTrue, textTrue, timeout120, ) if result.returncode 0: return True, return False, result.stderr这里有一个容易被忽略的点使用lake env lean而不是直接使用lean。原因是这样能够正确加载Mathlib依赖同时避免“找不到import”的问题。5.3 加入错误反馈循环单次生成大概率不会一次通过尤其是面对更复杂的命题。我们需要把验证器的错误信息作为新的上下文喂给大模型让它自己修改。# 文件路径scripts/llm_lean_demo.py def solve_with_llm(statement: str, project_dir: str, max_attempts: int 5) - str: messages [ {role: system, content: 你是一个擅长Lean4形式化证明的助手。}, {role: user, content: f证明这个命题{statement}\n只输出Lean代码。}, ] for i in range(max_attempts): resp requests.post( f{BASE_URL}/chat/completions, headers{Authorization: fBearer {API_KEY}}, json{model: MODEL, messages: messages, temperature: 0.2}, timeout120, ) resp.raise_for_status() code extract_lean_code(resp.json()[choices][0][message][content]) ok, error verify_lean(code, project_dir) if ok: print(f第 {i 1} 次尝试通过验证) return code print(f第 {i 1} 次尝试未通过错误信息\n{error[:500]}) messages.append({role: assistant, content: code}) messages.append({role: user, content: f验证失败请修改。错误信息\n{error[:2000]}}) raise RuntimeError(达到最大尝试次数仍未通过验证) if __name__ __main__: theorem_statement 对于任意自然数 a b c有 (a b) c a (b c) project_dir ../demo_proof proof solve_with_llm(theorem_statement, project_dir) print(最终通过的证明\n) print(proof)这个循环看起来很简单但它就是“GPT-5.6 Fable”这类协作终态的微型版本。大模型出错不可怕验证器会给出精确的错误位置模型再针对错误修改。只要错误反馈足够清晰这个问题就能被逐步压缩到可解决范围。5.4 用CI自动验证证明在真实项目中你不会只把证明跑在自己电脑上。更好的方式是把生成的证明提交到Git仓库然后通过CI自动验证保证后续修改不会破坏已有证明。一个常见的GitHub Actions配置如下# 文件路径.github/workflows/proof-check.yml name: proof-check on: pull_request: paths: - demo_proof/** jobs: check: runs-on: ubuntu-latest steps: - uses: actions/checkoutv4 - name: Install Lean toolchain run: | curl -sL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh bash elan-init.sh elan toolchain install stable - name: Run lean check working-directory: demo_proof run: | lake env lean Proof/Basic.lean lake env lean Proof/Generated.lean这样的配置可以让你在提交证明时自动运行验证。如果大模型后续又改了代码任何一条证明失败都会让CI变红在合并之前暴露问题。6. 运行结果与效果验证现在运行脚本观察输出。export LLM_API_KEY你的API Key export LLM_MODEL你使用的模型名称 python scripts/llm_lean_demo.py预期可能会看到类似下面的输出第 1 次尝试未通过错误信息 (demo_proof/Proof/Generated.lean:3:10) error: invalid type ascription, term has type a b c a (b c) but is expected to have type (a b) c a (b c)这个错误说明大模型可能把命题里的括号漏了或者使用了已经存在的定理名。随后它会在下一次尝试中修正。最终成功时输出会是这样第 3 次尝试通过验证 最终通过的证明 import Mathlib theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by ring判断成功的关键点是lake env lean Generated.lean退出码为0。终端没有打印任何错误。生成的证明文件可以被Lean正常加载。如果验证失败第一步不要去看大模型“为什么写错了”而应该先看Lean给出的错误信息和位置。验证器的错误信息通常很精确能定位到具体哪一行、哪一个表达式不匹配。7. 常见问题与排查思路在实际运行过程中新手最容易遇到的几类问题如下。问题现象可能原因排查方式解决方案elan安装失败网络或权限问题查看安装脚本输出使用管理员权限执行或去官方文档查看镜像方式lake env lean找不到import MathlibMathlib尚未下载或版本老旧执行lake update后重试更新依赖后重新验证大模型返回的代码是自然语言而不是Lean代码提示词不够明确检查extract_lean_code是否只提取代码块在提示词中明确“只输出Lean代码”并让提取逻辑兼容无代码块情况验证器报invalid type ascription大模型生成的命题类型与目标不一致对照命题原文检查括号和类型把目标命题直接写入 prompt 原文不要依赖模型记忆验证器超时证明策略太慢或循环过多查看Lea输出是否卡在某个策略拆成多个小引理降低单步证明复杂度API请求失败Key过期、额度不足或接口地址错误检查环境变量和HTTP错误码换成正确的端点或Key模型不断在同一个错误上循环错误反馈不够具体或提示词缺少上下文把完整stderr拼入错误信息截取错误信息末尾2000字符并保留最近几轮对话8. 最佳实践与工程建议真正要把“大模型形式化验证”用到数学研究或工程验证中建议遵循下面这组实践。第一永远把验证器当作最终裁判。大模型生成的证明无论多么“像回事”都必须先通过验证器。不要因为模型自信就跳过验证。尤其在网络讨论中看到类似“解决25年数学难题”的案例时更要注意如果证明没有经过可复现的形式化验证它就只能算作“候选结果”。第二尽量把大问题拆成小引理。大模型一次生成很长的证明很容易出现深层错误。但如果把证明拆成几十个小引理每个引理都短小、清晰验证器报错时也能更快定位。研究者通常会先用自然语言构思整体框架再逐个让大模型形式化每个引理。第三为每个生成结果保留元数据。记录模型名称、温度、随机种子、提示词版本、验证器版本和错误反馈历史。原因很简单LLM生成结果是随机性的同一个问题跑两次可能得到不同证明。如果没有记录后续很难复现“那次成功的证明”。第四控制API成本。每次验证失败都会消耗一次调用。如果问题很复杂可以先用一个小模型做粗筛再让更强模型做最终修正。也可以把历史成功证明缓存到本地避免反复生成相同引理。第五注意安全边界。在真实项目中不要把API Key提交到Git仓库。无论是本地运行还是CI都应该使用密钥管理服务或环境变量。如果模型提供了受信任代码生成能力验证后的代码仍然需要走正常的代码评审和测试流程不要因为“验证器通过”就直接执行到生产环境。第六对网传结果保持怀疑。数学史上有很多声称证明了自己猜想的新闻后来在形式化验证阶段被否决。当你看到“GPT-5.6和Fable联手解决难题”这类消息时第一件该做的事不是转发而是去找是否有公开的验证脚本、证明文件和可复现环境。没有这些它就只是一个“AI的猜想”而不是“数学上的定理”。9. 总结与后续学习方向“大模型生成思路验证器保证正确”这个模式确实是当前AI辅助数学研究最值得关注的方向之一。GPT-5.6这样的推理模型负责把人的直觉转成形式化脚本Fable这类验证工具负责把脚本变成机器可检查的证明记录。两者结合解决了一道悬了25年的数学难题看起来像是奇迹实际上背后是一条非常工程化的流程形成猜想。用大模型生成候选证明。用验证器机械地检查。根据错误信息迭代修复。保留可复现的证明文件和验证环境。对普通开发者来说不需要去直接解决数学难题也可以从今天这个最小示例开始把Lean 4跑起来再写一个Python脚本接入你手头的LLM API让模型帮你生成并验证一个简单定理。等你熟悉了错误反馈循环再逐步挑战更复杂的引理和实际问题。下一步建议按这个顺序深入熟悉Lean 4基础语法与infertactic至少能看懂策略代码。尝试用大模型证明一个你本来就会的简单定理先体会“验证失败—修改—通过”的循环。学习lake项目结构理解多文件依赖和Mathlib的管理方式。去了解著名的数学形式化项目比如液体张量实验和完美数问题观察社区如何组织大规模证明。数学研究正在从“同行评审式证明”转向“机器验证式证明”。大模型的出现只是加快了这个过程。真正让25年难题落下帷幕的不是模型读完题后给出的漂亮答案而是那道答案最终被一台不讲情面的验证器逐行接受。建议你先收藏本文然后用一个最小例子把这条链路跑通再回去看新闻你的判断会完全不同。