check

Evaluate Lean code and collect all messages (errors, warnings, and info). Use this to check if code compiles without verification against a formal statement, or to get the output of #check / #eval statements.

Looking to confirm a proof? check reports compilation only — its okay field stays true even when a declaration uses sorry or a disallowed axiom. If you want a single pass/fail for "is this a complete, valid proof of a given statement," use verify_proof instead, which folds those failures into okay.

Try this example in the web UI

See Also

For interactive compilation feedback without an API, try the Lean 4 Web Playground.

Input Parameters

content · str · required · Lean source code

The Lean source code to be processed by this tool.

mathlib_options · bool · default: False · Enable Mathlib options

If true, enables conventional Mathlib options. This toggle sets linter.mathlibStandardSet to true, autoImplicit to false, relaxedAutoImplicit to false, and pp.unicode.fun to true.

names · list[str] · Theorem names to process

Optional list of theorem names to process. If not specified, all theorems are processed. Requesting a name not found in the code returns an error. When theorems_only is false, these select over all declarations (not just theorems).

indices · list[int] · Theorem indices to process

Optional list of theorem indices to process (0-based). Supports negative indices: -1 is the last theorem, -2 is second-to-last, etc. If not specified, all theorems are processed. When theorems_only is false, these select over all declarations (not just theorems).

theorems_only · bool · default: True · Process theorems/lemmas only

If true (default), only theorem/lemma declarations are processed. Set to false to process all declaration kinds (def/instance/abbrev/opaque/etc). When false, names and indices select over all declarations rather than just theorems.

ignore_imports · bool · default: True · Ignore import mismatches

Controls import statement handling:

• true (default): Ignore the imports in content and substitute the environment's default header. This uses the pre-built cached environment, so it is fast. The substituted code is returned in the content field.
• false: Process the imports in content exactly as written. This is significantly slower (the cached environment cannot be reused) and may produce inconsistent or incorrect results if a required dependency such as Mathlib.Tactic is missing. A warning is returned in these cases. See the troubleshooting page for more details.

environment · str · required · Lean environment or version

The Lean environment to use for evaluation. Each environment includes a specific Lean version and pre-built dependencies (typically Mathlib).

Available environments: lean-4.28.0, lean-4.27.0, lean-4.26.0, etc.

timeout_seconds · float · default: 120 · Max execution time in seconds

Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 900 seconds (15 minutes).

Output Fields

okay · bool · True if the Lean code compiles

Returns true if the code compiles without errors. Warnings don't affect this value.

This only reflects compilation. It does not mean the code is a complete, valid proof: a declaration that uses sorry, disallowed axioms, or unsafe definitions still compiles and leaves okay as true. Those findings are reported in tool_messages.warnings (with the offending names in failed_declarations). If you need to know whether the input is a real proof, also check that failed_declarations is empty, or better yet, use verify_proof.

content · string · Processed Lean code

The Lean code that was actually processed. May differ from input if ignore_imports=true caused header injection.

lean_messages · dict · Messages from Lean compiler

Messages from the Lean compiler with errors, warnings, and infos lists. Errors here indicate invalid Lean code (syntax errors, type errors, etc.); an empty errors list means the code compiles.

If the tool allows declaration selection and a names/indices selection is given, elaboration is skipped for the proofs of unselected declarations, so this field reflects only the selected declarations and is otherwise incomplete.

tool_messages · dict · Messages from check tool

Messages from the check tool with errors, warnings, and infos lists.

Validation findings — uses of sorry, disallowed axioms, or unsafe definitions — are reported as warnings here. Use verify_proof to treat them as errors.

If the tool allows declaration selection and a names/indices selection is given, elaboration is skipped for the proofs of unselected declarations, so this field reflects only the selected declarations and is otherwise incomplete.

failed_declarations · list · Declaration names that failed validation

List of declaration names that have compilation or validation errors. These are declarations that do not compile, use sorry, use disallowed axioms, etc. A file-level validation finding (e.g. use of open private) marks every declaration in the file as failed.

If the tool allows declaration selection and a names/indices selection is given, elaboration is skipped for the proofs of unselected declarations, so this field reflects only the selected declarations and is otherwise incomplete.

timings · dict · Execution timing breakdown

Timing information in milliseconds for various stages of processing.

Python API

result = await axle.check(
    content="import Mathlib\n#eval 2+2",
    environment="lean-4.28.0",
    mathlib_options=False,     # Optional
    ignore_imports=True,     # Optional
    timeout_seconds=120,      # Optional
)

print(result.okay)  # True if code compiles
print(result.okay and not result.failed_declarations)  # True if code compiles AND contains only complete, valid proofs
print(result.content)  # The processed Lean code
print(result.lean_messages.infos)  # ["4\n"]

CLI

Usage: axle check CONTENT [OPTIONS]

# Basic usage
axle check theorem.lean --environment lean-4.31.0
# Pipeline usage
cat theorem.lean | axle check - --environment lean-4.31.0
# Exit non-zero if code is invalid
axle check theorem.lean --strict --environment lean-4.31.0
# Use in shell conditionals
if axle check theorem.lean --strict --environment lean-4.31.0 > /dev/null; then
    echo "Valid Lean code"
fi

HTTP API

curl -s -X POST https://axle.axiommath.ai/api/v1/check \
    -d '{"content": "import Mathlib\n#eval 2+2", "environment": "lean-4.28.0"}' | jq

Example Response

{
  "okay": true,
  "content": "import Mathlib\n\n#eval 2+2\n",
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": ["4\n"]
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "timings": {
    "parse_ms": 30,
    "total_ms": 62
  },
  "failed_declarations": []
}