# extract_theorems Deprecated `extract_theorems` is deprecated and will be removed in a future release. Use [`extract_decls`](https://axle.axiommath.ai/v1/docs/tools/extract_decls/) instead, which supports all declaration kinds (def, theorem, lemma, abbrev, instance, structure, etc.). Split a file containing one or more theorems into smaller units, each containing a single theorem along with any required dependencies. ## Input Parameters `content` · str · required · Lean source code The Lean source code to be processed by this tool. `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). `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 `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 extraction tool Messages from the extraction tool with `errors`, `warnings`, and `infos` lists. Errors here indicate tool-specific issues (not Lean compilation errors). `documents` · dict · Theorem names mapped to self-contained documents Dictionary mapping theorem names to self-contained Lean code documents. Each key is a theorem name, and the value is a self-contained breakdown of the theorem, including a content field containing that theorem plus all dependencies it needs (imports, definitions, etc.). `timings` · dict · Execution timing breakdown Timing information in milliseconds for various stages of processing. ## Document Fields Each document in the `documents` dictionary contains: `kind` · str · The kind of declaration The kind of the declaration. For `extract_theorems`, this is always `"theorem"`. For `extract_decls`, possible values are: `theorem`, `def`, `abbrev`, `axiom`, `opaque`, `structure`, `class`, `class inductive`, `inductive`, `instance`, `example`, `unknown`. `declaration` · str · The declaration source code The raw source code of this declaration. `content` · str · Standalone content including declaration and dependencies Complete, self-contained Lean code that includes the declaration and all its local dependencies. Can be compiled independently. **Empty** when the request specifies `names` or `indices`. In that mode only the selected declarations are returned and the unselected ones are _not_ elaborated (a large speedup), so their transitive dependencies can no longer be computed. A `tool_messages` warning is emitted; all other fields (`type`, dependency lists, `is_sorry`, etc.) are still populated. Call the tool without `names`/`indices` to get the self-contained `content`. `tokens` · list[str] · Raw tokens from the declaration The declaration's source code split into tokens. `signature` · str · Declaration signature (everything before the body) The declaration signature, e.g., `theorem foo (x : Nat) : x = x` or `def bar : Nat`. `type` · str · Pretty-printed type of the declaration The type of the declaration as pretty-printed by Lean. `type_hash` · int · Hash of the canonical type expression Hash of the canonical, alpha-invariant type expression. Useful for deduplication. `unfolded_type_hash` · int · Hash after unfolding local elaboration auxiliaries Hash of the type after unfolding module-local elaboration auxiliaries; useful for deduplication. `type_depth` · int · Structural depth of the type expression The nesting depth of the declaration's type as a Lean expression. This field maxes out at 255. `term_depth` · int · Structural depth of the value expression The nesting depth of the declaration's value or proof as a Lean expression, or 0 when the declaration has no value. This field maxes out at 255. `is_sorry` · bool · Whether the declaration contains a sorry True if the declaration contains a `sorry`. `index` · int · 0-based index in original file Position of this declaration in the original file. Note: indices may not be contiguous (mutual definitions share indices). `line_pos` · int · 1-based line number where declaration starts Line number where the declaration begins. `end_line_pos` · int · 1-based line number where declaration ends Line number where the declaration ends. `proof_length` · int · Approximate number of tactics in proof Rough measure of proof complexity based on tactic count. Only meaningful for theorems/lemmas with tactic proofs. `tactic_counts` · dict[str, int] · Map of tactic names to occurrence counts Breakdown of which tactics are used and how often. Only meaningful for theorems/lemmas with tactic proofs. `wall_ms` · int · Wall-clock milliseconds to elaborate the command How long this command took to elaborate. This field reports wall-clock time, so it can vary from run to run. `heartbeats` · int · Heartbeats consumed elaborating the command Lean heartbeats consumed while elaborating this command. `local_type_dependencies` · list[str] · Local dependencies of the type Local declarations that the declaration's type depends on (non-transitive). `local_value_dependencies` · list[str] · Local dependencies of the body Local declarations that the declaration's body/proof depends on (non-transitive). `external_type_dependencies` · list[str] · Immediate external dependencies of the type External constants (builtins, imports) that appear in the type. `external_value_dependencies` · list[str] · Immediate external dependencies of the body External constants (builtins, imports) that appear in the body/proof. `local_syntactic_dependencies` · list[str] · Local constants explicitly written in source Local constants that appear literally in source (not from notation/macro expansion). `external_syntactic_dependencies` · list[str] · External constants explicitly written in source External constants that appear literally in source (not from notation/macro expansion). `declaration_messages` · dict · Messages specific to this declaration Lean messages (`errors`, `warnings`, `infos`) specific to this declaration in the original document. `theorem_messages` · dict · (Deprecated) Messages specific to this declaration Lean messages (`errors`, `warnings`, `infos`) specific to this declaration. For `extract_theorems`, this contains the same data as `declaration_messages`. For `extract_decls`, this is always empty.