Unix-style command-line tools for AXLE
validate a Lean proof against a formal statement
axle verify_proof FORMAL_STATEMENT CONTENT [OPTIONS]
# Basic usage
axle verify-proof statement.lean proof.lean --environment lean-4.21.0
# With permitted sorries
axle verify-proof statement.lean proof.lean --permitted-sorries helper1,helper2 --environment lean-4.21.0
# Pipeline usage
cat proof.lean | axle verify-proof statement.lean - --environment lean-4.21.0
# Exit non-zero if proof is invalid
axle verify-proof statement.lean proof.lean --strict --environment lean-4.21.0
# Use in shell conditionals
if axle verify-proof statement.lean proof.lean --strict --environment lean-4.21.0 > /dev/null; then
echo "Proof valid"
fi
# Specify different environment
axle verify-proof statement.lean proof.lean --environment lean-4.25.1evaluate Lean code and report all messages
axle check CONTENT [OPTIONS]
# Basic usage
axle check theorem.lean --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle check - --environment lean-4.21.0
# Exit non-zero if code is invalid
axle check theorem.lean --strict --environment lean-4.21.0
# Use in shell conditionals
if axle check theorem.lean --strict --environment lean-4.21.0 > /dev/null; then
echo "Valid Lean code"
fisplit file into separate theorems with dependencies
axle extract_theorems CONTENT [OPTIONS]
# Extract to default directory
axle extract-theorems combined.lean --environment lean-4.21.0
# Extract to custom directory
axle extract-theorems combined.lean -o my_theorems/ --environment lean-4.21.0
# Force overwrite
axle extract-theorems combined.lean -o my_theorems/ -f --environment lean-4.21.0
# Pipeline usage
cat combined.lean | axle extract-theorems - -o output/ --environment lean-4.21.0rename declarations in Lean code
axle rename CONTENT [OPTIONS]
# Rename using command-line mapping
axle rename theorem.lean --declarations foo=bar,helper=main_helper --environment lean-4.21.0
# Rename using JSON file
axle rename theorem.lean --declarations-file mapping.json --environment lean-4.21.0
# Save to file
axle rename theorem.lean --declarations foo=bar -o renamed.lean --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle rename - --declarations foo=bar --environment lean-4.21.0 | axle check - --environment lean-4.21.0convert between theorem and lemma keywords
axle theorem2lemma CONTENT [OPTIONS]
# Convert all theorems to lemmas
axle theorem2lemma theorems.lean --environment lean-4.21.0
# Convert specific theorems by name
axle theorem2lemma theorems.lean --names foo,bar --environment lean-4.21.0
# Convert to theorem instead
axle theorem2lemma lemmas.lean --target theorem --environment lean-4.21.0
# Convert first and last theorems
axle theorem2lemma theorems.lean --indices 0,-1 --environment lean-4.21.0
# Pipeline usage
cat theorems.lean | axle theorem2lemma - --environment lean-4.21.0 | axle check - --environment lean-4.21.0replace theorem proofs with sorry
axle theorem2sorry CONTENT [OPTIONS]
# Convert all theorems to sorry
axle theorem2sorry solution.lean -o problem.lean --environment lean-4.21.0
# Convert specific theorems by name
axle theorem2sorry solution.lean --names main_theorem,helper --environment lean-4.21.0
# Pipeline usage
cat solution.lean | axle theorem2sorry - --names main_theorem --environment lean-4.21.0 > problem.leancombine multiple Lean files into a single file
axle merge FILE1 FILE2 ... [OPTIONS]
# Merge multiple files to stdout
axle merge theorem1.lean theorem2.lean theorem3.lean --environment lean-4.21.0
# Merge all .lean files in directory
axle merge *.lean -o combined.lean --environment lean-4.21.0
# Merge and check
axle merge *.lean --environment lean-4.21.0 | axle check - --environment lean-4.21.0simplify theorem proofs
axle simplify_theorems CONTENT [OPTIONS]
# Simplify all theorems
axle simplify-theorems complex.lean --environment lean-4.21.0
# Simplify specific theorems
axle simplify-theorems complex.lean --names main_theorem,helper --environment lean-4.21.0
# Apply only specific simplifications
axle simplify-theorems complex.lean --simplifications remove_unused_tactics --environment lean-4.21.0
# Pipeline usage
cat complex.lean | axle simplify-theorems - --environment lean-4.21.0 | axle check - --environment lean-4.21.0repair broken theorem proofs
axle repair_proofs CONTENT [OPTIONS]
# Repair all theorems
axle repair-proofs broken.lean --environment lean-4.21.0
# Repair specific theorems
axle repair-proofs broken.lean --names main_theorem,helper --environment lean-4.21.0
# Apply only specific repairs
axle repair-proofs broken.lean --repairs remove_extraneous_tactics --environment lean-4.21.0
# Pipeline usage
cat broken.lean | axle repair-proofs - --environment lean-4.21.0 | axle check - --environment lean-4.21.0extract have statements to standalone lemmas
axle have2lemma CONTENT [OPTIONS]
# Extract all have statements
axle have2lemma theorem.lean --environment lean-4.21.0
# Extract from specific theorems
axle have2lemma theorem.lean --names main_proof,helper --environment lean-4.21.0
# Include proof bodies in extracted lemmas
axle have2lemma theorem.lean --include-have-body --environment lean-4.21.0
# Reconstruct callsites (replace have with lemma call)
axle have2lemma theorem.lean --reconstruct-callsite --environment lean-4.21.0
# Skip context cleanup
axle have2lemma theorem.lean --no-include-whole-context --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle have2lemma - --environment lean-4.21.0 | axle check - --environment lean-4.21.0replace have statements with sorry
axle have2sorry CONTENT [OPTIONS]
# Replace all have statements
axle have2sorry theorem.lean --environment lean-4.21.0
# Replace from specific theorems
axle have2sorry theorem.lean --names main_proof,helper --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle have2sorry - --environment lean-4.21.0 | axle check - --environment lean-4.21.0extract sorries and errors to standalone lemmas
axle sorry2lemma CONTENT [OPTIONS]
# Extract all sorries and errors
axle sorry2lemma theorem.lean --environment lean-4.21.0
# Extract from specific theorems
axle sorry2lemma theorem.lean --names main_proof,helper --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle sorry2lemma - --environment lean-4.21.0 | axle check - --environment lean-4.21.0attempt to disprove theorems by proving the negation
axle disprove CONTENT [OPTIONS]
# Disprove all theorems
axle disprove theorems.lean --environment lean-4.21.0
# Disprove specific theorems by name
axle disprove theorems.lean --names main_theorem,helper --environment lean-4.21.0
# Disprove specific theorems by index
axle disprove theorems.lean --indices 0,-1 --environment lean-4.21.0
# Pipeline usage
cat theorems.lean | axle disprove - --environment lean-4.21.0standardize Lean file formatting
axle normalize CONTENT [OPTIONS]
# Normalize a file
axle normalize theorem.lean --environment lean-4.21.0
# Normalize and save to file
axle normalize theorem.lean -o normalized.lean --environment lean-4.21.0
# Apply only specific normalizations
axle normalize theorem.lean --normalizations remove_sections,expand_decl_names --environment lean-4.21.0
# Pipeline usage
cat theorem.lean | axle normalize - --environment lean-4.21.0 | axle merge - other.lean --environment lean-4.21.0
# Disable failsafe to always return normalized output
axle normalize theorem.lean --no-failsafe --environment lean-4.21.0thorough proof validation using third-party tool
axle comparator FORMAL_STATEMENT CONTENT [OPTIONS]
# Basic usage
axle comparator statement.lean solution.lean --environment lean-4.21.0
# With memory limit
axle comparator statement.lean solution.lean --memory-limit-mb 4096 --environment lean-4.21.0
# Pipeline usage
cat solution.lean | axle comparator statement.lean - --environment lean-4.21.0
# Exit non-zero if solution is invalid
axle comparator statement.lean solution.lean --strict --environment lean-4.21.0
# Use in shell conditionals
if axle comparator statement.lean solution.lean --strict --environment lean-4.21.0 > /dev/null; then
echo "Solution valid"
fi