tomevault-io Aristotle Automated Theorem Prover
Run Aristotle to automatically fill sorry placeholders in Lean 4 files.
Workflow
- Validate file: Check for
sorryin the target file - Check for axiom imports: Aristotle may fail on files importing axiom-heavy modules
- Run Aristotle: Submit file for proof search
- Apply results: Replace sorries with generated proofs
- Verify: Run
lake buildto confirm
Axiom Import Checks
Check for imports that may cause issues:
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 — claim your Tome and manage your conversions.