近几天技术社区里讨论最多的话题之一是“GPT-5.6 和 Fable 联手解决了一道悬了 25 年的数学难题”这则消息。由于公开细节还不完整这里不猜测难题本身也不对两个产品下结论而是把它当成一个更好的技术问题的起点大模型生成数学证明形式化验证器负责检查证明两者之间的错误反馈循环是否真的能跑通为了验证这件事我搭建了一套最小可复现环境用 Python 脚本扮演 Fable 的编排角色让大模型生成 Lean 4 证明片段再让 Lean 编译检查。这套链路完成之后你会看到“生成、验证、反馈、重试”的完整闭环也能理解为什么这项技术有潜力处理那些长期悬而未决的数学问题。1. 先理解 GPT-5.6 与 Fable 的协作点是什么标题里有三个关键词GPT-5.6、Fable、数学难题。要理解这次“联手”的价值需要先分清两个角色各自擅长什么以及它们为什么必须配合。1.1 大模型负责“猜”不负责“证明”大模型本质上是一个基于海量文本训练出来的概率语言模型。它擅长从上下文里预测下一个 token所以当它面对一个数学命题时能够给出看起来很像证明的推理链。比如让它证明“自然数乘法满足交换律”它可以写出“先对左边进行化简再利用乘法交换律”这样的文字描述甚至直接给出 Lean 代码片段。问题在于大模型的“看起来合理”和数学的“严格正确”不是一回事。模型在长链条推理中很容易出现幻觉少一个条件、跳一步变形、错误地使用某个引理甚至编造一个不存在的定理。对于简单命题错误很容易被肉眼发现但对于真正悬了 25 年的难题证明可能包含数百页逻辑推导和大量自定义抽象任何一个隐蔽错误都会让整条证明作废。所以大模型适合承担“猜”的工作提出证明方向、补全某个局部推导、给出引理候选。它不适合作为最终裁判。1.2 形式化验证器负责“查”不负责“猜”Lean 4 是一种交互式定理证明器它最大的特点是“内核验证”。写进 Lean 的每条定理、每个证明步骤最终都会被简化成一个极小的逻辑内核逐层检查。只要 Lean 接受了一个定理就意味着在给定数学库的公理和定义下这个定理在逻辑上是成立的。这种严格性是纯大模型输出不具备的。但验证器也有明显短板它不能自动替你想出证明方案。面对a * b * c a * (b * c)这种简单命题你可以用ring一条策略解决面对一个复杂的组合数学猜想验证器只会对着目标等待你给出足够多的引理和步骤。它不知道下一步该引入哪个中间量也不知道该对哪一部分做归纳。换句话说验证器“查”的能力很强“猜”的能力很弱。1.3 把两者串起来的闭环如果让大模型负责生成证明候选让验证器负责检查再把验证器报出的错误原样返回给大模型让模型根据错误修改证明就形成了下面这个闭环Fable 从任务文件中读取定理陈述。Fable 调用大模型 API要求模型补齐: by后面的证明代码。Fable 将模型输出拼成一个完整的.lean文件。使用lake env lean编译该文件。如果编译通过记录“已验证”结果。如果编译失败把 Lean 输出的错误信息拼回对话上下文让大模型再试一次。这套闭环的价值在于模型可以继续发挥它在自然语言和数学直觉上的优势而验证器从机制上兜住了模型幻觉的底。这正是在真实数学研究中使用 AI 辅助证明的基本范式。2. 环境准备安装 Lean 4 与 Mathlib下面开始搭建可复现环境。我会以 Lean 4 作为验证器因为它在数学界和计算机科学界都有比较活跃的社区Mathlib4 数学库覆盖了大量现代数学内容。大模型部分使用 OpenAI 兼容接口实际模型名以你账号可用模型为准示例中沿用标题里的 GPT-5.6 只是为了让讨论一致。2.1 目标环境与版本说明组件作用建议版本或方式elanLean 的工具链管理器类似 Node 的 nvm使用官方安装脚本Lean 4交互式定理证明器通过 elan 安装 stable 工具链Mathlib4Lean 的数学核心库通过 Lake 引入Python 3编写 Fable 编排脚本3.10 及以上openai 库调用大模型 APIpip install openai大模型 API生成候选证明以实际可用模型为准Lean 工具链版本变化很快落地前建议先查询 Lean 社区官方仓库的稳定版本。不同版本之间的 API 和数学库结构可能不同不要直接照搬旧教程。2.2 安装 elan 与 Lean 4在 Linux 或 macOS 终端执行curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh安装完成后重新加载 shell 配置source ~/.profile确认 elan 和 lean 命令存在elan --version lean --version如果 lean 命令不在 PATH 中可以检查~/.elan/bin是否被加入 PATH。后续所有 Lean 命令建议通过lake env执行这样才能正确加载项目依赖。2.3 新建 Lean 项目并引入 Mathlib使用 Lake 创建新项目lake new math_solver cd math_solver编辑lakefile.toml添加 Mathlib 依赖[[require]] name mathlib git https://github.com/leanprover-community/mathlib4.git rev v4.7.0rev字段建议改为当前官方稳定版本可以从 Mathlib4 的 GitHub 仓库主页获取。然后同步依赖lake update mathlib首次构建 Mathlib 会花很长时间因为它需要编译大量数学定义和定理。这个过程不是卡死耐心等待即可。构建完成后运行lake build这一步会确保项目里的依赖和配置没有基础错误。2.4 验证 Lean 环境在项目根目录创建Test.leanimport Mathlib example (p q : Prop) : p - q - p : by intro hp hq exact hp运行lake env lean Test.lean如果终端没有任何输出说明证明通过。这里用到的是import Mathlib让 Lean 能解析 Mathlib 里的标准库定义。intro hp hq引入两个前提exact hp告诉验证器结论就是前提p。注意lake env lean必须在 Lean 项目目录内运行否则它无法找到lakefile.toml和 Mathlib 依赖。3. 实现 Fable让 Python 调用大模型并交给 Lean 检查环境准备好之后写一个 Python 脚本模拟 Fable 的编排逻辑。这个脚本会完成三件事调用大模型生成证明、调用 Lean 检查证明、把错误反馈返回给模型重试。3.1 项目结构在math_solver项目目录下增加两个文件math_solver/ ├── lakefile.toml ├── Test.lean ├── fable_solver.py └── task.jsontask.json用于描述要证明的定理这样脚本可以复用不需要每次在代码里修改命题。3.2 定义证明任务格式创建task.json{ name: example_imp, statement: example (p q : Prop) : p - q - p, max_attempts: 3 }statement只写到: by之前。完整的 Lean 代码会由脚本拼接成import Mathlib example (p q : Prop) : p - q - p : by intro hp hq exact hpmax_attempts表示大模型最多可以拿反馈重试几次。设置太小容易失败设置太大则会增加 API 费用和等待时间。3.3 Python 封装调用大模型 API编写fable_solver.pyimport os import re import subprocess import tempfile from pathlib import Path from openai import OpenAI class Fable: def __init__(self, model: str, lean_project: str .): self.client OpenAI(api_keyos.environ[OPENAI_API_KEY]) self.model model self.lean_project Path(lean_project) def _call_llm(self, messages: list[dict]) - str: response self.client.chat.completions.create( modelself.model, messagesmessages, temperature0.2, max_tokens1024, ) return response.choices[0].message.content or def _extract_proof(self, raw: str) - str: # 去掉常见的 markdown 代码块标记 raw re.sub(r(?:lean)?, , raw) raw raw.replace(, ).strip() if raw.startswith(by): raw raw[2:].strip() return raw def _build_lean_code(self, statement: str, proof: str) - str: indented proof.replace(\n, \n ) return fimport Mathlib\n\n{statement} : by\n {indented}\n def _check_lean(self, code: str) - str: with tempfile.NamedTemporaryFile( w, suffix.lean, deleteFalse, dirself.lean_project, encodingutf-8, ) as f: f.write(code) file_path Path(f.name) try: proc subprocess.run( [lake, env, lean, file_path.name], cwdself.lean_project, capture_outputTrue, textTrue, timeout120, ) return proc.stdout proc.stderr finally: file_path.unlink(missing_okTrue) def prove(self, statement: str, max_attempts: int 3) - dict: messages [ { role: system, content: You write Lean 4 proofs., }, { role: user, content: ( fStatement:\n{statement} : by\n\n Complete the proof after : by.\n Return only Lean code, no explanations, no markdown.\n Do NOT use sorry, admit, or axioms. ), }, ] last_output for attempt in range(1, max_attempts 1): raw self._call_llm(messages) proof self._extract_proof(raw) if re.search(r\bsorry\b, proof) or re.search(r\badmit\b, proof): feedback ( The proof contains sorry or admit, which is not allowed. Rewrite the proof without them. ) messages.append({role: assistant, content: raw}) messages.append({role: user, content: feedback}) continue full_code self._build_lean_code(statement, proof) output self._check_lean(full_code) last_output output # Lean 中 sorry 会产生 warning 但退出码仍可能是 0 # 所以这里把 sorry、error、unsolved 都视为失败。 if ( error not in output.lower() and unsolved not in output.lower() and sorry not in output.lower() ): return { status: verified, attempt: attempt, proof: proof, } feedback Lean reported the following errors:\n output messages.append({role: assistant, content: raw}) messages.append({role: user, content: feedback}) return { status: failed, attempts: max_attempts, last_output: last_output, }运行前确保安装依赖pip install openai export OPENAI_API_KEY你的密钥3.4 关键参数与设计原因参数推荐值说明temperature0.2数值越低输出越稳定适合生成需要严谨语法的证明代码max_tokens1024大部分单步证明不会超过这个长度timeout120Lean 编译复杂证明可能较慢需要给足时间max_attempts3 到 5重试太多会显著增加 API 成本和等待时间model以实际可用模型为准示例中可写gpt-5.6生产环境要换成账号真实可调用的模型名这里有一个容易被忽略的坑脚本检查的是output中是否包含error、unsolved和sorry。为什么sorry也要算失败因为在 Lean 里sorry可以作为占位符让文件通过编译但它并没有给出真正的证明。如果模型输出的证明里偷偷带了sorry只检查退出码会误判成“验证通过”所以必须在代码和输出里都做关键词拦截。3.5 运行任务创建run.py或直接在交互式命令行中执行import json from fable_solver import Fable with open(task.json, encodingutf-8) as f: task json.load(f) fable Fable(modelgpt-5.6, lean_project.) result fable.prove(task[statement], task[max_attempts]) print(json.dumps(result, ensure_asciiFalse, indent2))如果一切正常你会看到类似这样的输出{ status: verified, attempt: 1, proof: intro hp hq\n exact hp }证明p - q - p本身很简单但这条链路的意义不在命题难度而在于它验证了“模型生成证明、验证器严格把关”这个机制是可行的。真实难题只是把同样的链路放大更多的引理、更长的反馈、更复杂的搜索策略。4. 从最小案例到真实难题工作流设计上的关键差异最小案例容易跑通真正悬了 25 年的数学难题则要复杂得多。如果你把这套脚本直接扔给一个数论猜想大概率会在第三步就失败因为模型不可能靠一个 prompt 生成几百页的证明。缩短模型现有能力与真实难题之间差距的关键是工作流设计。4.1 真实难题需要拆题而不是直接整体证明拿到一个复杂定理后Fable 的职责不能只是“调用 API 然后检查”而应该先做任务分解。例如把目标定理拆成若干引理每个引理单独交给一次模型调用最后再用一个组合引理把所有子结果拼起来。拆题本身就是一种数学能力它决定整个搜索空间的大小。任务粒度适合场景风险单条策略证明ring、omega能处理的简单等式无法覆盖复杂定理补全一个引理的证明定理已经有明确陈述需要构造证明模型可能生成错误策略提出一个有价值的中间引理需要模型发挥数学直觉引理本身可能不成立需要验证器筛选根据错误反馈修补证明证明的大部分正确只有局部错误反馈过长时模型容易丢失上下文4.2 错误反馈的质量决定重试效果模型的第二次尝试效果很大程度上取决于第一次失败时拿到了什么错误信息。Lean 的错误信息通常包含行号、目标状态和错误类型。把这些信息原样返回给模型比只丢一句“证明错误”有效得多。一个合理的反馈结构是Lean reported the following errors: 输出文件:行号: error: unsolved goals ... 请根据错误修正证明并只输出 Lean 代码。如果错误信息太长超过模型上下文窗口就要做摘要或只保留最近一部分错误。否则模型会在大量文本里失去重点。4.3 模型负责假设验证器负责淘汰在数学研究中很多新定理的证明方向最初只是假设。大模型可以快速列举“如果出现某个中间命题原题就可以成立”这类候选结构。Fable 的职责是用验证器快速淘汰错误假设保留能通过检查的片段。这项工作很像单元测试驱动开发模型写一个候选片段Lean 当测试框架通过就保留失败就反馈。循环往复最终得到可正式使用的证明模块。这也是“AI 辅助数学”最现实的落地方式它不是替代数学家而是加速从猜想到验证的反馈周期。5. 常见问题与排错路径把环境搭起来、把脚本跑起来只是开始。实际使用中会遇到不少问题下面按环境、模型输出和验证结果三个维度整理排查思路。5.1 环境类问题问题现象常见原因处理建议lake env lean: command not foundelan 安装后没有刷新 PATH执行source ~/.profile或确认~/.elan/bin在 PATH 中import Mathlib报错项目没有正确声明 Mathlib 依赖检查lakefile.toml执行lake update mathlib首次构建耗时过长Mathlib 需要编译大量内容属于正常现象给足磁盘空间和等待时间lake找不到项目文件当前目录不在 Lean 项目内先cd math_solver再运行命令中文路径或文件名导致编译异常Lean 工具链对非 ASCII 路径支持不稳定将项目放到纯英文路径下5.2 模型输出类问题问题现象常见原因处理建议输出包含lean代码块模型默认按 markdown 回复在_extract_proof中清理代码块标记输出包含by开头模型误以为要补全整个表达式去掉开头的by只保留策略列表输出包含sorry或admit模型想快速占位在脚本关键词拦截并在结果中标记失败输出使用不存在的定理名模型对 Lean 数学库知识不完整把错误信息反馈回去仍失败则降低模型期望输出策略缩进错误Lean 对缩进敏感在_build_lean_code中对多行策略统一添加缩进5.3 验证结果误判这里的核心风险是“表面通过实际未证明”。Lean 对sorry的默认行为是产生 warning但文件编译仍会成功。因此只检查returncode是不够的。推荐的失败判断逻辑def is_success(output: str, code: str) - bool: blacklist [error, unsolved, sorry, admit, failed] lower_output output.lower() lower_code code.lower() return not any(word in lower_output or word in lower_code for word in blacklist)注意即使 Lean 显示success也只代表证明在所依赖的数学库定义下成立。如果底层定义有误或者你使用了自定义公理验证结果的有效性仍然需要人工审查。5.4 排查顺序清单遇到问题时按以下顺序排查可以减少无意义尝试先确认 Lean 环境运行lean --version和lake env lean Test.lean。再确认依赖lakefile.toml是否正确Mathlib 是否成功构建。然后确认输入task.json的 statement 是否合法是否缺了import Mathlib。接着确认模型输出打印原始输出看是否被 markdown 或自然语言污染。再看验证反馈Lean 错误里有没有具体行号错误是语法错误、目标未解决还是未知定理。最后调整策略降低temperature、增加max_attempts、缩小证明目标。6. 生产化与最佳实践如果只是个人实验一个 Python 脚本就够用。但如果要长期维护一套“AI 提示 形式化验证”的数学辅助系统还需要进一步工程化。6.1 从脚本到服务生产环境建议把 Fable 封装成 HTTP 服务提供几个标准接口POST /tasks提交待证明定理。GET /tasks/{id}查询验证状态和最终证明。POST /tasks/{id}/retry手动触发重试。同时增加缓存层。已经验证过的定理连同证明代码一起存进数据库或 Redis下次遇到相同命题直接返回结果不用再呼叫大模型。这能显著降低成本和等待时间。每次调用都需要记录日志至少包含模型名称和参数。输入定理。每次尝试的原始输出。Lean 的完整错误信息。最终验证状态。耗时和 token 消耗。有了这些日志才能定位是模型能力瓶颈、提示词问题还是数学库定义问题。6.2 可复用检查清单下面这份清单可以用在任何“大模型 验证器”协作场景检查项说明环境检查Lean 工具链、Mathlib、Python 依赖均已安装并验证输入规范定理陈述有明确类型签名不依赖不明确的公理代码拼接模型输出经过 markdown 清理、缩进修复和by前缀处理禁用词检查对sorry、admit、axiom等占位符做硬拦截验证不可跳过最终状态必须以验证器输出为准不能只看模型自信度错误反馈保留把 Lean 错误完整返回给下一轮模型尝试重试上限设置max_attempts避免无限调用日志完整每次尝试、每个错误、每个 token 消耗都要记录人工审查对于公开发布或论文结论必须有人工复核上下文定义6.3 安全与学术边界“大模型证明数学题”很容易被宣传成“人工智能独立解决难题”。在工程实践上不建议使用这种表述。真实情况是大模型提供了候选证明验证器完成了严格校验数学家设计了问题拆解方案。三者的贡献应当并列呈现。另外模型名称和版本会快速变化。今天文章里写的gpt-5.6到读者操作时可能已经不再可用也可能对应新的 API 结构。生产项目必须把模型名做成配置项不要硬编码。7. 扩展方向验证器足够强时模型可以成为猜想的发动机最后回到那道悬了 25 年的数学难题。如果大模型真的参与了解决它的价值并不在于某一次“灵光一现”而在于它可以海量提出证明方向和中间引理并快速淘汰错误路径。这个过程如果完全由数学家手工完成会消耗数年时间如果由大模型和验证器协作可能只需要几天。想在这个方向深入可以从几个角度继续扩展。一是让大模型直接提出新猜想而不仅仅补全证明只要猜想能被形式化验证器就能给出通过或不通过的结论。二是接入更强的自动化证明策略Lean 4 的omega、ring、linarith、aesop已经可以处理大量局部推导如果模型生成的策略恰好命中这些工具验证速度会快很多。三是设计更好的拆题算法让 Fable 能自动把一个大型定理拆成若干可独立验证的子命题并按依赖关系排序执行。对于想尝试这套技术栈的开发者建议不要从 25 年难题开始而是先从ring能处理的等式、omega能处理的整数不等式这类小命题开始。把“生成、验证、反馈、重试”这条链路跑熟再逐步引入更复杂的定理陈述、更大的数学库和更长上下文的模型。技术原理并不神秘真正困难的是把每一步都做成可靠的工程模块这才是 AI 辅助数学走向实用的关键。