axiom-verify

Axiom Lean 4 证明验证

Axiom 通过 Axle API 提供基于云端的 Lean 4 证明验证服务。它无需本地安装 Lean，即可在完整的 Mathlib 环境中编译并检查 Lean 代码——几秒内就能返回验证结果，而本地构建需要几分钟。

首次使用前

每个会话中运行任何 Axle 命令前，请先检查以下内容：

1. API 密钥：运行 echo $AXLE_API_KEY。如果为空，用户需要从 axle.axiommath.ai/app/console 获取密钥并设置：export AXLE_API_KEY=<key>。
2. CLI 已安装：运行 axle --version。如果找不到，请使用 pip install axiom-axle 安装。
3. Lean 环境：检查项目根目录中是否有 lean-toolchain 文件，以确定 Lean 版本。如果有，请使用其中指定的版本（例如，leanprover/lean4:v4.28.0 对应 lean-4.28.0）。如果没有，则默认使用 lean-4.28.0。

参考文件

根据任务需要阅读以下文件：

1. references/axiom-configuration.md -- 设置、身份验证和环境选择。如果用户尚未配置 Axiom，请先阅读此文件。
2. references/axiom-api-reference.md -- 全部 14 个 API 端点及其参数和响应格式。需要确认确切的参数名称或响应字段时阅读。
3. references/axiom-cli-reference.md -- CLI 命令和选项。处理本地文件时，请阅读以确认确切的标志和用法。
4. references/axiom-best-practices.md -- 工作流指导、结果解读、常见问题和技巧。规划多步骤工作流或遇到意外行为时阅读。
5. references/agents/verify-fix-agent.md -- 用于自主执行检查 → 修复 → 验证工作流的 Agent。
6. references/agents/clean-analyze-agent.md -- 用于自主执行规范化 → 提取 → 清理 → 检查工作流的 Agent。

工作流

第 1 步：选择合适的工具

根据用户意图选择相应的端点：

用户想要……	端点	说明
验证证明是否正确	verify_proof	根据形式化陈述检查候选证明
检查代码能否编译	check	快速进行语法和类型检查
了解证明结构	extract_theorems	将文件拆分为独立的定理单元
重命名声明	rename	自动更新各处的引用
转换 theorem/lemma	theorem2lemma	在 theorem 和 lemma 关键字之间切换
为证明添加占位内容	theorem2sorry	用 sorry 替换证明，以搭建框架
合并文件	merge	智能去重合并的文件
移除无操作的 tactic 或 have	simplify_theorems	移除不会改变证明状态的 tactic 和未使用的 have
移除完成后的 tactic	repair_proofs	移除证明完成后的 tactic、替换 sorry、修复不安全的 tactic
提取 have 语句	have2lemma	将内联的 have 提升为独立引理
为 have 主体添加占位内容	have2sorry	用 sorry 替换 have 主体
提取 sorry 占位符	sorry2lemma	将 sorry 转换为引理占位内容
测试陈述是否为假	disprove	通过 Plausible 尝试寻找反例
统一格式	normalize	清理 section、命名空间和注释

不确定该使用哪个工具时：

• 先使用 check，查看代码是否能够编译
• 使用 extract_theorems，了解文件中的内容
• 如果文件使用 section/namespace 块（这可能导致其他工具出现问题），请先使用 normalize

步骤 2：执行

处理本地文件时，优先使用 axle CLI——它直接从磁盘读取文件，语法更简单，还可以通过 -o 将输出写入文件。CLI 会自动从环境中读取 AXLE_API_KEY。注意：CLI 命令使用连字符（例如，verify-proof），而 HTTP API 使用下划线（verify_proof）。所有代码都会发送到 axle.axiommath.ai，在完整的 Mathlib 环境中编译——CLI 并非本地验证工具。

动态构造 Lean 代码时（在脚本、CI/CD 流水线中生成内容，或以编程方式构建代码字符串），请通过 curl 或 Python 客户端（pip install axiom-axle）使用 HTTP API。API 接受 JSON 字符串形式的内容，更适合处理生成的代码或内存中的代码。

检查代码是否能编译：

axle check file.lean --environment lean-4.28.0 --ignore-imports

验证证明：

axle verify-proof formal_statement.lean proof.lean \
  --environment lean-4.28.0 --ignore-imports

修复有问题的证明：

axle repair-proofs file.lean --environment lean-4.28.0 --ignore-imports \
  --repairs remove_extraneous_tactics,apply_terminal_tactics

反驳猜想：

axle disprove file.lean --environment lean-4.28.0 --ignore-imports

规范化文件（展平 section/namespace）：

axle normalize file.lean -o normalized.lean --environment lean-4.28.0 --ignore-imports

提取定理：

axle extract-theorems file.lean --environment lean-4.28.0 --ignore-imports

简化定理：

axle simplify-theorems file.lean --environment lean-4.28.0 --ignore-imports

重命名声明：

axle rename file.lean --declarations '{"old_name": "new_name"}' \
  --environment lean-4.28.0 --ignore-imports

用 sorry 占位证明：

axle theorem2sorry file.lean --environment lean-4.28.0 --ignore-imports

将转换结果写入文件（适用于 normalize、repair-proofs、simplify-theorems、rename 等）：

axle normalize file.lean -o output.lean -f --environment lean-4.28.0 --ignore-imports

API 示例（用于动态构造代码）：

curl -s -X POST https://axle.axiommath.ai/api/v1/check \
  -H "Authorization: Bearer $AXLE_API_KEY" \
  -H "Content-Type: application/json" \
  -d "$(jq -n \
    --arg content "$LEAN_CODE" \
    '{content: $content, environment: "lean-4.28.0", ignore_imports: true}')" \
  | jq '{okay, failed_declarations, lean_errors: .lean_messages.errors, tool_errors: .tool_messages.errors}'

完整的 CLI 命令参考请参阅 references/axiom-cli-reference.md。全部 14 个端点的 API 参数完整参考请参阅 references/axiom-api-reference.md。

步骤 3：解读结果

每个响应都包含 lean_messages（Lean 编译器输出）和 tool_messages（Axle 诊断信息）。务必同时检查两者——转换工具可能在没有任何 tool_messages 错误的情况下“成功”，但 lean_messages.errors 会显示代码未能编译。

请阅读 references/axiom-best-practices.md，了解按端点类型（check、verify_proof、转换工具和 disprove）解读结果的详细说明、user_error 响应格式以及严重级别。

重要： 除非要测试确切的导入项，否则始终使用 --ignore-imports / "ignore_imports": true。否则，导入项不匹配时会返回 user_error，而不是标准响应。

常见多步骤工作流

验证并修复证明： 按照 references/agents/verify-fix-agent.md 的说明启动 Agent。它会自主运行 check → repair → re-check → verify，并返回结构化诊断结果。

分析并清理文件： 按照 references/agents/clean-analyze-agent.md 的说明启动 Agent。它会自主运行 normalize → extract → repair → simplify → check，并返回结构摘要和清理后的输出。

搭建证明开发框架：

1. 编写形式化陈述
2. theorem2sorry——用 sorry 占位证明（使用 names 参数指定目标定理）
3. 逐步补全证明
4. 每完成一个证明后运行 check，验证进度
5. sorry2lemma——跟踪剩余义务（生成 {name}.sorried 引理占位，并插入每个含 sorry 的定理之前）
6. 使用 verify_proof 进行最终验证

测试猜想：

1. disprove——先寻找反例
2. 如果没有找到反例，再尝试证明
3. 在构建证明时逐步运行 check
4. 完成后运行 verify_proof

常见陷阱

提交代码前请阅读 references/axiom-best-practices.md。需要注意的关键问题：必须移除自定义属性；Mathlib 中的 autoImplicit 处于关闭状态；名称遮蔽会导致静默失败；必须先运行 normalize 处理 section/namespace；任何编译错误都会导致转换工具静默返回未更改的内容。