Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
git clone --depth 1 https://github.com/afhverjuekki/claude-code-aristotle-pluginWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/commands/afhverjuekki/claude-code-aristotle-plugin/aristotle)<a href="https://agentmods.dev/commands/afhverjuekki/claude-code-aristotle-plugin/aristotle"><img src="https://agentmods.dev/badge/commands/afhverjuekki/claude-code-aristotle-plugin/aristotle.svg" alt="Measured on agentmods" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00015 | $0.00681 |
| Opus 5 | $0.00008 | $0.00341 |
| Sonnet 5 | $0.00003 | $0.00136 |
| Haiku 4.5 | $0.00002 | $0.00068 |
Grade A, and why
aristotle scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 7d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 90 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Aristotle Lean 4 Formalization
Load the aristotle-workflow skill for comprehensive guidance.
Workflow Overview
Aristotle is a cloud-based theorem prover that formalizes proofs to Lean 4. It works best when given an informal proof to formalize, not when asked to discover proofs from scratch.
If Given a Lean File ($ARGUMENTS)
-
Read the file: @$1
-
Identify theorems with
sorryplaceholders -
For each theorem:
- Check if docstring contains
PROVIDED SOLUTIONhint - If no hint, ask user for informal proof strategy
- Add hint to docstring
- Check if docstring contains
-
Create standalone file if needed (custom library imports won't compile in Aristotle's cloud)
-
Submit to Aristotle:
uvx --from aristotlelib aristotle prove-from-file "$1" \
--no-validate-lean-project --no-auto-add-imports
- After Aristotle completes (3-6 min queue):
- Review the output file (
*_aristotle.lean) - Verify proofs with
#print axioms theorem_name - Check for
sorryAxcontamination
- Review the output file (
If Given a Theorem Description
Follow the Erdos-style workflow:
Step 1: Write Informal Proof
Draft a rigorous informal proof first. Break into small lemmas.
Step 2: Create Lean Scaffold
/--
[Informal proof here]
PROVIDED SOLUTION
[Specific hints: lemmas to use, induction strategy, etc.]
-/
theorem theorem_name : [statement] := by
sorry
Step 3: Submit to Aristotle
uvx --from aristotlelib aristotle prove-from-file theorem.lean \
--no-validate-lean-project --no-auto-add-imports
Step 4: Verify and Fix
- Check
#print axiomsfor sorryAx - Fix any Lean warnings
- Adapt proof back to project if needed
Critical Reminders
- Aristotle runs in cloud: Lean 4.24.0 + mathlib 4.24.0
- Custom imports fail: Create standalone files with inlined definitions
- Upstream sorries contaminate: Verify
#print axiomsshows nosorryAx - Queue time: Expect 3-6 minutes
- Provide hints: Break proofs into small lemmas in docstrings
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 7d ago First seen · 90 lines · 15 tokens per session scan A d1481dd2b506
aristotle is a command published in the GitHub repository afhverjuekki/claude-code-aristotle-plugin (10 stars, last pushed 8mo ago), licensed MIT. It adds 15 tokens to every session and 681 once invoked, about $0.0001 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.
Other commands, from other repositories
xray
Multi-dimensional paper audit — spawns 5 parallel sub-agents to check numerical accuracy, terminology consistency, code-paper alignment, citation accuracy, and evaluation integrity.
derive
Save a clean reference derivation of a target equation or theorem to derivations/. Draws from course materials (textbook, lecture notes) rather than testing the user.
prove-dev
Generate Lean 4 proof obligations from a Z specification.
b-animate-dev
Animate and model-check a B machine with probcli.
paper-trail-ingest
Ingest the citations of one SOTA into the registry. Extracts bibliographic sections, parses citations via the citation-parser sub-agent, resolves DOI via Crossref/S2, deduplicates against the registry, creates new candidate refs, and substitutes free-text citations with [[wikilinks]]. Required first step to make a…
paper-trail-new-paper
Start writing an academic paper (IMRaD structure) on a topic, with anti-hallucination citation verification at every step. Builds on existing audited SOTAs.