Harmonic Aristotle

Status: assess | Maturity: production-ready | Last reviewed: 2026-03-20

What it does

Harmonic Aristotle is a cloud-based automated theorem prover that proves and formally verifies graduate- and research-level mathematical results using Lean 4. It converts natural-language problem statements into machine-checked formal proofs, and can fill sorry placeholders in existing Lean projects. Harmonic demonstrated Aristotle solving all six International Mathematical Olympiad 2025 problems and raised a $120M Series C in November 2025.

Key capabilities

• Fill sorries — submit a Lean 4 file and Aristotle replaces all sorry placeholders with verified proofs
• Formalize mathematics — convert a paper, textbook passage, or LaTeX file into Lean 4 proofs
• Prove from prompts — describe a theorem in plain English; Aristotle formalizes and proves it
• Find counterexamples — disprove a false statement and surface a concrete counterexample
• REST API and Python SDK — aristotlelib (v1.0.0, March 2026) provides CLI commands (aristotle submit, aristotle formalize, aristotle result) and programmatic access

Fit for Sheffield researchers

Primarily relevant to researchers in mathematics, theoretical computer science, and formal methods — a small but high-value audience. Potential applications include:

• Verifying proofs in pure mathematics research (algebra, number theory)
• Formal verification of algorithms and software specifications
• Automated proof assistance for graduate students learning Lean 4
• Hardware and software verification in engineering research

No Sheffield adoption is known. The Research Grant Programme may be worth exploring for relevant groups (e.g. the Verification group in Computer Science).

Licensing and access

Currently free to use via API key (sign up at aristotle.harmonic.fun). The Terms of Service prohibit using outputs to train other AI models. No institutional agreement, Jisc CHEST availability, or tiered pricing is currently published.

Trust and governance notes

Data is processed on US servers. Harmonic’s privacy policy references GDPR adequacy decisions and Standard Contractual Clauses for EU/UK data transfers, with a UK Data Transfer Addendum. However, no Data Processing Agreement template is publicly available — institutional review by IT Services / Research IT would be needed before using with sensitive research data. Rated unclear for GDPR compliance pending a formal DPA review.

Observed limitations

• Lean 4 only — no support for other proof assistants (Coq, Isabelle, Lean 3)
• Mathlib coverage gaps — results are less reliable in topology, probability, and linear algebra
• Human formalisation responsibility — the tool cannot verify that an English statement was correctly translated; researchers must validate the formalization step
• Cloud-only — no offline or self-hosted option; requires continuous internet access
• Proof jobs can be slow — complex theorems may take minutes to hours (asynchronous workflow recommended)
• Output restriction — cannot use Aristotle outputs to train any other model

Related tools

kosmos · google-co-scientist

Sources and evidence

• Aristotle product page: https://aristotle.harmonic.fun (accessed 2026-03-20)
• Harmonic company site: https://harmonic.fun (accessed 2026-03-20)
• Research paper: Aristotle: IMO-level Automated Theorem Proving — https://arxiv.org/abs/2510.01346
• aristotlelib Python SDK: https://pypi.org/project/aristotlelib/
• Harmonic $120M Series C: https://www.startupresearcher.com/news/harmonic-hits-unicorn-status-with-usd120-million-series-c (accessed 2026-03-20)
• IMO 2025 solutions repository: https://github.com/harmonic-ai/IMO2025