1. 项目概述当大语言模型遇上形式化证明如果你是一位数学、计算机科学或形式化验证领域的研究者或开发者那么你很可能对“定理证明”这项工作既爱又恨。爱的是它带来的绝对严谨性恨的是其过程往往繁琐、枯燥需要投入巨大的心智和精力。传统的交互式定理证明器如 Coq、Isabelle 和 Lean虽然功能强大但陡峭的学习曲线和命令式的交互方式让许多潜在用户望而却步。近年来以 ChatGPT 为代表的大语言模型在代码生成和逻辑推理上展现出了惊人的潜力一个自然而然的想法是能否让 ChatGPT 来帮我们做定理证明这正是 LeanDojoChatGPT 项目试图回答的问题。简单来说它是一个为 ChatGPT 设计的插件让 ChatGPT 能够与 Lean 定理证明器进行交互从而辅助甚至自动化完成定理证明任务。其核心在于它并非让 ChatGPT 凭空“想象”出一个证明而是通过一个名为 LeanDojo 的中间层让 ChatGPT 能够像人类用户一样向 Lean 发送证明指令即“策略”并接收 Lean 的反馈如当前证明目标的状态、错误信息等在此基础上进行多轮推理和尝试最终完成证明。想象一下你不再需要逐行手动输入rewrite、apply、simp等策略而是可以用自然语言告诉 ChatGPT“我想证明这个关于自然数加法的交换律定理请先给我一个高层次证明计划然后尝试用归纳法来证。” 接下来ChatGPT 会理解你的意图通过 LeanDojo 与 Lean 交互执行具体的证明步骤并将过程反馈给你。这极大地降低了形式化证明的门槛也为探索大语言模型在严格逻辑推理任务上的能力提供了一个绝佳的试验场。这个项目源自论文《LeanDojo: Theorem Proving with Retrieval-Augmented Language Models》并在 NeurIPS 2023 上发表。它不仅仅是一个工具更是一个研究平台展示了如何将检索增强的语言模型与专业的证明环境相结合。对于数学爱好者、形式化方法工程师、以及 AI 与逻辑交叉领域的研究者来说LeanDojoChatGPT 提供了一个窥见未来“AI 协证”工作流的窗口。在本文中我将带你深入拆解这个项目的设计思路、搭建过程、核心玩法以及背后的原理并分享我在部署和实验过程中积累的一手经验和避坑指南。2. 核心架构与组件拆解要理解 LeanDojoChatGPT 如何工作我们需要将其分解为几个关键组件并厘清它们之间的协作关系。整个系统可以看作是一个“人用户- 大模型ChatGPT- 证明环境Lean”的协同循环。2.1 三大核心组件及其角色1. ChatGPT 与插件系统这是整个流程的“大脑”和交互界面。用户通过 ChatGPT 的 Web 界面或 API 与系统交互。ChatGPT 插件是一种扩展机制允许 ChatGPT 在对话中调用外部工具和服务。在本项目中插件的作用是让 ChatGPT 能够接收用户的证明请求并将请求转发给后端的 LeanDojo 服务同时将 LeanDojo 返回的证明状态和结果呈现给用户。ChatGPT 在这里扮演了“策略生成器”和“计划制定者”的角色它需要理解数学陈述规划证明步骤并生成正确的 Lean 策略代码。2. LeanDojo连接语言模型与 Lean 的桥梁这是项目的核心中间件也是其命名来源。LeanDojo 本身是一个独立的开源工具包它提供了与 Lean 证明环境进行程序化交互的能力。你可以把它想象成一个“机器人操作员”它能够启动和管理 Lean 进程加载特定的 Lean 项目代码库。执行策略接收来自外部的 Lean 策略命令如intro h将其发送给 Lean 进程执行。捕获和解析状态从 Lean 的输出中精确地提取当前的证明目标Goal、上下文中的假设Hypotheses、以及任何错误信息。提供检索功能这是论文中的重点LeanDojo 可以从庞大的数学库如 Mathlib中检索相关的定义、定理和证明片段为语言模型提供额外的上下文和提示从而增强其证明能力。在 ChatGPT 插件版本中这一检索功能被集成到后端服务中。3. Lean 定理证明器这是执行证明的“引擎”。Lean 是一个功能强大的依赖类型理论证明助手和编程语言。它接收策略严格地检查每一步的逻辑正确性并更新证明状态。Lean 的严格性是整个系统的基石它确保了 ChatGPT 生成的证明步骤最终能构成一个经得起机器检验的严谨证明。数据流与协作流程用户发起请求用户在 ChatGPT 界面输入自然语言指令例如“证明定理hello_world它在文件src/example.lean中”。ChatGPT 解析与规划ChatGPT 理解用户意图并可能先制定一个高层次的证明计划。插件调用后端ChatGPT 通过插件机制将证明请求包含定理定位信息发送到本地运行的 LeanDojoChatGPT 后端服务器。LeanDojo 初始化环境后端服务器根据请求使用 LeanDojo 加载指定的 Lean 项目仓库和提交版本定位到目标定理初始化证明状态。多轮交互证明ChatGPT 根据当前证明目标生成一个或多个 Lean 策略如apply Exists.intro。策略通过插件发送到后端后端通过 LeanDojo 在 Lean 中执行该策略。LeanDojo 捕获执行结果新的目标、成功或错误信息并将其返回给 ChatGPT。ChatGPT 分析结果如果证明未完成则基于新目标生成下一个策略如果出错则尝试调整策略或解释错误。完成与反馈当 Lean 报告定理已证明goals accomplished或达到某种终止条件时完整的证明脚本或最终状态被返回给用户。注意由于 OpenAI 插件 API 的变更当前仓库的代码可能无法直接与最新版 ChatGPT 插件系统兼容。一个更通用的思路是将此架构应用于 ChatGPT 的 Function Calling 功能或 Assistants API甚至直接用于开源大模型如 LLaMA、CodeLlama的推理流程中。后文会讨论这一变通方案。2.2 为什么选择 Lean 和 LeanDojo在众多定理证明器中为什么这个项目选择了 Lean 和 LeanDojo选择 Lean 的优势活跃的社区与庞大的数学库MathlibLean 拥有目前最庞大、最活跃的形式化数学库 Mathlib涵盖了从基础代数到前沿数学的无数定义和定理。这为检索增强提供了丰富的素材。可编程性与元编程Lean 4 本身就是一个强大的编程语言其策略Tactic框架和元编程能力允许用户编写复杂的自动化证明过程这为与 AI 结合提供了良好的接口。精确的错误反馈Lean 能提供相对清晰、定位准确的错误信息这对于引导大模型进行调试至关重要。LeanDojo 的核心价值标准化交互接口它将与 Lean 交互的复杂性进程管理、状态解析封装成简洁的 Python API让研究者可以专注于语言模型部分而无需深入 Lean 的内部工作机制。检索增强的基石LeanDojo 内置了对 Mathlib 等库的索引和检索能力能够根据当前证明目标快速找到可能相关的定理和证明。这对于弥补大模型在精确知识记忆上的不足至关重要。可复现的研究基准LeanDojo 提供了一系列基准测试数据集如 LeanDojo Benchmark使得不同模型在定理证明上的性能可以公平比较。这个架构的精妙之处在于它没有试图让 ChatGPT 一次性生成整个冗长的证明代码这几乎注定会失败而是将其分解为一系列小的、可验证的步骤。每一步ChatGPT 都根据具体的、明确的上下文当前目标来行动并且每一步都立即得到来自 Lean 这个“严师”的反馈。这是一种典型的“强化学习”式交互模型通过试错和即时反馈来学习如何证明。3. 环境搭建与部署实操详解虽然原仓库因 API 变更而暂时无法直接使用但理解其部署过程对于复现思路或迁移到新平台至关重要。下面我将详细拆解每一步并补充官方文档中未提及的细节和潜在问题。3.1 前期准备与依赖安装系统要求建议使用 Linux 或 macOS 系统进行开发。Windows 系统可能需要在 WSL2 环境下运行以确保与 Docker 和 Lean 环境的兼容性。确保你的 Python 版本在 3.8 以上。第一步创建并激活虚拟环境强烈建议使用虚拟环境来管理依赖避免与系统包冲突。# 使用 venv python -m venv leandojo_env source leandojo_env/bin/activate # Linux/macOS # 或 .\leandojo_env\Scripts\activate # Windows # 或者使用 conda conda create -n leandojo_env python3.10 conda activate leandojo_env第二步安装核心 Python 依赖根据项目要求安装以下包pip install loguru quart quart_cors lean-dojologuru: 一个更友好、功能更强大的日志库方便调试后端服务。quart: 一个异步的 Python Web 框架与 Flask API 兼容。ChatGPT 插件后端需要以 Web 服务器形式提供 APIQuart 是一个轻量级的选择。quart_cors: 处理跨域资源共享CORS这对于本地开发时 ChatGPT 网页端访问本地服务是必须的。lean-dojo: 核心组件。安装时会自动处理一些 Lean 相关的依赖。第三步处理潜在的依赖冲突lean-dojo可能对某些包的版本有特定要求。如果安装失败或后续运行出错可以尝试先安装 LeanDojo 的基础依赖再安装其他包。# 先单独安装 lean-dojo观察其依赖 pip install lean-dojo # 然后再安装 quart 等如果版本冲突pip 会提示可能需要指定版本 # 例如pip install “quart0.18.0”实操心得我在 Ubuntu 22.04 上部署时遇到了cryptography包编译失败的问题这通常是因为缺少系统级的开发库。解决方案是安装build-essential和libssl-devsudo apt-get update sudo apt-get install build-essential libssl-dev。对于 macOS可能需要通过 Homebrew 安装openssl。3.2 启动后端服务器参数详解与问题排查原项目的启动命令如下CONTAINERdocker python main.py --port 23456 --url https://github.com/yangky11/lean-example --commit 5a0360e49946815cb53132638ccdd46fb1859e2a让我们逐一解析每个参数和背后的逻辑CONTAINERdocker这是一个环境变量告诉 LeanDojo 使用 Docker 容器来运行 Lean 环境。这是推荐的方式因为它能确保一个干净、一致、与宿主机隔离的 Lean 环境避免因本地 Lean 版本、路径等问题导致的失败。如果设置为CONTAINERpodman则使用 Podman如果未设置或设置为其他值则会尝试在本地直接运行 Lean这要求你的系统已正确安装 Lean 和项目依赖不推荐新手使用。python main.py运行后端的入口脚本。--port 23456指定后端服务器监听的端口号。你可以更改为任何未被占用的端口如 5000, 8080。--url https://github.com/yangky11/lean-example指定一个包含 Lean 代码的 Git 仓库地址。这个仓库是证明任务的“工作区”其中包含了你要证明的定理。示例中使用的是一个简单的示例仓库。--commit 5a0360e...指定要使用的 Git 提交哈希。这非常重要它确保了代码版本的一致性。Lean 和 Mathlib 发展迅速不同版本的定理名称、定义或证明方式可能发生变化。锁定一个提交可以保证实验的可复现性。启动过程详解与监控执行上述命令后服务器会开始启动。你会看到一系列日志输出。首次运行的 Docker 拉取如果本地没有所需的 Docker 镜像通常是lean-dojo/lean-dojo相关镜像会自动从 Docker Hub 拉取。这可能需要几分钟时间取决于你的网络速度。克隆代码仓库服务器会克隆指定的 Git 仓库到临时目录。构建 Lean 项目进入仓库目录运行lake buildLean 的包管理/构建工具来编译项目依赖。这是第一个常见的卡点。如果项目依赖了特定版本的 Mathliblake build可能需要下载和编译大量文件耗时较长并可能因网络问题失败。服务器就绪当看到类似Running on http://0.0.0.0:23456的日志时说明后端 API 服务器已经启动成功。常见启动问题与排查问题现象可能原因解决方案Docker not found错误Docker 未安装或未运行。安装 Docker Desktop 或 Docker Engine并确保 Docker 守护进程正在运行sudo systemctl start docker或启动 Docker Desktop。lake build失败提示找不到包或版本冲突1. 网络问题无法下载依赖。2. 仓库的lakefile.lean配置可能已过时。1. 检查网络或配置代理。2. 尝试使用更近期的、已知可工作的示例仓库或根据错误信息调整lakefile.lean。端口23456被占用该端口已被其他程序使用。更改--port参数例如--port 34567。启动后立即退出无错误信息可能缺少某些依赖或环境变量设置错误。设置环境变量VERBOSE1再运行查看更详细的调试日志VERBOSE1 CONTAINERdocker python main.py ...ImportErrorforlean_dojoPython 路径问题或未正确安装lean-dojo包。确保在正确的虚拟环境中并尝试重新安装pip install --force-reinstall lean-dojo。重要提示由于 OpenAI 已更新其插件协议原main.py中实现的插件清单 (/.well-known/ai-plugin.json) 接口可能已不被 ChatGPT 识别。这是项目“过时”的主要原因。后续的“变通与进阶玩法”章节将讨论如何适配新的 API。3.3 历史步骤ChatGPT 插件配置这部分描述了在插件 API 变更前如何将本地服务注册到 ChatGPT 的流程。了解它有助于理解整个工作流确保后端服务器在本地运行如http://localhost:23456。登录 ChatGPT 网页版并确保已开通插件功能通常需要 ChatGPT Plus 订阅。在模型选择处选择 “GPT-4” 下的 “Plugins” 模式。点击插件下拉菜单进入 “Plugin store”。选择 “Develop your own plugin”。在弹出的对话框中输入你的本地服务器地址http://localhost:23456。ChatGPT 会尝试访问该地址下的/.well-known/ai-plugin.json文件来获取插件清单。如果成功便可安装这个“本地插件”。安装成功后你就可以在对话中要求 ChatGPT 使用这个插件来证明定理了。4. 核心原理大语言模型如何与证明器协同工作要让 ChatGPT 这样的生成式模型完成定理证明这样高精度的任务简单的端到端生成是行不通的。LeanDojoChatGPT 项目揭示了一种有效的范式工具增强的、基于反馈的迭代生成。下面我们深入看看其背后的原理。4.1 从自然语言到证明策略提示工程与思维链用户输入的是自然语言如“证明定理hello_world”。ChatGPT 需要将其转化为一系列动作。这背后依赖于精心设计的系统提示词System Prompt和思维链Chain-of-Thought, CoT引导。系统提示词的角色 系统提示词在后台定义了 ChatGPT 在本次对话中的“角色”和行为准则。对于定理证明插件提示词可能包含身份设定“你是一个 Lean 定理证明助手能够与 Lean 证明环境交互。”能力说明“你可以通过调用插件工具来获取当前证明目标、执行策略、或重置证明状态。”工作流程指令“当用户提出证明请求时你应首先定位定理然后解释定理含义接着制定一个高层次证明计划最后通过迭代执行策略来完成证明。”格式要求“你应当清晰地区分你的推理过程和发送给插件的命令。”思维链的引导 模型在生成最终动作策略前会进行内部推理。例如用户“证明hello_world。”ChatGPT 思考“用户想证明hello_world。我需要先让插件在指定仓库中定位这个定理。然后我应该查看它的类型向用户解释。这是一个简单的等式证明吗可能需要使用rfl自反性策略。让我先获取初始状态。”ChatGPT 行动调用插件工具get_initial_state参数为{“file_path”: “src/example.lean”, “theorem_name”: “hello_world”}。插件返回返回初始证明目标⊢ “Hello, world!” “Hello, world!”。ChatGPT 思考“目标是一个字符串的相等性自反命题。最简单的策略是rfl。”ChatGPT 行动调用插件工具run_tactic参数为{“tactic”: “rfl”}。插件返回“Proof completed successfully.”通过这种“思考-行动-观察”的循环ChatGPT 将复杂的证明任务分解为可管理的步骤并在每一步都基于真实的环境反馈进行决策。4.2 LeanDojo 的交互机制状态、策略与反馈LeanDojo 作为桥梁其 API 设计至关重要。它主要提供以下几类接口初始化与状态获取initialize加载特定仓库和提交返回一个会话句柄。get_state给定定理位置返回初始的证明目标、假设和环境信息。这通常是对话的起点。策略执行run_tactic这是核心接口。输入是当前的证明状态和一个策略字符串如intro h输出是执行后的新状态。如果策略执行成功新状态会显示更新后的目标如果失败则会返回 Lean 给出的错误信息。检索增强retrieve根据当前的证明目标通常表示为一个序列化的目标字符串从 Mathlib 等知识库中检索出最相关的定理、定义或证明片段。这些检索结果可以作为额外的上下文插入到给 ChatGPT 的提示中帮助它“想起”可用的定理或常见的证明模式。状态表示 LeanDojo 如何将 Lean 的内部证明状态转化为语言模型能理解的格式通常它会将“目标”和“假设”格式化为一种结构化的文本。例如假设 h1 : n 0 h2 : m : Nat 目标 ⊢ n m m这种表示方式清晰地将上下文与待证目标分离便于模型理解。错误处理与恢复 当run_tactic失败时Lean 返回的错误信息如 “unknown identifier ‘x’”、“tactic failed” 等会被捕获并返回给 ChatGPT。一个强大的模型应该能解析这些错误并调整策略。例如看到 “unknown identifier”它可能会尝试先unfold一个定义或者检查变量名是否拼写正确。这种从错误中学习的能力是 AI 辅助证明走向实用的关键。4.3 检索增强的价值弥补模型的“知识盲区”大语言模型拥有广泛的“常识”和模式识别能力但它不可能精确记住 Mathlib 中成千上万个定理的名称和用法。这就是检索增强的价值所在。工作原理当证明陷入僵局或者模型不确定该用什么定理时可以触发检索。LeanDojo 将当前证明目标可能是一个复杂的逻辑命题转换为一个查询向量。在一个预先构建的、包含 Mathlib 所有定理的向量数据库中进行相似性搜索。返回最相关的几个定理及其类型签名和文档。这些定理被作为“提示”插入到给 ChatGPT 的上下文中“这里有一些可能相关的定理add_comm (a b : Nat) : a b b a,mul_le_mul...”。模型可以据此选择使用哪个定理并生成相应的apply或rewrite策略。这相当于给 ChatGPT 配备了一个随时可查的、精准的“数学公式手册”极大地提升了其在专业领域内的表现。这也是 LeanDojo 论文的核心贡献之一它表明即使是强大的通用模型在专业任务上也需要与领域特定的知识库相结合。5. 变通方案与进阶玩法探索既然原插件因 API 变更而失效我们如何继续利用这一强大思路以下是一些可行的变通和进阶方向。5.1 转向 ChatGPT Assistants API 或 Function CallingOpenAI 已经推出了更通用、更强大的 Assistants API 和一直可用的 Function Calling 功能。我们可以用它们来重建类似的工作流。方案一使用 Function Calling定义工具函数将 LeanDojo 的核心功能get_state,run_tactic,retrieve包装成几个具体的函数并为其编写清晰的描述和参数 JSON Schema。在对话中调用在向 ChatGPT API 发送消息时在tools参数中传入这些函数的定义。当 ChatGPT 认为需要调用时它会返回一个包含函数名和参数的响应。本地执行并返回你的后端程序接收到这个调用请求后通过 LeanDojo 实际执行然后将结果以特定格式返回给 ChatGPT API继续对话。示例流程伪代码# 1. 定义函数 tools [ { “type”: “function”, “function”: { “name”: “get_theorem_state”, “description”: “Get the initial proof state of a theorem in a Lean repository.”, “parameters”: {...} # 定义 file_path, theorem_name 等参数 } }, { “type”: “function”, “function”: { “name”: “apply_tactic”, “description”: “Apply a Lean tactic to the current proof state and return the new state.”, “parameters”: {...} # 定义 tactic 字符串参数 } } ] # 2. 发起对话 response openai.chat.completions.create( model“gpt-4-turbo”, messages[{“role”: “user”, “content”: “Prove theorem hello_world in src/example.lean”}], toolstools ) # 3. 处理模型可能发起的函数调用 tool_call response.choices[0].message.tool_calls[0] if tool_call.function.name “get_theorem_state”: # 解析参数调用 LeanDojo result lean_dojo_client.get_state(...) # 将结果作为新的消息追加继续对话方案二使用 Assistants APIAssistants API 原生支持“代码解释器”和“函数调用”并且可以维护持久的线程和状态。你可以创建一个专用于“定理证明”的 Assistant为其配置上述函数作为工具。用户在一个线程中与 Assistant 对话Assistant 可以自主决定调用工具整个过程更接近原插件的体验。这两种方案都不再依赖旧的插件商店机制通用性更强并且可以由开发者完全控制。5.2 与开源大模型集成你并不一定需要 ChatGPT。可以将 LeanDojo 的后端与开源大模型如 CodeLlama、DeepSeek-Coder、Qwen-Coder 等相结合构建一个本地运行的定理证明助手。架构调整本地模型服务使用 Ollama、vLLM 或 Transformers 库部署一个开源代码大模型。自定义推理循环编写一个主控程序其逻辑为接收用户查询。调用本地模型并按照特定的提示模板将当前证明状态、历史、可用工具描述发送给模型。解析模型的输出需要训练或提示模型以固定格式输出如THOUGHT: ...\nACTION: get_state(...)\n。执行模型指定的动作通过 LeanDojo。将结果反馈给模型进入下一轮。提示工程为开源模型设计详细的系统提示教导它如何与 LeanDojo 交互包括解释证明状态格式、可用的策略语法、以及如何处理错误。优势与挑战优势完全本地化数据隐私有保障可定制性极高可以进行微调以专门优化证明能力。挑战开源模型的代码和推理能力可能弱于 GPT-4需要更精细的提示工程和可能的微调需要自己管理整个推理流程复杂度较高。5.3 扩展应用场景不仅仅是证明LeanDojoChatGPT 的范式可以推广到其他需要高精度、交互式反馈的任务中。程序验证与代码调试让模型与一个程序验证器如 F*、Dafny或符号执行引擎交互来验证代码的属性或查找 bug。模型可以提出修改建议验证器负责检查。教育工具构建一个交互式的数学或编程习题辅导系统。学生用自然语言描述解题思路系统通过背后的符号计算引擎如 SymPy或证明器来验证每一步的正确性并给出提示。形式化规范编写辅助工程师将自然语言需求逐步细化为形式化的、机器可检查的规范。模型可以建议规范的结构而工具则检查规范的一致性。其核心思想是“大语言模型作为规划与生成器专用工具作为验证与执行器”。这种分工协作让大模型得以在它擅长的模糊理解、创意生成领域发挥同时用专用工具来保证最终输出的精确性是解决大模型“幻觉”问题的一条重要路径。6. 实战案例从零开始证明一个简单定理为了让你有更直观的感受我们抛开过时的插件前端直接使用 LeanDojo 的 Python API 和 GPT-4 的 Function Calling 来模拟一次完整的证明过程。我们将使用一个极其简单的示例仓库。步骤 1准备 Lean 项目我们创建一个最简单的 Lean 项目只包含一个定理。mkdir lean_example cd lean_example # 创建 lakefile.lean定义项目 echo ‘ import Lake open Lake DSL package “lean_example” where -- add package configuration options here [default_target] lean_lib “LeanExample” where -- add library configuration options here ‘ lakefile.lean # 创建源代码目录和文件 mkdir -p LeanExample echo ‘ namespace LeanExample theorem hello_world : “Hello, world!” “Hello, world!” : by rfl end LeanExample ‘ LeanExample/Example.lean这个定理hello_world的证明就是rfl自反性。步骤 2编写 Python 控制脚本我们将编写一个脚本它使用 LeanDojo 与 Lean 交互并使用 OpenAI API 来模拟 ChatGPT 的决策。import asyncio from lean_dojo import * import openai import os # 设置 OpenAI API 密钥 openai.api_key os.getenv(“OPENAI_API_KEY”) # 1. 连接到 Lean 仓库这里使用本地路径 repo LocalRepo(“./lean_example”) # 指向我们刚创建的项目目录 commit repo.get_commit() lean Dojo(repo, commit, “lean_example:LeanExample”) # 2. 定义工具函数这些函数将被“暴露”给 GPT def get_theorem_state(file_path: str, theorem_name: str): “”“获取定理的初始证明状态。”“” try: theorem lean.get_theorem(f“{file_path}:{theorem_name}”) state lean.init_state(theorem) return { “success”: True, “state”: f“目标{state.goal}\n假设{state.hypotheses}” } except Exception as e: return {“success”: False, “error”: str(e)} def apply_tactic(tactic: str): “”“在当前状态下应用一个策略。”“” global current_state try: # 这里需要维护一个全局的 current_state模拟连续对话 result lean.run_tactic(current_state, tactic) if result.is_successful: current_state result.next_state return { “success”: True, “new_state”: f“目标{current_state.goal}\n假设{current_state.hypotheses}”, “is_done”: len(current_state.goals) 0 # 检查是否证明完成 } else: return {“success”: False, “error”: result.error} except Exception as e: return {“success”: False, “error”: str(e)} # 3. 与 GPT 交互的主循环 async def prove_with_gpt(): global current_state print(“ 定理证明助手启动...) print(“请输入你想证明的定理格式文件路径:定理名例如LeanExample/Example.lean:hello_world) theorem_input input(“ “).strip() file_path, theorem_name theorem_input.split(“:”) # 获取初始状态 print(f“ 正在定位定理 {theorem_name}...”) init_result get_theorem_state(file_path, theorem_name) if not init_result[“success”]: print(f“❌ 失败{init_result[‘error’]}”) return current_state lean.init_state(lean.get_theorem(theorem_input)) print(f“✅ 初始状态获取成功\n{init_result[‘state’]}”) messages [ {“role”: “system”, “content”: “你是一个 Lean 定理证明专家。用户会给你一个证明目标你需要一步一步地使用 Lean 策略来完成证明。你只能使用 apply_tactic 工具来执行策略。每次只尝试一个策略。如果证明完成我会告诉你。”}, {“role”: “user”, “content”: f“请证明以下定理。当前状态是\n{init_result[‘state’]}\n请开始你的证明每次只给出一个策略。”} ] max_steps 20 for step in range(max_steps): # 调用 GPT-4并告诉它可用的工具 response openai.chat.completions.create( model“gpt-4”, messagesmessages, tools[{ “type”: “function”, “function”: { “name”: “apply_tactic”, “description”: “Apply a Lean tactic to the current proof state.”, “parameters”: { “type”: “object”, “properties”: { “tactic”: {“type”: “string”, “description”: “The Lean tactic to apply, e.g., ‘intro h‘, ‘apply foo‘, ‘rfl‘.”} }, “required”: [“tactic”] } } }], tool_choice“auto” ) msg response.choices[0].message messages.append(msg) # 将模型的回复加入历史 # 检查模型是否调用了工具 if msg.tool_calls: tool_call msg.tool_calls[0] if tool_call.function.name “apply_tactic”: import json args json.loads(tool_call.function.arguments) tactic args[“tactic”] print(f“ 尝试策略{tactic}”) # 执行策略 result apply_tactic(tactic) # 将工具执行结果作为新消息加入对话 tool_msg { “role”: “tool”, “content”: json.dumps(result), “tool_call_id”: tool_call.id } messages.append(tool_msg) if result.get(“success”): print(f“✅ 策略成功。新状态\n{result.get(‘new_state’, ‘No new state’)}”) if result.get(“is_done”): print(“ 定理证明完成”) break else: print(f“❌ 策略失败{result.get(‘error’)}”) else: # 模型没有调用工具而是说了别的话如解释 print(f“ 模型回复{msg.content}”) if step max_steps - 1: print(“⏰ 达到最大步数限制证明未完成。”) await asyncio.sleep(1) # 避免请求过快 if __name__ “__main__”: current_state None asyncio.run(prove_with_gpt())步骤 3运行与观察运行这个脚本并输入LeanExample/Example.lean:hello_world。你会看到类似以下的交互 定理证明助手启动... 请输入你想证明的定理格式文件路径:定理名例如LeanExample/Example.lean:hello_world LeanExample/Example.lean:hello_world 正在定位定理 hello_world... ✅ 初始状态获取成功 目标⊢ “Hello, world!” “Hello, world!” 假设 尝试策略rfl ✅ 策略成功。新状态 目标 假设 定理证明完成在这个简单例子中GPT-4 很可能一眼就看出目标是一个自反等式直接使用了rfl策略并成功。对于更复杂的定理你会看到多轮的“思考-尝试-反馈”过程。这个案例虽然简单但它完整地展示了将大语言模型、函数调用和 LeanDojo 结合起来的核心工作流。你可以在此基础上增加更多功能如检索增强、更复杂的策略规划、或支持多定理证明等。7. 常见问题、挑战与未来展望在实际使用和探索类似项目时你可能会遇到以下挑战这里提供一些思路和展望。7.1 常见技术问题与排查问题类别具体表现排查思路与解决方案LeanDojo 环境问题lake build失败Docker 镜像拉取慢内存不足。1. 使用更小的示例仓库进行测试。2. 确保 Docker 有足够资源建议 4GB 内存。3. 对于网络问题可尝试配置 Docker 镜像加速器或使用预构建的镜像。API 与网络问题OpenAI API 调用失败本地服务器被 ChatGPT 网页端拒绝连接CORS。1. 检查 API 密钥是否正确是否有额度。2. 确保本地服务器使用quart_cors正确处理 CORS或使用ngrok等工具将本地服务暴露到公网注意安全。3. 确认 OpenAI API 的可用区域。模型能力问题ChatGPT 生成的策略总是错误无法理解复杂目标陷入循环。1.改进提示工程在系统提示中提供更详细的指导例如“优先尝试intro,apply,simp等简单策略”、“先分析目标的结构”。2.提供更多上下文在每次请求时不仅发送当前目标也发送最近几次的尝试和错误历史。3.使用检索增强集成 LeanDojo 的检索功能为模型提供相关定理提示。4.降级模型对于简单问题可以尝试使用gpt-3.5-turbo以降低成本但其证明能力会显著下降。性能与成本证明一个中等难度定理需要几十甚至上百轮交互API 调用成本高、速度慢。1.设置步数限制防止在不可能证明的目标上无限循环。2.本地模型替代对于研究或特定领域微调一个较小的开源模型可能是更经济的选择。3.缓存缓存常见的初始状态和成功的策略序列。7.2 当前范式的主要挑战搜索空间巨大即使是一个简单的定理可能的策略组合也是天文数字。当前的 GPT-4 加反馈循环本质上是一种启发式搜索效率远低于人类专家对于长证明或需要创造性构造的证明如存在量词的见证仍然力不从心。对提示高度敏感模型的表现极大地依赖于系统提示和用户指令的写法。微小的提示词改动可能导致证明成功率的显著变化这增加了使用的不可预测性。缺乏真正的“理解”模型是在学习策略应用的统计模式而非像人类一样理解数学对象的语义。这导致其证明过程可能脆弱在面对略微变化或需要深层数学洞察时容易失败。可复现性由于大语言模型固有的随机性同一个定理的证明过程可能每次都不一样甚至有时成功有时失败这对将其集成到严肃的开发流程中构成了障碍。7.3 未来发展方向尽管有挑战但 AI 辅助定理证明的方向充满希望专用模型的微调在大量 Lean 证明代码上对 CodeLlama 等模型进行监督微调或强化学习微调可以显著提升其生成正确策略的概率。LeanDojo 项目本身就提供了用于训练的数据集和基准。与符号推理引擎结合将大语言模型与传统的自动定理证明器ATP或 SMT 求解器结合。让大模型负责高层规划和解构将子目标交给这些专精于特定逻辑片段的、可确定的引擎去解决。人机协同交互模式未来的证明编辑器可能深度集成 AI 助手。人类数学家提出一个猜想并勾勒大致思路AI 负责填充繁琐的细节、查找引用、或处理大量重复的 case analysis。人类则专注于高层的创意和方向性指导。数学知识的发现也许更长远地这类系统不仅能证明已知定理还能通过探索巨大的数学空间提出新的猜想或发现非平凡的反例成为数学研究的真正合作伙伴。LeanDojoChatGPT 项目即使在其原始形式过时之后仍然为我们点亮了一条清晰的道路将大语言模型的自然语言交互和模式生成能力与形式化工具的精确性和可靠性相结合。这不仅是定理证明的未来也可能是许多其他需要高可靠性推理领域的未来。搭建和实验这样的系统对于任何对 AI 前沿应用感兴趣的开发者来说都是一次极具价值的实践。