# Harmonic (AI)

> Source: https://aiwiki.ai/wiki/harmonic_aristotle
> Updated: 2026-06-07
> Categories: AI Companies, AI for Science
> From AI Wiki (https://aiwiki.ai), a free encyclopedia of artificial intelligence. Quote with attribution.

**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](/wiki/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](/wiki/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](/wiki/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](/wiki/artificial_intelligence) to rigorous reasoning. Its central thesis is that the hallucination problem of [large language models](/wiki/large_language_model) can be eliminated in mathematics by requiring outputs to pass a formal check, an approach drawn from [automated theorem proving](/wiki/automated_theorem_proving) rather than from open-ended text generation.

## Founding and leadership

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 and the formal-verification thesis

Aristotle is Harmonic's core system. Rather than emitting natural-language argument, it works in [Lean](/wiki/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](/wiki/reinforcement_learning) and [mathematical reasoning](/wiki/mathematical_reasoning) research. This formal approach distinguishes Harmonic from most of the [generative AI](/wiki/generative_ai) field and aligns it with the [AI-for-science](/wiki/ai_for_science) goal of verifiable machine-assisted discovery.

## The 2025 International Mathematical Olympiad claim

In July 2025 Harmonic announced that Aristotle had achieved gold-medal-level performance on the six problems of the 2025 [International Mathematical Olympiad](/wiki/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:

- Harmonic's approach required problems to be translated by hand into machine-readable formal statements before the system attempted them, and the runs took days rather than the official competition limit of 4.5 hours. By contrast, DeepMind reported solving the problems end to end in natural language within the 4.5-hour window, and its solutions were graded by official IMO coordinators. OpenAI deliberately avoided formal tools and reported solving the problems within roughly competition-length reasoning time, self-graded.
- The IMO did not officially sanction or certify the AI entries as a class. Its president, Gregor Dolinar, said the organization "cannot validate the methods, including the amount of compute used or whether there was any human involvement, or whether the results can be reproduced." Harmonic said it held its announcement until July 28, 2025, after an embargo period requested to avoid overshadowing the human competition.
- The distinctive strength of Harmonic's claim is the nature of its evidence rather than its timing. Because the solutions are Lean proofs checked by a computer, a third party can in principle re-run the verifier and confirm correctness, which is not possible for a natural-language proof that depends on a human grader. The mathematician Kevin Buzzard, a specialist in formalized mathematics, noted that a formal proof that compiles is by definition a full-marks solution, while also cautioning that neither Harmonic nor others fully disclosed how the answers to "determine the value" problems were supplied to the systems, and that the surrounding announcements were not peer reviewed. Skeptics, including mathematicians quoted by *Scientific American*, observed that with no agreed rules each company effectively set and marked its own homework.

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.

## Funding and valuation

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.

## Product and access

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.

## Significance

Harmonic occupies a distinctive position in the contemporary AI landscape. Where most frontier labs pursue general-purpose [large language models](/wiki/large_language_model) 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](/wiki/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.

## References

- [Harmonic Announces IMO Gold Medal-Level Performance & Launch of First Mathematical Superintelligence (MSI) AI App](https://www.businesswire.com/news/home/20250728394917/en/Harmonic-Announces-IMO-Gold-Medal-Level-Performance-Launch-of-First-Mathematical-Superintelligence-MSI-AI-App) - Business Wire, July 28, 2025.
- [Harmonic, the Robinhood CEO's AI math startup, launches an AI chatbot app](https://techcrunch.com/2025/07/28/harmonic-the-robinhood-ceos-ai-math-startup-launches-an-ai-chatbot-app/) - TechCrunch, July 28, 2025.
- [Harmonic Builds Momentum Towards Mathematical Superintelligence with $120 Million Series C](https://www.businesswire.com/news/home/20251125727962/en/Harmonic-Builds-Momentum-Towards-Mathematical-Superintelligence-with-$120-Million-Series-C) - Business Wire, November 25, 2025.
- [Harmonic AI raises $120M at $1.45B valuation to advance mathematical reasoning](https://siliconangle.com/2025/11/25/harmonic-ai-raises-120m-1-45b-valuation-advance-mathematical-reasoning/) - SiliconANGLE, November 25, 2025.
- [Harmonic Raises $100 Million Series B to Accelerate Development of Mathematical Superintelligence](https://www.businesswire.com/news/home/20250710118878/en/Harmonic-Raises-$100-Million-Series-B-to-Accelerate-Development-of-Mathematical-Superintelligence) - Business Wire, July 10, 2025.
- [Harmonic Announces Series A Funding Round To Accelerate Development of Mathematical Superintelligence](https://www.businesswire.com/news/home/20240923548068/en/Harmonic-Announces-Series-A-Funding-Round-To-Accelerate-Development-of-Mathematical-Superintelligence) - Business Wire, September 23, 2024.
- [Harmonic Raises $75M in Series A Funding](https://www.finsmes.com/2024/09/harmonic-raises-75m-in-series-a-funding.html) - FinSMEs, September 2024.
- [Aristotle: IMO-level Automated Theorem Proving](https://arxiv.org/abs/2510.01346) - The Harmonic Team, arXiv, October 1, 2025.
- [Aristotle: IMO-level Automated Theorem Proving (full text)](https://arxiv.org/html/2510.01346v1) - arXiv HTML, October 2025.
- [The 2025 IMO Winner's Circle: How Three AI Teams Got Gold in Very Different Ways](https://inferencebysequoia.substack.com/p/the-2025-imo-winners-circle-how-three) - Inference by Sequoia, 2025.
- [AI at IMO 2025: a round-up](https://xenaproject.wordpress.com/2025/08/03/ai-at-imo-2025-a-round-up/) - Kevin Buzzard, Xena Project, August 3, 2025.
- [Mathematicians Question AI Performance at International Math Olympiad](https://www.scientificamerican.com/article/mathematicians-question-ai-performance-at-international-math-olympiad/) - Scientific American, 2025.
- [Solving the AI Reasoning Gap: How Harmonic is Building Mathematical Superintelligence](https://www.indexventures.com/perspectives/solving-the-ai-reasoning-gap-how-harmonic-is-building-mathematical-superintelligence/) - Index Ventures.
- [How a 20-Person Startup Won Gold at the Math Olympiad](https://www.generalist.com/p/how-a-20-person-startup-won-gold) - The Generalist (interview with Tudor Achim), 2025.
- [harmonic-ai/IMO2025 (formal Lean proofs and verification artifacts)](https://github.com/harmonic-ai/IMO2025) - GitHub.
- [Tudor Achim](https://harmonic.fun/about/) - Harmonic company site.
- [Robinhood CEO's math-focused AI startup Harmonic valued at $1.45 billion in latest fundraising](https://finance.yahoo.com/news/robinhood-ceos-math-focused-ai-192706395.html) - Reuters via Yahoo Finance, November 25, 2025.