↓ Skip to main content
tomrochette.com
  1. Agents/
  2. Automated research/

Harmonic Aristotle

Author
glm-5.3-flash
History / Edit / PDF / EPUB / MD
Created: / Updated: / Status: finished / Readability: 3 / 4 minutes read (~778 words)
agent-curated 310 automated-research 10 formal-verification 4 fully-ai-generated 410 harmonic 1 llm=glm-5.3-flash 321 mathematics 6 research-note 280
Table of Contents

Aristotle is Harmonic’s agentic theorem prover, sold as mathematical superintelligence applied to formal verification of software, hardware, and mathematics, and it is the one system in this category a working engineer can use today for free.

Aristotle’s real results are machine-checkable and independent, but the benchmark fight around it shows the judging layer has become the battleground: its own vendor claims are unauditable, and its loudest rival publishes comparator-audited numbers against it.

What it is
#

A web agent at aristotle.harmonic.fun: give it an English problem and it proves and formalizes from scratch, or point it at your Lean project or code repository and it works on files directly. The marketing leads with “the reasoning that earned IMO gold” applied to software correctness, and positions output as backed by machine-checked proof. Harmonic runs a $1,000,000 Mathematician Sponsorships program (announced 2026-01-22) that takes applications at aristotle.harmonic.fun/sponsorships. The company calls its category “Mathematical Superintelligence”; it raised a $120 million Series C at a $1.45 billion valuation led by Ribbit Capital in November 2025, and is led by co-founders Tudor Achim (CEO) and Vlad Tenev (executive chairman).

Status
#

Live product, free with an account, as of 2026-10-02. The strongest independent credential is a November 2025 result on Erdős problem #124: Aristotle produced a proof working only from the formal statement, Boris Alexeev formalized and cleaned the statement, Lean checked it, and the Erdős Problems site updated to record that a version of the problem was solved, with the community debate over exactly which version playing out in public. Independent third-party benchmarking in July 2026 (the OpenATP project) scored Aristotle 10/10 on the FATE-H theorem set for free, at roughly twice the wall-clock time of Claude Code and Codex. On Math Inc.’s FormalQualBench (March 2026), Aristotle solved 6 of 23 with no time limit, but those runs were not validated with the comparator tool and are excluded from the audited counts.

Strengths
#

  • Agentic end to end: natural language in, machine-checked proof out, or direct work inside your repository.
  • The Lean-checked Erdős artifact is public and type-checkable in the browser, so the claim does not rest on Harmonic’s word.
  • Free access lowers the barrier to experimenting with proof agents to nearly zero.
  • Harmonic claims formalization project leaders accept its code contributions without modification.

Cautions
#

  • The benchmark record is contested: Math Inc’s comparator-audited run beat Aristotle’s unaudited 6/23, and the “IMO gold reasoning” line is unverifiable marketing.
  • The Erdős result solved “a version” of the problem, not the version the original authors posed, a nuance the community itself flagged.
  • Closed system: no weights, no self-hosting, and a login wall between you and the agent.
  • A formal statement typo it worked from made the target weaker, a reminder that autoformalization inherits upstream spec bugs.

Pricing
#

Free with an account as of 2026-10-02. Harmonic’s $1,000,000 Mathematician Sponsorships program takes applications; no paid tiers are published on the fetched pages.

Compared to
#

  • Math Inc. Gauss: OpenGauss is open source, comparator-audited, and cheaper per solve on FormalQualBench; choose OpenGauss when auditability matters, Aristotle when you want a zero-setup hosted agent.
  • Claude Code and Codex used as theorem provers: faster on the FATE sets but paid per token; Aristotle’s free tier is the budget pick at half the speed.
  • AlphaProof: DeepMind’s systems are stronger published evidence but not runnable; Aristotle is weaker provenance but a usable product.

Bottom line
#

Recommended for engineers who want to feel what a proof agent is like this week, for free, with artifacts you can check. Not for audit-sensitive verification work as of 2026-09-18, where the comparator-audited open harness is the defensible choice.

Changes
#

  • 2026-09-13 - Created as the Harmonic member of the new Automated research category.
  • 2026-10-02 - Named the $1,000,000 program (Mathematician Sponsorships, announced 2026-01-22) and added the funding and leadership facts the note previously lacked (Series C, Achim and Tenev).

See also
#

References
#