claude-code-aristotle-plugin

KO | EN

gitlite — search

#javascript #python #hacktoberfest #react #ai #typescript #llm #go #golang #android #machine-learning #rust #deep-learning #linux

claude-code-aristotle-plugin

★ 10 Open GitHub ↗

Aristotle AI plugin for Claude Code - theorem proving and code verification with Lean 4

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Aristotle Plugin for Claude Code

A Claude Code plugin for **theorem proving** and **code verification** using [Aristotle AI](https://aristotle.harmonic.fun/) from Harmonic.

## Installation

```bash
# 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:**

```bash
# 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
```lean
/--
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
```lean
-- 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**:
```lean
#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:

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

```bash
# 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](LICENSE)

claude-code-aristotle-plugin

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README