skill-zealousear-claude-skills-aristotle-prover · by Install
$ agentstack add skill-zealousear-claude-skills-aristotle-prover ✓ scanned · ✓ verified, works with Claude Code, Cursor, and more.
Security review
✓ PassedNo issues found. Passed automated security review. · v0.1.0 How review works →
- ✓ Prompt-injection patterns
- ✓ Secret / credential exfiltration
- ✓ Dangerous shell & filesystem operations
- ✓ Untrusted network calls
- ✓ Known-malicious package signatures
What it can access
- ✓ Network access No
- ✓ Filesystem access No
- ✓ Shell / process execution No
- ✓ Environment & secrets No
- ✓ Dynamic code execution No
From automated source analysis of v0.1.0. “Used” means the capability is present in the source — more access means more to trust, not that it’s unsafe.
Verified badge
Passed review? Show it. Paste this badge into your README, it links to the public security report.
Links to your public security report.[](https://agentstack.voostack.com/security/report/skill-zealousear-claude-skills-aristotle-prover) Reliability & compatibility
Declared compatibility
Compatibility is declared by the source manifest. End-to-end runtime verification is coming, see below.
We're building live execution health for every listing: tool-call success rate, median latency, uptime, and last-checked timestamps, measured, not self-reported. It isn't live yet, so we don't show numbers we can't stand behind.
How agent discovery & health will work →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
sorrystubs 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 userCapabilities
- 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
aristotlelibPython package (v0.7.0+)ARISTOTLE_API_KEYenvironment 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 promptsSource & license
This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.
- Author: ZealousEar
- Source: ZealousEar/claude-skills
- License: MIT
Install and usage instructions live in the source repository linked above.
Reviews
No reviews yet, be the first.
Write a review
Versions
- v0.1.0 Imported from the upstream source.