Artificial intelligence for formal mathematical reasoning startup Harmonic AI Inc. announced today that it has raised $120 million in new funding on a $1.45 billion valuation.

The funding is intended to accelerate its momentum in developing an advanced mathematical reasoning model that eliminates hallucinations, a common situation in which AI models make up erroneous answers.

The company was co-founded in 2023 by Vlad Tenev, chief executive of Robinhood Markets Inc. Its main offering is Aristotle, an AI engine that specializes in formal mathematical reasoning. The engine uses the Lean 4 proof assistant, a proof assistant that allows users to write mathematical definitions, theorems and proofs in a way that can be checked for correctness by a computer, to translate natural-language math problems into formally verifiable proofs.

The company’s approach is focused on mathematical superintelligence, AI with reasoning capabilities that match or exceed humans. The methodology involves the use of synthetic data generation for training that, instead of relying on web-scraped data, autonomously generates formal problem-proof pairs, which enable recursive self-improvement.

Essentially, the AI model can train itself through a “self-play loop” to scale its capabilities, working from simple exercises toward solving advanced theorems. Aristotle recently achieved a gold-medal level performance at the International Mathematical Olympiad, considered the most prestigious mathematical competition in the world and is now available to the public.

More recently, Harmonic released an application programming interface for Aristotle that has already been used by mathematicians and researchers to accelerate progress and create novel discoveries. The company also rolled out major upgrades last week, including support for plain English input (in addition to native Lean4), automated lemma generation and a streamlined terminal interface.

“Aristotle’s gold-medal performance at the IMO offered an early glimpse into what Mathematical Superintelligence makes possible with advanced reasoning and formal verification together in a single system,” said Harmonic Chief Executive Tudor Achim. “This funding allows us to advance that foundation even further and faster, while aggressively deploying Aristotle across industries where reliability is critical.”

The Series C funding round was led by Ribbit Capital Management, with Sequoia Capital Operations, Index Ventures Management, Kleiner Perkins Caufield & Byers and Emerson Collective also participating.

“The Harmonic team is achieving extraordinary success in showing how MSI can accelerate progress in mathematics and other quantitative fields and Aristotle, even in its early form, already gives us a glimpse toward the better future we will all be in once advanced reasoning and formal verification fully merge,” said Tenev, who serves as Harmonic’s executive chairman.

The new funding follows previous raises of $100 million in Series B funding on a $900 million valuation in July and a Series A raise of $75 million in September 2024.

Image: Harmonic