Aristotle Automated Theorem Prover

This skill runs Aristotle to automatically fill sorry placeholders in Lean 4 files.

Quick Usage

code

/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

bash

grep -n "sorry" "path/to/file.lean"

Step 2: Run Aristotle

bash

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:

lean

/-
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:

bash

lake build ModuleName

Command Variations

Basic Usage

code

/aristotle Metatheory/Lambda/NewLemma.lean

With Custom Output

code

/aristotle Metatheory/Lambda/NewLemma.lean --output NewLemma_proved.lean

Interpreting Aristotle Output

Success Indicators

lean

/-
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

lean

/- 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:

bash

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