Harmonic (AI)
Last reviewed
Jun 7, 2026
Sources
No citations yet
Review status
Needs citations
Revision
v1 · 1,800 words
Improve this article
Add missing citations, update stale details, or suggest a clearer explanation.
Suggest edit
CtrlK
Last reviewed
Jun 7, 2026
Sources
No citations yet
Review status
Needs citations
Revision
v1 · 1,800 words
Add missing citations, update stale details, or suggest a clearer explanation.
Harmonic is an American artificial intelligence company building what it calls mathematical superintelligence (MSI), a system designed to reason about mathematics and related quantitative fields without producing false statements. Its flagship model, Aristotle, generates solutions in the Lean proof assistant language and checks them with a formal verifier, so that any output the system presents as proven has been machine-verified down to the axioms. The company was founded in 2023 by Tudor Achim, who serves as chief executive, and Vlad Tenev, the co-founder and chief executive of Robinhood, who serves as executive chairman. Harmonic drew wide attention in July 2025 when it reported that Aristotle had reached gold-medal-level performance on the problems of the 2025 International Mathematical Olympiad, with every submitted solution formally verified in Lean. It is based in Palo Alto, California.
Harmonic positions itself within the broader effort to apply artificial intelligence to rigorous reasoning. Its central thesis is that the hallucination problem of large language models can be eliminated in mathematics by requiring outputs to pass a formal check, an approach drawn from automated theorem proving rather than from open-ended text generation.
Harmonic was founded in 2023. Tudor Achim is co-founder and chief executive. Before Harmonic he co-founded and was chief technology officer of Helm.ai, an autonomous-driving software company, and earlier worked on machine learning at Quora. He holds a bachelor's degree in computer science from Carnegie Mellon University and was a doctoral candidate in computer science at Stanford University before leaving the program.
Vlad Tenev is co-founder and executive chairman. He is best known as the co-founder and chief executive of the retail brokerage Robinhood, a role he has continued to hold while backing and chairing Harmonic. Tenev has spoken publicly about a long-standing personal interest in mathematics, which he has cited as motivation for the venture. The pairing of a sitting public-company chief executive as chairman with an operating founder-chief executive is a defining feature of how the company is described in press coverage, which often refers to Harmonic as "the Robinhood CEO's math startup."
Aristotle is Harmonic's core system. Rather than emitting natural-language argument, it works in Lean 4, an open-source proof assistant and functional programming language in which a proof is a program that the Lean kernel either accepts or rejects. Harmonic's claim is that this makes the system effectively hallucination-free within the domains it supports: a proof that compiles is correct by construction, and the system flags rather than fabricates when it cannot complete an argument. Achim has described Aristotle as the first reasoning system available to the public that formally verifies its own output, and has said that within supported domains "we actually do guarantee that there's no hallucinations."
According to the company's technical report, posted to arXiv on October 1, 2025 under the title Aristotle: IMO-level Automated Theorem Proving, the system combines three components: a Lean proof-search engine; an informal-reasoning module that proposes and then formalizes intermediate lemmas, bridging from natural-language intuition to formal statements; and a dedicated geometry solver for the geometry problems that are awkward to express directly in Lean. The report states that the system reaches state-of-the-art results on automated-theorem-proving benchmarks with favorable scaling, and describes a synthetic-data pipeline in which the model generates its own problem-and-proof pairs to drive further training, a form of self-improvement that builds on ideas from reinforcement learning and mathematical reasoning research. This formal approach distinguishes Harmonic from most of the generative AI field and aligns it with the AI-for-science goal of verifiable machine-assisted discovery.
In July 2025 Harmonic announced that Aristotle had achieved gold-medal-level performance on the six problems of the 2025 International Mathematical Olympiad. Independent commentary and the company's own materials indicate that the system solved five of the six problems for a score of 35 points, the same tally reached by the systems from Google DeepMind and OpenAI, and above the gold-medal threshold for that year. All three systems failed Problem 6, a combinatorics problem. Harmonic published its formal Lean proofs and verification artifacts in a public GitHub repository.
The result came alongside parallel announcements from Google DeepMind, whose Gemini Deep Think model worked in natural language, and OpenAI, whose general-purpose model likewise produced natural-language proofs. Several important caveats attach to and differentiate these claims, and reporting on them deserves careful attribution:
In short, Harmonic's headline of "gold-medal-level performance" is best read as a strong but unofficial result whose chief advantage over its rivals is independent machine-checkability, offset by its reliance on manual formalization and an extended, non-competition time budget.
Harmonic raised roughly $295 million across three rounds in about 14 months, climbing to a reported $1.45 billion post-money valuation and unicorn status by late 2025.
| Round | Date | Amount | Post-money valuation | Lead investor(s) |
|---|---|---|---|---|
| Series A | September 2024 | $75 million | $325 million | Sequoia Capital (with Index Ventures) |
| Series B | July 2025 | $100 million | about $875 million | Kleiner Perkins |
| Series C | November 25, 2025 | $120 million | $1.45 billion | Ribbit Capital |
| Total | -- | about $295 million | -- | -- |
The Series C, announced on November 25, 2025, was led by Ribbit Capital with participation from Sequoia Capital, Index Ventures, Kleiner Perkins and, as a new investor, the Emerson Collective. Some outlets reported the July 2025 Series B valuation as about $900 million; the figure most commonly cited, including in TechCrunch's coverage, is $875 million. The company said the new capital would fund further development of its mathematical-superintelligence models and the expansion of Aristotle's public products.
On July 28, 2025, Harmonic launched a beta of the Aristotle consumer application for iOS and Android, offering free public access to the model's mathematical reasoning. The company said it would follow the mobile beta with a web interface and an application programming interface (API) aimed at enterprises, mathematicians, researchers and students; the Aristotle API was subsequently released. Reported product improvements include accepting plain-English problem statements, automated generation of intermediate lemmas, and a streamlined interface. Harmonic has framed these releases as steps toward making formally verified reasoning a routine tool rather than a research demonstration, while noting that the guarantee of correctness applies within the mathematical domains the system supports rather than to arbitrary queries.
Harmonic occupies a distinctive position in the contemporary AI landscape. Where most frontier labs pursue general-purpose large language models and treat reliability as a property to be improved statistically, Harmonic stakes its case on formal verification: the claim that, by routing reasoning through Lean, it can offer a machine-checkable guarantee of correctness in mathematics. The 2025 IMO episode, in which a roughly 20-person company matched the problem-solving score of far larger rivals, was widely read as evidence that formal methods are now competitive at the research frontier, even as the unofficial and self-defined nature of the AI results drew sustained criticism from mathematicians. If the formal-verification thesis generalizes beyond competition mathematics to areas such as physics, statistics and software verification, as the company intends, it could influence how trustworthy reasoning systems are built. For now, Harmonic's importance rests on a concrete demonstration that verifiable, hallucination-free mathematical reasoning is achievable, paired with open questions about how far that approach scales and how independently its strongest claims can be reproduced.