Aristotle Plugin for Claude Code

A Claude Code plugin for theorem proving and code verification using Aristotle AI from Harmonic.

Installation

# Step 1: Add the marketplace
claude plugin marketplace add afhverjuekki/claude-code-aristotle-plugin

# Step 2: Install the plugin
claude plugin install aristotle@aristotle-plugin

Alternative methods:

# Direct from GitHub
claude --plugin-dir https://github.com/afhverjuekki/claude-code-aristotle-plugin

# Local development
git clone https://github.com/afhverjuekki/claude-code-aristotle-plugin.git
claude --plugin-dir ./claude-code-aristotle-plugin

---

Overview

Aristotle has achieved:

• Gold-medal IMO 2025 performance (5/6 problems)
• 96.8% accuracy on VERINA benchmark for code verification
• Solved open Erdos problems that were unsolved for decades
• Contributed to Mathlib, Polynomial Freiman-Ruzsa, and Quantum Stein's Lemma

This plugin provides:

• Two workflows: Theorem proving and code verification
• Skill knowledge about Aristotle's architecture and best practices
• Specialized agents for proof and code verification
• Helper scripts for common tasks

Two Main Use Cases

1. Theorem Proving (Mathematics)

Formalize mathematical proofs to Lean 4.

/aristotle Prove that √2 is irrational

2. Code Verification (Software Engineering)

Verify algorithm correctness with formal specifications.

/verify-code my-sorting-algorithm.lean

---

Quick Start: Theorem Proving

Invoke the Command

/aristotle my-theorem.lean

Follow the Erdos-Style Workflow

1. Write informal proof first
2. Add hints with PROVIDED SOLUTION in docstrings
3. Create standalone file (if using custom libraries)
4. Submit to Aristotle
5. Verify proofs with #print axioms

Example

/--
PROVIDED SOLUTION
Use induction on n. Apply Nat.add_comm for the base case.
-/
theorem sum_formula (n : Nat) : 2 * sum n = n * (n + 1) := by
  sorry

---

Quick Start: Code Verification

Invoke the Command

/verify-code selection-sort.lean

Follow the VERINA-Style Workflow

1. Define precondition - Input constraints
2. Implement algorithm - The code to verify
3. Define postcondition - Required output properties
4. State specification theorem
5. Submit to Aristotle

Example

-- Precondition: no special requirements
def sort_precond (arr : Array Int) : Prop := True

-- Algorithm implementation
def selectionSort (arr : Array Int) (h : sort_precond arr) : Array Int := ...

-- Postcondition: sorted + permutation
def sort_postcond (arr result : Array Int) (h : sort_precond arr) : Prop :=
  List.Pairwise (· ≤ ·) result.toList ∧ result.toList.Perm arr.toList

-- Specification theorem
theorem selectionSort_correct (arr : Array Int) (h : sort_precond arr) :
    sort_postcond arr (selectionSort arr h) h := by
  sorry

Verification Outcomes

• Proof found: Algorithm is correct
• Counterexample: Bug detected (e.g., use [4, 1, 2, 1, 4], 2)
• False detected: Specification or implementation is wrong

---

Components

Commands

Command	Description
/aristotle	Theorem proving workflow
/verify-code	Code verification workflow

Agents

Agent	Purpose	Color
proof-verifier	Validates Aristotle proofs, checks sorryAx	Green
code-verifier	Sets up VERINA-style specifications	Cyan

Skill: aristotle-workflow

Comprehensive knowledge covering:

• Erdos-style theorem proving pipeline
• VERINA-style code verification structure
• Writing effective hints
• Creating standalone files
• Troubleshooting common issues

Triggers on: "prove theorem", "verify algorithm", "use Aristotle", "check correctness"

Scripts

Script	Purpose
verify-proof.sh	Check for sorryAx contamination
create-standalone.sh	Generate theorem file template

---

Critical Limitations

1. Cloud Environment

Aristotle runs in Harmonic's cloud:

• Lean 4.24.0 + Mathlib 4.24.0
• Custom library imports will fail

Solution: Create standalone files with inlined definitions.

2. Upstream Sorries

If your codebase has sorries, Aristotle may exploit them.

Always verify:

#print axioms my_theorem
-- Should NOT show: sorryAx

3. Queue Time

Expect 3-6 minutes for job completion.

---

Writing Good Hints

Add PROVIDED SOLUTION in docstrings:

/--
PROVIDED SOLUTION
Use induction on array size. Each iteration:
1. Finds minimum in unsorted suffix
2. Swaps to correct position
3. Maintains sorted prefix invariant
Apply swap_preserves_perm and sorted_prefix_extends.
-/
theorem algorithm_correct ... := by sorry

Best practices:

• Reference specific lemmas
• Describe strategy (induction, contradiction, etc.)
• Break into small steps
• Mention key insights

---

CLI Reference

# Standalone file (custom libraries)
uvx --from aristotlelib aristotle prove-from-file FILE.lean \
  --no-validate-lean-project --no-auto-add-imports

# Mathlib project
uvx --from aristotlelib aristotle prove-from-file lib/File.lean

# With context folder
uvx --from aristotlelib aristotle prove-from-file FILE.lean \
  --context-folder lib/

# Fire and forget
uvx --from aristotlelib aristotle prove-from-file FILE.lean --no-wait

---

Verified Algorithms (VERINA Benchmark)

Aristotle has successfully verified:

• Selection sort (in-place sorting correctness)
• Run-length encoding (string compression)
• Longest increasing subsequence (dynamic programming)
• 160+ more algorithm implementations

And detected bugs like the top-k frequent elements error in the VERINA benchmark.

---

Architecture

Aristotle has three subsystems:

1. Lean proof search - MCGS with 200B+ parameter transformer
2. Lemma-based reasoning - Decomposes and formalizes incrementally
3. Geometry solver - Yuclid (500x faster than AlphaGeometry-1)

See skills/aristotle-workflow/references/architecture.md for details.

---

Troubleshooting

Issue	Solution
"Import not found"	Create standalone file with inlined definitions
Proof depends on sorryAx	Fix upstream sorries or isolate in standalone file
"Block is false"	Theorem/specification is genuinely false
Long queue time	Normal is 3-6 min; use --no-wait for batch
Counterexample found	Check implementation, postcondition, or precondition

---

Version

1.1.0 (Added code verification support)

License

MIT