Leverage an IMO gold-medal-level engine to solve the most complex formal reasoning problems.

Aristotle seamlessly integrates into your project, automatically leveraging your entire library of theorems and definitions, lake dependencies, and Mathlib.

Aristotle can follow your lead in Lean4 or English. It can fill in the holes of your formal proof, even completing more than one sorry in a single theorem. Aristotle can also follow your English proofs - just add a comment above the statement you are proving, tagged with “PROVIDED SOLUTION.”

Aristotle provides counterexamples when the statement is incorrect, helping you find logical errors, missed edge cases, or even misformalizations.