extract_theorems

Split a file containing one or more theorems into smaller units, each containing a single theorem along with any required dependencies.

Python API

result = await axle.extract_theorems(
    content="import Mathlib\ntheorem foo : 1 = 1 := rfl\ntheorem bar : 2 = 2 := rfl",
    environment="lean-4.26.0",
    ignore_imports=False,  # Optional
    timeout_seconds=120,   # Optional
)

print(result.content)  # The processed Lean code
for name, doc in result.documents.items():
    print(f"{name}: {doc.signature}")
    print(f"  Dependencies: {doc.local_value_dependencies}")

CLI

Usage: axle extract-theorems CONTENT [OPTIONS]

# Extract to default directory
axle extract-theorems combined.lean --environment lean-4.26.0
# Extract to custom directory
axle extract-theorems combined.lean -o my_theorems/ --environment lean-4.26.0
# Force overwrite
axle extract-theorems combined.lean -o my_theorems/ -f --environment lean-4.26.0
# Pipeline usage
cat combined.lean | axle extract-theorems - -o output/ --environment lean-4.26.0

HTTP API

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

Input Parameters

Name	Type	Required	Description
content	str	Yes	A string of Lean code
environment	str	Yes	Environment to use (e.g., "lean-4.26.0", "lean-4.25.1")
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
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
tool_messages	dict	Messages from extraction tool with errors, warnings, infos lists
documents	dict[str, Document]	Map of theorem names to document objects
timings	dict	Timing info: total_ms, parse_ms

Document Fields

Each document in the documents dictionary contains:

Name	Type	Description
declaration	str	The content of this theorem declaration
content	str	Standalone content including theorem and dependencies
tokens	list[str]	Raw tokens from the theorem
signature	str	Theorem signature (everything before proof body)
type	str	Pretty-printed type of the theorem
type_hash	int	Hash of the canonical (reduced, alpha-invariant) type expression
is_sorry	bool	Whether the theorem contains a sorry
index	int	0-based index in original file
line_pos	int	1-based line number where theorem starts
end_line_pos	int	1-based line number where theorem ends
proof_length	int	Approximate number of tactics in proof
tactic_counts	dict[str, int]	Map of tactic names to occurrence counts
local_type_dependencies	list[str]	Transitive local dependencies of the type
local_value_dependencies	list[str]	Transitive local dependencies of the proof
external_type_dependencies	list[str]	Immediate external dependencies of the type (e.g., builtins, from imports)
external_value_dependencies	list[str]	Immediate external dependencies of the proof (e.g., builtins, from imports)
local_syntactic_dependencies	list[str]	Local constants explicitly written in source (not from notation/macro expansion)
external_syntactic_dependencies	list[str]	External constants explicitly written in source (not from notation/macro expansion)
document_messages	dict	Messages from standalone document with errors, warnings, infos lists
theorem_messages	dict	Messages specific to the theorem with errors, warnings, infos lists

Note: The set of all index fields is NOT necessarily {0..n-1}. There may be missing or duplicate indices (for mutual definitions). Sort by index to get an ordered list.

Example Response

{
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl\n",
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "timings": {
    "total_ms": 92,
    "parse_ms": 87
  },
  "documents": {
    "foo": {
      "declaration": "theorem foo : 1 = 1 := rfl",
      "content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl",
      "tokens": ["theorem", "foo", ":", "1", "=", "1", ":=", "rfl"],
      "signature": "theorem foo : 1 = 1",
      "type": "1 = 1",
      "type_hash": 12345678901234567890,
      "is_sorry": false,
      "index": 0,
      "line_pos": 1,
      "end_line_pos": 1,
      "proof_length": 1,
      "tactic_counts": {},
      "local_value_dependencies": [],
      "local_type_dependencies": [],
      "external_value_dependencies": ["rfl", "Nat", "OfNat.ofNat", "instOfNatNat"],
      "external_type_dependencies": ["Eq", "Nat", "OfNat.ofNat", "instOfNatNat"],
      "local_syntactic_dependencies": [],
      "external_syntactic_dependencies": ["rfl"],
      "document_messages": {"errors": [], "warnings": [], "infos": []},
      "theorem_messages": {"errors": [], "warnings": [], "infos": []}
    }
  }
}