axiom-verify（公理验证）

Axiom Lean 4 Proof Verification

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.

Before First Use

Check these once per session before running any Axle commands:

1. API key: Run echo $AXLE_API_KEY. If empty, the user needs to get a key from axle.axiommath.ai/app/console and set it: export AXLE_API_KEY=<key>.
2. CLI installed: Run axle --version. If not found, install with pip install axiom-axle.
3. Lean environment: Check for a lean-toolchain file in the project root to detect the Lean version. If present, use its version (e.g., leanprover/lean4:v4.28.0 becomes lean-4.28.0). If absent, default to lean-4.28.0.

Reference Files

Read these as needed based on the task:

1. references/axiom-configuration.md -- Setup, authentication, environment selection. Read this first if the user hasn't configured Axiom yet.
2. references/axiom-api-reference.md -- All 14 API endpoints with parameters and response formats. Read when you need exact parameter names or response fields.
3. references/axiom-cli-reference.md -- CLI commands and options. Read for exact flags and usage details when working with local files.
4. references/axiom-best-practices.md -- Workflow guidance, result interpretation, pitfalls, and tips. Read when planning a multi-step workflow or hitting unexpected behavior.
5. references/agents/verify-fix-agent.md -- Agent for autonomous check → repair → verify workflow.
6. references/agents/clean-analyze-agent.md -- Agent for autonomous normalize → extract → clean → check workflow.

Workflow

Step 1: Select the Right Tool

Match the user's intent to the appropriate endpoint:

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)

Step 2: Execute

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:

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

Verify a proof:

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

Repair broken proofs:

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

Disprove a conjecture:

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

Normalize a file (flatten sections/namespaces):

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

Extract theorems:

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

Simplify theorems:

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

Rename declarations:

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

Stub proofs with sorry:

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.):

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

API example (for dynamically constructed code):

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.

Step 3: Interpret Results

Every response includes lean_messages (Lean compiler output) and tool_messages (Axle diagnostics). Always check both -- transformation tools can "succeed" with zero tool_messages errors while lean_messages.errors reveals the code didn't compile.

Read references/axiom-best-practices.md for detailed result interpretation by endpoint type (check vs verify_proof vs transformation tools vs disprove), the user_error response format, and severity levels.

Critical: Always use --ignore-imports / "ignore_imports": true unless testing exact imports. Without it, import mismatches return user_error instead of the standard response.

Common Multi-Step Workflows

Verify and fix a proof: Spawn an agent following references/agents/verify-fix-agent.md. It autonomously runs check → repair → re-check → verify and returns a structured diagnosis.

Analyze and clean a file: Spawn an agent following references/agents/clean-analyze-agent.md. It autonomously runs normalize → extract → repair → simplify → check and returns a structural summary with cleaned output.

Scaffold a proof development:

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

Test a conjecture:

1. disprove -- look for counterexamples first
2. If no counterexample found, attempt the proof
3. check incrementally as you build the proof
4. verify_proof when complete

Common Pitfalls

Read references/axiom-best-practices.md before submitting code. Key traps: custom attributes must be stripped, autoImplicit is off in Mathlib, name shadowing causes silent failures, sections/namespaces require normalize first, and transformation tools silently return unchanged content on any compilation error.