← All models

Aristotle

Harmonic

Aristotle is Harmonic's automated theorem-proving system, combining Lean proof search, informal reasoning that generates and formalizes lemmas, and a dedicated geometry solver. It accepts natural-language, Lean 4, and photo inputs and produces natural-language answers and machine-verifiable Lean 4 proofs. Its technical system report was published in October 2025; the June 2024 research announcement does not establish a public release date for this artifact.

Benchmark scores