# Aristotle > Run Aristotle automated theorem prover on Lean files to fill sorry placeholders. Use when you have a file with sorries that needs automated proof search. Handles API setup, axiom import checks, and result verification. Use when this capability is needed. - Skill: `tomevault-io/aristotle` (Agent Skill, multi-file: 2 files) - Install (CLI): `npx skillmds@latest add tomevault-io/aristotle` - Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/aristotle/raw - Safety review: pending (external: skill-scanner PASS, skillspector PASS) - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Integrations & APIs - Author: tomevault-io (https://skillmd.com/u/tomevault-io) - Updated: 2026-09-17 - Page: https://skillmd.com/skills/tomevault-io/aristotle --- # Aristotle Automated Theorem Prover Run [Aristotle](https://aristotle.harmonic.fun) to automatically fill `sorry` placeholders in Lean 4 files. ## Workflow 1. **Validate file**: Check for `sorry` in the target file 2. **Check for axiom imports**: Aristotle may fail on files importing axiom-heavy modules 3. **Run Aristotle**: Submit file for proof search 4. **Apply results**: Replace sorries with generated proofs 5. **Verify**: Run `lake build` to confirm ## Axiom Import Checks Check for imports that may cause issues: ```bash grep -E "import.*Axiom|axiom " "path/to/file.lean" ``` If axiom imports are found, consider: - Moving the proof to a separate file - Using manual proof instead ## Usage Notes - Aristotle works best on pure computational proofs - May struggle with axiom-heavy modules - Always verify generated proofs compile --- > Converted and distributed by [TomeVault](https://tomevault.io/claim/arthur742ramos) — claim your Tome and manage your conversions.