# 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`](https://axle.axiommath.ai/v1/docs/tools/verify_proof/) instead, which folds those failures into `okay`.

## 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`](https://axle.axiommath.ai/v1/docs/tools/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`](https://axle.axiommath.ai/v1/docs/tools/verify_proof/) to treat them as errors.

`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.

`timings` · dict · Execution timing breakdown  
Timing information in milliseconds for various stages of processing.