axiom-verify

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Axiom Lean 4 Proof Verification

Axiom Lean 4 证明验证

Axiom provides cloud-based Lean 4 proof verification through the Axle API. It compiles and checks Lean code against a full Mathlib environment without requiring a local Lean installation -- verification results come back in seconds rather than the minutes it takes to build locally.

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

Reference Files

参考文档

Read these as needed based on the task:

references/axiom-configuration.md -- Setup, authentication, environment selection. Read this first if the user hasn't configured Axiom yet.
references/axiom-api-reference.md -- All 14 API endpoints with parameters and response formats. Read when you need exact parameter names or response fields.
references/axiom-cli-reference.md -- CLI commands and options. Read for exact flags and usage details when working with local files.
references/axiom-best-practices.md -- Workflow guidance, scope limitations, and tips. Read when planning a multi-step workflow or hitting unexpected behavior.

可根据任务需求阅读以下文档：

references/axiom-configuration.md —— 配置、身份验证、环境选择。如果用户尚未配置Axiom，请先阅读此文档。
references/axiom-api-reference.md —— 包含14个API端点的所有参数和响应格式。当需要确切的参数名称或响应字段时阅读此文档。
references/axiom-cli-reference.md —— CLI命令及选项。处理本地文件时，如需确切的标志和使用细节请阅读此文档。
references/axiom-best-practices.md —— 工作流指导、范围限制及技巧。规划多步骤工作流或遇到异常行为时阅读此文档。

Workflow

工作流

Step 1: Select the Right Tool

步骤1：选择合适的工具

Match the user's intent to the appropriate endpoint:

User wants to...	Endpoint	Notes
Verify a proof is correct	`verify_proof`	Checks candidate proof against a formal statement
Check if code compiles	`check`	Quick syntax and type checking
Understand proof structure	`extract_theorems`	Splits file into self-contained theorem units
Rename declarations	`rename`	Automatic reference updates throughout
Convert theorem/lemma	`theorem2lemma`	Switch between `theorem` and `lemma` keywords
Stub out proofs	`theorem2sorry`	Replace proofs with `sorry` for scaffolding
Combine files	`merge`	Intelligent deduplication across files
Remove no-op tactics/haves	`simplify_theorems`	Tactics that don't change proof state, unused haves
Remove post-completion tactics	`repair_proofs`	Tactics after proof is done, replace sorry, fix unsafe tactics
Extract have statements	`have2lemma`	Promote inline `have` to standalone lemma
Stub have bodies	`have2sorry`	Replace `have` bodies with `sorry`
Extract sorry placeholders	`sorry2lemma`	Turn `sorry` into lemma stubs
Test if statement is false	`disprove`	Attempts counterexample via Plausible
Standardize formatting	`normalize`	Clean up sections, namespaces, comments

When unsure which tool to use:

Start with
```
check
```
to see if the code compiles at all
Use
```
extract_theorems
```
to understand what's in the file
Use
```
normalize
```
first if the file uses
```
section
```
/
```
namespace
```
blocks (these can cause issues with other tools)

根据用户的需求匹配对应的端点：

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

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

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

Step 2: Execute

步骤2：执行操作

When working with local files, prefer the

axle

CLI -- it reads files directly from disk, has simpler syntax, and can write output to files with

-o

. The CLI reads

AXLE_API_KEY

from the environment automatically. Note: CLI commands use hyphens (e.g.,

verify-proof

), while the HTTP API uses underscores (

verify_proof

). All code is sent to

axle.axiommath.ai

for compilation against a full Mathlib environment -- the CLI is not local verification.

When constructing Lean code dynamically (generating content in scripts, CI/CD pipelines, or building code strings programmatically), use the HTTP API via curl or the Python client (

pip install axiom-axle

). The API accepts content as JSON strings, which is better suited for generated or in-memory code.

Check code compiles:

bash

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

Verify a proof:

bash

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

Repair broken proofs:

bash

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

Disprove a conjecture:

bash

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

Normalize a file (flatten sections/namespaces):

bash

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

Extract theorems:

bash

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

Simplify theorems:

bash

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

Rename declarations:

bash

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

Stub proofs with sorry:

bash

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

Write transformation output to a file (works with normalize, repair-proofs, simplify-theorems, rename, etc.):

bash

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

API example (for dynamically constructed code):

bash

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}'

For the full CLI command reference, see references/axiom-cli-reference.md. For the full API parameter reference for all 14 endpoints, see references/axiom-api-reference.md.

处理本地文件时，优先使用

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格式的字符串内容，更适合生成的或内存中的代码。

检查代码是否可编译：

bash

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

验证证明：

bash

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

修复损坏的证明：

bash

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

反证猜想：

bash

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

标准化文件格式（展开sections/namespaces）：

bash

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

提取定理：

bash

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

简化定理：

bash

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

重命名声明：

bash

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

用sorry生成证明占位符：

bash

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

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

bash

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

API示例（适用于动态构建的代码）：

bash

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。

Step 3: Interpret Results

步骤3：解读结果

Every response includes two types of messages -- understanding both is key to helping the user:

lean_messages
: Direct Lean compiler output. Errors here mean the Lean code itself has problems (type mismatches, tactic failures, unknown identifiers).
tool_messages
: Axle-specific diagnostics. Errors here mean the tool couldn't process the request (import mismatches, unsupported constructs, timeouts). The
```
tool_messages.infos
```
field often contains unsolved goals when a proof fails -- always check this for debugging context.

Severity levels:

Errors: Result may be unusable
Warnings: Suspicious but non-fatal
Infos: Timing/debug output, unsolved goals

For
check
: Returns

okay

(boolean) and

failed_declarations

(list). The

okay

flag reflects compilation success only --

true

if the code compiles without errors (warnings like

sorry

don't affect it).

failed_declarations

is empty when

okay

true

. The

check

endpoint does not detect sorry usage or other verification-level issues -- it only checks that code compiles. Use

verify_proof

to validate that proofs are complete.

For
verify_proof
: Returns

okay

(boolean) and

failed_declarations

(list). The

okay

flag reflects proof validity --

true

only if the code compiles and passes all verification checks (no sorry, signatures match, no disallowed axioms). Note the distinction:

Compilation errors (tactic failures, syntax errors, name collisions):
```
okay
```
is
```
false
```
,
```
failed_declarations
```
is empty. The errors appear in
```
lean_messages.errors
```
.
Verification failures (sorry usage, signature mismatch, disallowed axioms):
```
okay
```
is
```
false
```
, and the offending names appear in
```
failed_declarations
```
with details in
```
tool_messages.errors
```
.
Fully valid proof:
```
okay
```
is
```
true
```
and
```
failed_declarations
```
is empty. This is the only state that means the proof is both compilable and complete.

For transformation tools (

repair_proofs

simplify_theorems

normalize

, etc.): These do not return

okay

failed_declarations

. Check that

lean_messages.errors

is empty and inspect the

content

field for the transformed result.

For
disprove
: Check

disproved_theorems

(list of refuted names) and

results

(dict mapping each theorem name to a human-readable outcome string). If a counterexample is found, the name appears in

disproved_theorems

and the

results

entry contains the counterexample. If disprove fails (the theorem may be true),

disproved_theorems

is empty and the

results

entry describes why the negation could not be proven.

Import handling: Always use

--ignore-imports

(CLI) or

"ignore_imports": true

(API) unless you have a specific reason not to (e.g., testing that exact imports are correct). Without this flag, import mismatches return a

user_error

string instead of the standard response format, which breaks JSON parsing and hides the actual verification result. Code snippets, code from different Lean/Mathlib versions, and proof-logic checks all require this flag.

user_error
responses: Several error conditions return

{"user_error": "...", "info": {...}}

instead of the standard response format. This includes import mismatches (when

ignore_imports

is false), unrecognized declaration names in

rename

, and other request-level validation failures. Always check for a

user_error

field before parsing

lean_messages

tool_messages

每个响应都包含两种类型的消息——理解这两种消息是帮助用户的关键：

lean_messages
：Lean编译器的直接输出。此处的错误意味着Lean代码本身存在问题（类型不匹配、策略失败、未知标识符）。
tool_messages
：Axle特有的诊断信息。此处的错误意味着工具无法处理请求（导入不匹配、不支持的构造、超时）。当证明失败时，
```
tool_messages.infos
```
字段通常包含未解决的目标——调试时务必查看此字段。

严重级别：

错误：结果可能无法使用
警告：存在可疑但非致命的问题
信息：计时/调试输出、未解决的目标

对于
check
：返回

okay

（布尔值）和

failed_declarations

（列表）。

okay

标志仅反映编译是否成功——如果代码编译无错误则为

true

（像

sorry

这样的警告不影响该值）。当

okay

为

true

时，

failed_declarations

为空。

check

端点不会检测

sorry

的使用或其他验证级别的问题——它仅检查代码是否可编译。请使用

verify_proof

验证证明是否完整。

对于
verify_proof
：返回

okay

（布尔值）和

failed_declarations

（列表）。

okay

标志反映证明的有效性——只有当代码可编译并且通过所有验证检查（无sorry、签名匹配、无禁用公理）时才为

true

。请注意以下区别：

编译错误（策略失败、语法错误、名称冲突）：
```
okay
```
为
```
false
```
，
```
failed_declarations
```
为空。错误信息出现在
```
lean_messages.errors
```
中。
验证失败（使用sorry、签名不匹配、使用禁用公理）：
```
okay
```
为
```
false
```
，有问题的名称会出现在
```
failed_declarations
```
中，详细信息在
```
tool_messages.errors
```
中。
完全有效的证明：
```
okay
```
为
```
true
```
且
```
failed_declarations
```
为空。只有这种状态才表示证明既可以编译又完整。

对于转换工具（

repair_proofs

、

simplify_theorems

、

normalize

等）：这些工具不会返回

okay

或

failed_declarations

。请检查

lean_messages.errors

是否为空，并查看

content

字段获取转换后的结果。

对于
disprove
：查看

disproved_theorems

（已被反驳的名称列表）和

results

（将每个定理名称映射为人类可读结果字符串的字典）。如果找到反例，该名称会出现在

disproved_theorems

中，

results

中的对应条目包含反例信息。如果反证失败（定理可能为真），

disproved_theorems

为空，

results

中的条目会说明为何无法证明该陈述的否定。

导入处理： 除非有特定原因（例如测试导入是否完全正确），否则请始终使用

--ignore-imports

（CLI）或

"ignore_imports": true

（API）。如果不使用此标志，导入不匹配会返回

user_error

字符串而非标准响应格式，这会破坏JSON解析并隐藏实际的验证结果。代码片段、来自不同Lean/Mathlib版本的代码、证明逻辑检查都需要使用此标志。

user_error
响应：多种错误情况会返回

{"user_error": "...", "info": {...}}

而非标准响应格式。这包括导入不匹配（当

ignore_imports

为false时）、

rename

中无法识别的声明名称，以及其他请求级别的验证失败。在解析

lean_messages

tool_messages

之前，请始终检查是否存在

user_error

字段。

Common Multi-Step Workflows

常见多步骤工作流

Verify and fix a proof:

```
check
```
-- see if it compiles
If errors:
```
repair_proofs
```
-- attempt automatic fix
```
check
```
again -- verify the repair worked
```
verify_proof
```
-- confirm it proves the intended statement

Analyze and clean a file:

```
normalize
```
-- standardize formatting first (flatten sections/namespaces)
```
extract_theorems
```
-- understand the structure
```
repair_proofs
```
with
```
remove_extraneous_tactics
```
-- remove tactics after proof is already complete
```
simplify_theorems
```
-- remove unused haves and no-op tactics
```
check
```
-- verify nothing broke

Scaffold a proof development:

Write formal statements
```
theorem2sorry
```
-- stub out proofs with
```
sorry
```
(use
```
names
```
parameter to target specific theorems)
Fill in proofs incrementally
```
check
```
after each proof to verify progress
```
sorry2lemma
```
-- track remaining obligations (generates
```
{name}.sorried
```
lemma stubs inserted before each sorry'd theorem)
```
verify_proof
```
for final verification

Test a conjecture:

```
disprove
```
-- look for counterexamples first
If no counterexample found, attempt the proof
```
check
```
incrementally as you build the proof
```
verify_proof
```
when complete

验证并修复证明：

```
check
```
—— 查看是否可编译
如果有错误：
```
repair_proofs
```
—— 尝试自动修复
再次
```
check
```
—— 验证修复是否有效
```
verify_proof
```
—— 确认证明符合预期陈述

分析并清理文件：

```
normalize
```
—— 先标准化格式（展开sections/namespaces）
```
extract_theorems
```
—— 理解文件结构
使用
```
repair_proofs
```
并设置
```
remove_extraneous_tactics
```
—— 移除证明完成后的多余策略
```
simplify_theorems
```
—— 移除未使用的have语句和无操作策略
```
check
```
—— 验证未出现问题

搭建证明开发框架：

编写形式化陈述
```
theorem2sorry
```
—— 用
```
sorry
```
生成证明占位符（使用
```
names
```
参数指定目标定理）
逐步填充证明内容
每次填充后使用
```
check
```
验证进度
```
sorry2lemma
```
—— 跟踪剩余任务（在每个带sorry的定理前生成
```
{name}.sorried
```
引理占位符）
最终使用
```
verify_proof
```
验证

测试猜想：

```
disprove
```
—— 先尝试寻找反例
如果未找到反例，尝试编写证明
编写证明时逐步使用
```
check
```
验证
完成后使用
```
verify_proof
```
验证

Common Pitfalls

常见陷阱

Custom project attributes and constructs. Files from Lean projects often define custom attributes (e.g.,
```
@[category research open, AMS 11]
```
) and helper constructs (e.g.,
```
answer(sorry)
```
) via project-specific imports. When
```
ignore_imports: true
```
replaces those imports with standard Mathlib, these custom constructs become unresolvable and produce compilation errors. Before submitting, strip custom attributes and project-specific constructs using sed or similar:
```
sed 's/@\[category [^]]*\]//' file.lean
```
removes
```
@[category ...]
```
blocks; replace
```
answer(sorry)
```
with
```
True
```
or remove it entirely. Note:
```
@[category ... open ...]
```
triggers a misleading "Candidate uses banned 'open private' command" tool error because the parser misinterprets the word
```
open
```
inside the attribute as the
```
open private
```
command -- this is a false positive that disappears once the attribute is stripped.
autoImplicit
is off in Mathlib environments. Always declare type variables explicitly (e.g.,
```
variable {α : Type*}
```
or
```
(α : Type*)
```
). Implicit variables like
```
List α
```
without declaring
```
α
```
will fail.
Mathlib name shadowing. If your theorem names match existing Mathlib declarations (e.g.,
```
add_zero
```
,
```
add_comm
```
,
```
mul_comm
```
), you'll get "already declared" errors and all transformation tools will silently return unchanged content with zero stats. The error appears only in
```
lean_messages.errors
```
, not
```
tool_messages
```
-- you must inspect
```
lean_messages
```
to notice the problem. Use
```
rename
```
to give theorems unique names, or prefix with a namespace.
omega
cannot see through opaque definitions. The
```
omega
```
tactic works on linear arithmetic over
```
Nat
```
and
```
Int
```
, but it treats user-defined functions as opaque. If you define
```
def my_double (n : Nat) := n + n
```
and try to prove
```
my_double n = 2 * n
```
with
```
omega
```
, it will fail because
```
omega
```
doesn't know what
```
my_double
```
computes. Use
```
unfold my_double
```
(or
```
simp [my_double]
```
) before
```
omega
```
to expose the definition.
simplify_theorems
vs
repair_proofs
for cleanup. These serve different purposes:
- ```
simplify_theorems
```
  with
```
remove_unused_tactics
```
  : removes tactics that are no-ops (don't change the proof state at all)
- ```
repair_proofs
```
  with
```
remove_extraneous_tactics
```
  : removes tactics that appear after the proof is already complete
- For cleaning up redundant tactics, you usually want
```
repair_proofs
```
  first, then
```
simplify_theorems
```
  .
Sections and namespaces.
```
extract_theorems
```
,
```
theorem2sorry
```
, and other transformation tools may produce non-compilable output when sections/namespaces are present because extracted names won't be fully qualified. Always run
```
normalize
```
first to flatten these constructs. Note that
```
normalize
```
preserves the original indentation from inside flattened blocks -- the output may look oddly indented but still compiles correctly. Caveat:
```
normalize
```
may not update all references inside theorem bodies when flattening namespaces (e.g.,
```
p k
```
may not become
```
Namespace.p k
```
). Always
```
check
```
the normalized output and fix any unresolved references manually.
rename
requires fully-qualified names. The
```
declarations
```
parameter must use fully-qualified names including namespace prefixes. For example, if
```
my_thm
```
is inside
```
namespace Foo
```
, use
```
{"Foo.my_thm": "Foo.new_name"}
```
, not
```
{"my_thm": "new_name"}
```
. Using an unqualified name returns a
```
user_error
```
("Source name not found").
Non-theorem commands in
extract_theorems
. The
```
extract_theorems
```
tool warns about any non-theorem command it encounters with
```
"Unsupported command kind ..."
```
. This includes
```
variable
```
,
```
open
```
,
```
notation
```
,
```
set_option
```
, and other non-declaration commands. These warnings are informational -- the tool still correctly extracts all theorem declarations and includes dependencies (including
```
variable
```
bindings,
```
open
```
statements, etc.) in each theorem's standalone
```
content
```
block.
Always check both message types. Transformation tools can "succeed" (return content with zero
```
tool_messages
```
errors) while the underlying code has compilation errors visible only in
```
lean_messages.errors
```
. Always inspect
```
lean_messages.errors
```
even when
```
tool_messages
```
is clean. This silent failure mode applies broadly: any compilation error (custom attributes, missing imports, syntax issues, name shadowing) causes transformation tools to return unchanged content with zero stats. The only signal is non-empty
```
lean_messages.errors
```
.
The environments endpoint uses
```
/v1/environments
```
(no
```
/api/
```
prefix), while all tool endpoints use
```
/api/v1/{tool_name}
```
.

自定义项目属性和构造。来自Lean项目的文件通常会通过项目特定的导入定义自定义属性（例如
```
@[category research open, AMS 11]
```
）和辅助构造（例如
```
answer(sorry)
```
）。当
```
ignore_imports: true
```
将这些导入替换为标准Mathlib时，这些自定义构造会无法解析并导致编译错误。提交前，请使用sed或类似工具移除自定义属性和项目特定构造：
```
sed 's/@\[category [^]]*\]//' file.lean
```
会移除
```
@[category ...]
```
块；将
```
answer(sorry)
```
替换为
```
True
```
或直接移除。注意：
```
@[category ... open ...]
```
会触发误导性的“Candidate uses banned 'open private' command”工具错误，因为解析器会错误地将属性中的
```
open
```
视为
```
open private
```
命令——移除该属性后此错误会消失。
Mathlib环境中
autoImplicit
处于关闭状态。请始终显式声明类型变量（例如
```
variable {α : Type*}
```
或
```
(α : Type*)
```
）。像
```
List α
```
这样未声明
```
α
```
的隐式变量会导致失败。
Mathlib名称冲突。如果你的定理名称与现有Mathlib声明冲突（例如
```
add_zero
```
、
```
add_comm
```
、
```
mul_comm
```
），会出现“already declared”错误，所有转换工具会静默返回未修改的内容且无统计信息。该错误仅出现在
```
lean_messages.errors
```
中，不会出现在
```
tool_messages
```
中——你必须查看
```
lean_messages
```
才能发现问题。请使用
```
rename
```
为定理指定唯一名称，或添加命名空间前缀。
omega
无法穿透不透明定义。
```
omega
```
策略适用于
```
Nat
```
和
```
Int
```
上的线性算术，但它会将用户定义的函数视为不透明的。如果你定义
```
def my_double (n : Nat) := n + n
```
并尝试用
```
omega
```
证明
```
my_double n = 2 * n
```
，会失败，因为
```
omega
```
不知道
```
my_double
```
的计算逻辑。在使用
```
omega
```
之前，请使用
```
unfold my_double
```
（或
```
simp [my_double]
```
）来暴露该定义。
simplify_theorems
与
repair_proofs
的清理区别。它们的用途不同：
- ```
simplify_theorems
```
  搭配
```
remove_unused_tactics
```
  ：移除无操作（完全不改变证明状态）的策略
- ```
repair_proofs
```
  搭配
```
remove_extraneous_tactics
```
  ：移除证明完成后的多余策略
- 清理冗余策略时，通常先使用
```
repair_proofs
```
  ，再使用
```
simplify_theorems
```
Sections和Namespaces。
```
extract_theorems
```
、
```
theorem2sorry
```
等转换工具在处理sections/namespaces时可能会生成无法编译的输出，因为提取的名称不会被完全限定。请始终先运行
```
normalize
```
来展开这些构造。注意：
```
normalize
```
会保留展开块中的原始缩进——输出的缩进可能看起来奇怪，但仍然可以正确编译。注意事项：
```
normalize
```
在展开命名空间时可能不会更新定理体中的所有引用（例如
```
p k
```
可能不会变为
```
Namespace.p k
```
）。请始终
```
check
```
标准化后的输出，并手动修复任何无法解析的引用。
rename
需要完全限定名称。
```
declarations
```
参数必须使用包含命名空间前缀的完全限定名称。例如，如果
```
my_thm
```
在
```
namespace Foo
```
中，请使用
```
{"Foo.my_thm": "Foo.new_name"}
```
，而非
```
{"my_thm": "new_name"}
```
。使用非限定名称会返回
```
user_error
```
（“Source name not found”）。
extract_theorems
中的非定理命令。
```
extract_theorems
```
工具会对遇到的任何非定理命令发出
```
"Unsupported command kind ..."
```
警告。这包括
```
variable
```
、
```
open
```
、
```
notation
```
、
```
set_option
```
以及其他非声明命令。这些警告仅为信息性——工具仍会正确提取所有定理声明，并在每个定理的独立
```
content
```
块中包含依赖项（包括
```
variable
```
绑定、
```
open
```
语句等）。
始终检查两种类型的消息。转换工具可能会“成功”返回内容且
```
tool_messages
```
无错误，但底层代码可能存在仅在
```
lean_messages.errors
```
中可见的编译错误。即使
```
tool_messages
```
无错误，也请始终检查
```
lean_messages.errors
```
。这种静默失败模式广泛存在：任何编译错误（自定义属性、缺少导入、语法问题、名称冲突）都会导致转换工具返回未修改的内容且无统计信息。唯一的信号是
```
lean_messages.errors
```
非空。
环境端点使用
```
/v1/environments
```
（无
```
/api/
```
前缀），而所有工具端点使用
```
/api/v1/{tool_name}
```
。