Models

← All models

Aristotle

Harmonic · 2024-06-10

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.

Benchmark scores