# Aristotle Prover

> >

- **Type:** Skill
- **Install:** `agentstack add skill-zealousear-claude-skills-aristotle-prover`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ZealousEar](https://agentstack.voostack.com/s/zealousear)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [ZealousEar](https://github.com/ZealousEar)
- **Source:** https://github.com/ZealousEar/claude-skills/tree/main/claude-code/aristotle-prover

## Install

```sh
agentstack add skill-zealousear-claude-skills-aristotle-prover
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# Aristotle Prover Skill

## When to Use

- User wants to **formally prove** a mathematical statement (convergence, bounds, correctness)
- User wants to **verify** whether a claim is true or find a **counterexample**
- User wants to **formalize** natural language math into Lean 4
- User has a **Lean file with `sorry`** stubs to fill
- User wants to **prove algorithm correctness** (sorting, optimization, numerical methods)
- User asks about **regret bounds**, **estimator properties**, **convergence guarantees**

## When NOT to Use

- General coding tasks (use normal Claude Code)
- Data analysis, ML training, visualization
- Non-mathematical questions
- Tasks that don't benefit from formal verification

## Invocation

```
/prove 
```

## Architecture

```
User prompt
    |
    v
[Prompt Translator] -- Claude converts user's question into
    |                   an optimal Aristotle-compatible prompt
    |                   (formal Lean or structured informal)
    v
[aristotle_submit.py] -- Submits to Aristotle API, polls for result
    |
    v
[Solution] -- Lean 4 proof or counterexample returned to user
```

## Capabilities

1. **Informal mode**: Natural language -> Aristotle formalizes and proves
2. **Formal mode**: Lean 4 theorem with `sorry` -> Aristotle fills proofs
3. **Hybrid mode**: Lean theorem + English proof hints (PROVIDED SOLUTION)
4. **Counterexample detection**: When statements are false, returns proof of negation

## Requirements

- `aristotlelib` Python package (v0.7.0+)
- `ARISTOTLE_API_KEY` environment variable set
- Python 3.10+

## File Structure

```
~/.claude/skills/aristotle-prover/
├── SKILL.md                    # This file
├── scripts/
│   └── aristotle_submit.py     # API submission + polling script
├── settings/
│   └── prompt-templates.json   # Domain-specific prompt templates
└── references/
    ├── lean-patterns.md        # Common Lean 4 patterns for translation
    └── prompt-guide.md         # How to write effective Aristotle prompts
```

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [ZealousEar](https://github.com/ZealousEar)
- **Source:** [ZealousEar/claude-skills](https://github.com/ZealousEar/claude-skills)
- **License:** MIT

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-zealousear-claude-skills-aristotle-prover
- Seller: https://agentstack.voostack.com/s/zealousear
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.