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
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
Converted and distributed by TomeVault — claim your Tome and manage your conversions.
1---2name: zealousear-claude-skills-aristotle-prover3description: Aristotle Prover Skill4---56# Aristotle Prover Skill78## When to Use910- User wants to **formally prove** a mathematical statement (convergence, bounds, correctness)11- User wants to **verify** whether a claim is true or find a **counterexample**12- User wants to **formalize** natural language math into Lean 413- User has a **Lean file with `sorry`** stubs to fill14- User wants to **prove algorithm correctness** (sorting, optimization, numerical methods)15- User asks about **regret bounds**, **estimator properties**, **convergence guarantees**1617## When NOT to Use1819- General coding tasks (use normal Claude Code)20- Data analysis, ML training, visualization21- Non-mathematical questions22- Tasks that don't benefit from formal verification2324## Invocation2526```27/prove <natural language math question or file path>28```2930## Architecture3132```33User prompt34 |35 v36[Prompt Translator] -- Claude converts user's question into37 | an optimal Aristotle-compatible prompt38 | (formal Lean or structured informal)39 v40[aristotle_submit.py] -- Submits to Aristotle API, polls for result41 |42 v43[Solution] -- Lean 4 proof or counterexample returned to user44```4546## Capabilities47481. **Informal mode**: Natural language -> Aristotle formalizes and proves492. **Formal mode**: Lean 4 theorem with `sorry` -> Aristotle fills proofs503. **Hybrid mode**: Lean theorem + English proof hints (PROVIDED SOLUTION)514. **Counterexample detection**: When statements are false, returns proof of negation5253## Requirements5455- `aristotlelib` Python package (v0.7.0+)56- `ARISTOTLE_API_KEY` environment variable set57- Python 3.10+5859## File Structure6061```62~/.claude/skills/aristotle-prover/63├── SKILL.md # This file64├── scripts/65│ └── aristotle_submit.py # API submission + polling script66├── settings/67│ └── prompt-templates.json # Domain-specific prompt templates68└── references/69 ├── lean-patterns.md # Common Lean 4 patterns for translation70 └── prompt-guide.md # How to write effective Aristotle prompts71```7273---74> Converted and distributed by [TomeVault](https://tomevault.io/claim/zealousear) — claim your Tome and manage your conversions.75<!-- tomevault:4.0:skill_md:2026-04-14 -->
Run npx skillmds@latest add tomevault-io/zealousear-claude-skills-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.
Aristotle Prover Skill It is listed under Coding & Dev Tools on SkillMD.
This skill has not completed SkillMD's automated safety review yet. Independent scanners report: SkillSpector: PASS, Skill Scanner: PASS. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.
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.
Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.
tomevault-io (@tomevault-io) published this skill. Their other Agent Skills are listed on their SkillMD profile.
tomevault-io