verify_proof

Validate a candidate Lean theorem and check that it conforms to the given formal statement.

Python API

result = await axle.verify_proof(
    formal_statement="import Mathlib\ntheorem citation_needed : 1 = 1 := by sorry",
    content="import Mathlib\ntheorem citation_needed : 1 = 1 := rfl",
    environment="lean-4.26.0",
    permitted_sorries=["helper"],  # Optional
    mathlib_linter=False,          # Optional
    ignore_imports=False,          # Optional
    timeout_seconds=120,           # Optional
)

print(result.okay)  # True if proof is valid
print(result.content)  # The processed Lean code

CLI

Usage: axle verify-proof FORMAL_STATEMENT CONTENT [OPTIONS]

# Basic usage
axle verify-proof statement.lean proof.lean --environment lean-4.26.0
# With permitted sorries
axle verify-proof statement.lean proof.lean --permitted-sorries helper1,helper2 --environment lean-4.26.0
# Pipeline usage
cat proof.lean | axle verify-proof statement.lean - --environment lean-4.26.0
# Exit non-zero if proof is invalid
axle verify-proof statement.lean proof.lean --strict --environment lean-4.26.0
# Use in shell conditionals
if axle verify-proof statement.lean proof.lean --strict --environment lean-4.26.0 > /dev/null; then
    echo "Proof valid"
fi
# Specify different environment
axle verify-proof statement.lean proof.lean --environment lean-4.26.0

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/verify_proof \
    -d '{"content": "import Mathlib\ntheorem citation_needed : 1 = 1 := rfl", "formal_statement": "import Mathlib\ntheorem citation_needed : 1 = 1 := by sorry", "environment": "lean-4.26.0"}' | jq

Input Parameters

Name	Type	Required	Description
formal_statement	str	Yes	Sorried out problem to validate against
content	str	Yes	A string of Lean code (the proof to verify)
environment	str	Yes	Environment to use (e.g., "lean-4.26.0", "lean-4.25.1")
permitted_sorries	list[str]	No	List of theorem names allowed to contain sorries
mathlib_linter	bool	No	If true, enables Mathlib's standard linter set. Requires Mathlib. Default: false
use_def_eq	bool	No	If true, uses definitional equality to compare types. Default: true
ignore_imports	bool	No	If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false
timeout_seconds	float	No	Maximum execution time (default: 120)

Notes:

• permitted_sorries may include theorem names not present in the candidate content or formal statement.
• use_def_eq is on by default to robustly capture types that are definitionally equal (equal after kernel reduction). However, definitional equality can be slow, so set it to false for faster (but occasionally flaky) comparison.

Output Fields

Name	Type	Description
okay	bool	True if the candidate theorem passes verification
content	str	The Lean code that was actually processed (after header injection if imports were ignored)
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists. Errors here mean the provided content was not valid Lean code.
tool_messages	dict	Messages from verification tool with errors, warnings, infos lists. Errors here mean content was valid Lean code, but not a satisfactory proof of formal_statement.
failed_declarations	list[str]	Declaration names that failed validation
timings	dict	Timing info: total_ms, candidate_ms, formal_statement_ms, declarations_ms

Verification Error Messages

tool_messages.errors will match one of the following patterns:

Pattern	Meaning
Missing required declaration '{name}'	A symbol in formal_statement is missing from content
Kind mismatch for '{name}': candidate has {X} but expected {Y}	Mismatch between definition kinds (e.g., theorem vs def)
Theorem '{name}' does not match expected signature: expected {X}, got {Y}	Type of theorem has been changed
Definition '{name}' does not match expected signature: expected {X}, got {Y}	Type or value of definition has been changed
Unsafe/partial function '{name}' detected	Use of a disallowed function
In '{name}': Axiom '{axiom}' is not in the allowed set of standard axioms	Use of a disallowed axiom
Declaration '{name}' uses 'sorry' which is not allowed in a valid proof	Theorem is not proven
Candidate uses banned 'open private' command	Use of disallowed open private command

Example Response

{
  "okay": false,
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl\n",
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [
      "Theorem 'foo' does not match expected signature: expected type 2 = 2, got 1 = 1"
    ],
    "warnings": [],
    "infos": []
  },
  "timings": {
    "total_ms": 160,
    "formal_statement_ms": 3,
    "declarations_ms": 0,
    "candidate_ms": 28
  },
  "failed_declarations": ["foo"]
}