How do I install the Aristotle Prover skill?

Run npx skillmds add zealousear/aristotle-prover in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Aristotle Prover safe to use?

This skill has not completed SkillMD's automated safety review yet. Capability flags: executes scripts. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Aristotle Prover?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Aristotle Prover free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Aristotle Prover?

ZealousEar (@zealousear) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Aristotle Prover by zealousear — Agent Skill

Name: Aristotle Prover
Rating: 4.5 (4 reviews)
Author: ZealousEar

Aristotle Prover

Translates natural language mathematical questions into optimal prompts for Harmonic's Aristotle formal theorem prover, submits them via the aristotlelib API, and returns the verified Lean 4 proof or counterexample.

ZealousEar 64cf62f 5 files · 16.7 KB Updated Sep 10, 2026

File contents

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 <natural language math question or file path>

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

Informal mode: Natural language -> Aristotle formalizes and proves
Formal mode: Lean 4 theorem with sorry -> Aristotle fills proofs
Hybrid mode: Lean theorem + English proof hints (PROVIDED SOLUTION)
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

---name: aristotle-proverdescription: Translates natural language mathematical questions into optimal prompts for Harmonic's Aristotle formal theorem prover, submits them via the aristotlelib API, and returns the verified Lean 4 proof or counterexample.---# 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 <natural language math question or file path>```## 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```## Capabilities1. **Informal mode**: Natural language -> Aristotle formalizes and proves2. **Formal mode**: Lean 4 theorem with `sorry` -> Aristotle fills proofs3. **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```

Frequently asked questions