Aristotle Lean

Trit: -1 (MINUS) Domain: Formal Verification / Theorem Proving Provider: Harmonic (harmonic.fun)

Overview

Aristotle is an IMO Gold Medal level Lean4 theorem prover that fills sorry holes in proofs, auto-generates counterexamples for false statements, and integrates with Mathlib and lake dependencies.

API Configuration

Endpoint: aristotle.harmonic.fun
Auth: Auth0-based (requires signup/login at harmonic.fun)

Capabilities