comparator

A slower, more thorough version of verify_proof using the third-party leanprover/comparator tool.

This endpoint extracts theorem names from the formal statement, writes both the challenge and solution to temporary files, and validates the solution using the comparator.

Note: This endpoint uses a Docker-based comparator tool that currently only supports Lean 4.21.0. The environment parameter is ignored. Code written for other Lean versions may fail due to syntax or API differences.

Python API

result = await axle.comparator(
    content=solution_code,
    formal_statement=statement_code,
    environment="lean-4.21.0",
    memory_limit_mb=4096,  # Optional
    timeout_seconds=120,   # Optional
)
print(result.okay)
print(result.validated_theorem_names)

CLI

Usage: axle comparator FORMAL_STATEMENT CONTENT [OPTIONS]

# Basic usage
axle comparator statement.lean solution.lean --environment lean-4.26.0
# With memory limit
axle comparator statement.lean solution.lean --memory-limit-mb 4096 --environment lean-4.26.0
# Pipeline usage
cat solution.lean | axle comparator statement.lean - --environment lean-4.26.0
# Exit non-zero if solution is invalid
axle comparator statement.lean solution.lean --strict --environment lean-4.26.0
# Use in shell conditionals
if axle comparator statement.lean solution.lean --strict --environment lean-4.26.0 > /dev/null; then
    echo "Solution valid"
fi

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/comparator \
    -d '{"formal_statement": "import Mathlib\nlemma myDecl : 2 + 2 = 4 := by sorry", "content": "import Mathlib\nlemma myDecl : 2 + 2 = 4 := by simp", "environment": "lean-4.21.0"}' | jq

Input Parameters

Name	Type	Required	Description
formal_statement	str	Yes	Lean code containing the formal statement(s) to validate against
content	str	Yes	Lean code containing the candidate solution
environment	str	Yes	Environment to use (ignored - only Lean 4.21.0 is supported)
memory_limit_mb	int	No	Memory limit for the Docker container in megabytes
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)

Output Fields

Name	Type	Description
okay	bool	True if the solution is valid (determined by presence of "Your solution is okay!" in output)
output	str	The stdout/stderr output from the comparator Docker container
exit_status	int	The exit code from the Docker container (0 indicates success)
validated_theorem_names	list[str]	List of theorem names that were successfully validated
timings	dict	Timing info: total_ms, extract_theorems_ms, comparator_ms

Example Response

{
  "okay": true,
  "exit_status": 0,
  "output": "Building Challenge\n⚠ [36/37] Built Challenge\nwarning: Challenge.lean:2:6: declaration uses 'sorry'\nBuild completed successfully.\nExporting #[myDecl] from Challenge\nBuilding Solution\n✔ [36/37] Built Solution\nBuild completed successfully.\nExporting #[myDecl] from Solution\nRunning kernel on solution.\nSolution valid.\nYour solution is okay!",
  "validated_theorem_names": ["myDecl"],
  "timings": {
    "total_ms": 6363,
    "extract_theorems_ms": 1022,
    "comparator_ms": 5340
  }
}