---

name: aristotle description: Prove Lean 4 theorems using the Aristotle proof synthesis service. Use when the user mentions "aristotle", "prove", "fill sorries", or wants to automatically generate proofs for Lean files with sorry placeholders. allowed-tools:

• Bash
• Read
• Edit
• Write
• Glob
• Grep hooks: PreToolUse:
  • matcher: "Bash(aristotle prove-from-file:*)" hooks:
    • type: command command: ".claude/skills/aristotle/scripts/validate.sh"

---

Aristotle Theorem Prover

Aristotle is an LLM-powered proof synthesis service that generates verified Lean 4 proofs. Given a file with sorry placeholders, it returns either a complete proof, a counterexample if the statement is false, or an explanation of why it couldn't find a proof.

Features

• Automatic Proof Synthesis: Fills sorry placeholders with verified Lean 4 proofs
• Counterexample Finding: Automatically disproves false statements with counterexamples
• Natural Language Input: Convert problems from text/LaTeX/markdown using --informal mode
• Proof Guidance: Guide with natural language hints via PROVIDED SOLUTION: in doc comments
• Custom Tactics: Output may include negate_state and revert_all tactics

See submission-guide.md for detailed examples and best practices.

TUI Modes

The Aristotle terminal UI (aristotle command without arguments) provides four modes:

Instructions

1. Prepare the input file

Ensure your Lean file:

• Has sorry placeholders for theorems you want proved
• Uses admit for definitions or theorems to skip
• Contains no axiom declarations (Aristotle cannot verify these)
• Typechecks with lake env lean <file.lean>

Optionally add PROVIDED SOLUTION: hints in doc comments:

Copy/--
Given x, y ∈ [0, π/2], show that cos(sqrt(x ^ 2 + y ^ 2)) ≤ cos x * cos y.

PROVIDED SOLUTION:
Set r := sqrt(x^2 + y^2). If r > π/2, then the inequality holds trivially
since the LHS is at most 1 and the RHS is non-negative...
-/
theorem my_theorem : ... := by
  sorry

2. Run the validation script

Copy.claude/skills/aristotle/scripts/validate.sh <file.lean>

This checks for common issues before submission.

3. Submit to Aristotle

Copyaristotle prove-from-file <input_file> [options]

Key options:

4. Review the output

• Proofs filled: sorry replaced with proof tactics
• Counterexamples: False statements get a comment with proof of negation
• Errors: See troubleshooting.md for fixes

5. Handle partial progress

If Aristotle hits budget limits or only solves some theorems, see troubleshooting.md for the recovery workflow.

Examples

Basic usage

Copyaristotle prove-from-file Problems/Example.lean

With additional context

Copyaristotle prove-from-file Problems/Hard.lean --context-folder ./notes/

Natural language input

Copyaristotle prove-from-file problem.txt --informal --formal-input-context context.lean

Full workflow example

Copy# 1. Validate the file
.claude/skills/aristotle/scripts/validate.sh Problems/my_theorem.lean

# 2. Submit to Aristotle
aristotle prove-from-file Problems/my_theorem.lean

# 3. Check the output
lake env lean Problems/my_theorem_aristotle.lean

How It Works

Aristotle uses a project-based workflow:

1. Create: Initialize a project with optional context files
2. Add Context: Attach dependency files (up to 10 per request, unlimited requests)
3. Solve: Submit the problem for processing
4. Poll: Check status until completion
5. Download: Retrieve the solved proof file

Project Status Values

NOT_STARTED → QUEUED → IN_PROGRESS → COMPLETE

Jobs may also enter FAILED (unrecoverable) or PENDING_RETRY (auto-recovering). See troubleshooting.md if a job seems stuck.

Input Modes

For informal mode, use --formal-input-context <file.lean> to provide type definitions and imports.

Technical Limits

Required Project Files

Aristotle validates your Lean project structure. Ensure you have:

• lakefile.toml or lakefile.lean
• lean-toolchain matching Aristotle's version

Automatic Import Resolution

By default (auto_add_imports=True), Aristotle:

1. Detects your project root from lakefile.toml
2. Parses imports in your input file
3. Recursively discovers all local dependencies
4. Uploads them as context automatically

To disable this and manually specify context files, use --context-files (mutually exclusive with auto-imports).

SDK Validation

The SDK automatically:

• Validates file paths are within the Lean project
• Enforces the 100 MB per-file limit
• Checks for required project structure files
• Resolves relative paths to absolute paths

Reference

All CLI options

Environment

Requires ARISTOTLE_API_KEY environment variable. Automatically loaded from .env when entering the nix shell.

Version compatibility

• Lean toolchain: leanprover/lean4:v4.24.0
• Mathlib: v4.24.0 (Oct 14, 2025) - commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7

Additional Resources

• submission-guide.md - Best practices for crafting submissions
• troubleshooting.md - Error handling and debugging
• python-api.md - Python SDK (aristotlelib) documentation
• openapi.yaml - REST API specification