| name | aristotle |
| description | Run Aristotle automated theorem prover on Lean files to fill sorry placeholders. Use when you have a file with sorries that needs automated proof search. Handles API setup and result verification. |
Aristotle Automated Theorem Prover
This skill runs Aristotle to automatically fill sorry placeholders in Lean 4 files.
Quick Usage
/aristotle path/to/file.lean
Project Policy Note
This repository has a "No Sorrys Allowed" policy. Aristotle is useful for:
- Development workflow (fill sorries before committing)
- Exploring proof strategies
- Verifying that automated provers can handle certain goals
Workflow
When the user invokes /aristotle, follow these steps:
Step 1: Validate the Target File
- Check file exists: Verify the specified
.lean file exists
- Check for sorries: Grep for
sorry in the file - if none, inform user
grep -n "sorry" "path/to/file.lean"
Step 2: Run Aristotle
export ARISTOTLE_API_KEY='arstl_hCSoWHQ4OwTccQbXeuRXOHF-UqIH8RtVMUjS2B_vIpI'
uvx --from aristotlelib aristotle.exe prove-from-file "path/to/file.lean" \
--output-file "path/to/file_aristotle.lean"
IMPORTANT - Long Processing Times:
- Aristotle can take 30+ minutes for complex proofs (e.g., substitution lemmas, normalization proofs)
- DO NOT kill the process prematurely - let it run to completion
- Run the command in the background with
run_in_background: true
- Periodically check progress by reading the output file
- Progress may stay at low percentages (1-10%) for extended periods while Aristotle searches for proofs
- Only consider it failed if it returns an error status, not just because it's taking a long time
Step 3: Report Results
After Aristotle completes, read the output file header to see what was proved:
/-
This file was edited by Aristotle.
...
The following was proved by Aristotle:
- theorem foo : ...
- theorem bar : ...
-/
Report to user:
- Number of theorems attempted
- Number successfully proved
- Any that failed or were skipped
Step 4: Verify Output
Try building to verify the proofs compile:
lake build ModuleName
Command Variations
Basic Usage
/aristotle Metatheory/Lambda/NewLemma.lean
With Custom Output
/aristotle Metatheory/Lambda/NewLemma.lean --output NewLemma_proved.lean
Interpreting Aristotle Output
Success Indicators
/-
The following was proved by Aristotle:
- theorem my_theorem : ...
-/
Common Proof Tactics
| Tactic | Meaning |
|---|
exact? | Found matching lemma (build to see suggestion) |
grind | Automation solved it |
simp | Simplification |
rfl | Reflexivity |
omega | Linear arithmetic |
decide | Decidable proposition |
Failure Indicators
/- Aristotle failed to load this code into its environment. -/
Cause: Syntax issues or import problems.
Environment Setup
The API key should be set in ~/.bashrc:
export ARISTOTLE_API_KEY='arstl_hCSoWHQ4OwTccQbXeuRXOHF-UqIH8RtVMUjS2B_vIpI'
Project-Specific Modules
Modules That Should Work Well
| Module | Description |
|---|
Rewriting/Basic.lean | Core ARS definitions |
Rewriting/Diamond.lean | Diamond property proofs |
Rewriting/Newman.lean | Newman's lemma |
Lambda/Term.lean | De Bruijn terms |
TRS/Syntax.lean | Expression syntax |
Complex Modules
| Module | Notes |
|---|
Lambda/Complete.lean | Complex substitution lemmas |
STLC/Normalization.lean | Logical relations proofs |
Troubleshooting
| Issue | Solution |
|---|
| API key error | Check ARISTOTLE_API_KEY is set |
| Timeout | Use --no-wait, check dashboard later |
exact? in output | Run lake build to see suggestions |
Example Session
User: /aristotle Metatheory/Lambda/NewLemma.lean
Claude:
- Reads file, finds 2 sorries
- Runs Aristotle (waits ~3-5 minutes)
- Reports: "Aristotle proved 2/2 theorems"
- Offers: "Want me to verify the output compiles?"
- Builds, reports success
