Harmonic: Aristotle, Lean Proofs & Company History

A fintech CEO and a formal-methods founder

Harmonic was founded in June 2024 by Tudor Achim, who leads it as chief executive, and Vlad Tenev, who serves as executive chairman while remaining chief executive of Robinhood Markets. Achim had previously co-founded Helm.ai, an autonomous-driving company, after studying computer science at Carnegie Mellon and beginning a PhD at Stanford; Tenev holds mathematics degrees from Stanford and UCLA. The company states its mission as mathematical superintelligence, its term for AI systems that can match or exceed the best human mathematicians. [1]

A proof you can check, not just trust

Harmonic's product, Aristotle, is a reasoning engine that outputs formal proofs in Lean, a proof assistant that mechanically checks whether each logical step actually follows, rather than a paragraph of prose asserting that a result is true. That distinction matters for a system meant to do mathematics: a language model can produce a plausible-sounding but wrong derivation, while a Lean-checked proof either compiles or it does not. Aristotle became available to the public through an API in October 2025, with later updates adding support for plain-English problem input alongside native Lean 4. [1][2]

Funding that tracked the results

Harmonic raised a Series A in September 2024 led by Sequoia Capital, with Index Ventures also participating. A Series B followed in July 2025, $100 million led by Kleiner Perkins at roughly a $900 million valuation, announced alongside Aristotle reaching gold-medal-level performance at the 2025 International Mathematical Olympiad, a result Harmonic's own technical writeup and an accompanying paper describe in detail. By November 2025, a $120 million Series C led by Ribbit Capital, with Sequoia, Index, and Emerson Collective continuing to invest, valued the company at $1.45 billion, making it a unicorn roughly seventeen months after founding. [3][4][5]

Atlas interpretation: The funding pattern is straightforward for a pre-revenue research company: each round followed a public demonstration rather than a product metric, first the IMO result and then, two months later, the Erdős problem resolution described below. Investors were pricing a research trajectory, not usage. [4][5]

An Erdős problem resolved, with help from a rival lab

On January 12, 2026, a writeup by Nat Sothanaphan described the resolution of Erdős Problem #728, one of the open problems collected from Paul Erdős's decades of published conjectures. OpenAI's GPT-5.2 Pro produced the informal mathematical argument, and Harmonic's Aristotle converted that argument into a Lean proof that could be mechanically checked. The writeup describes it as the first Erdős problem regarded as fully resolved autonomously by an AI system, with a human mathematician driving the process rather than doing the mathematics by hand. [6]

Atlas interpretation: The pairing is notable on its own terms: Harmonic's formal-verification engine supplied the rigor for an argument generated by a competitor's general-purpose model, on a problem neither company built alone. That is a different shape of collaboration than the funding and licensing deals that dominate the rest of the timeline, where labs mostly compete for the same customers rather than checking each other's proofs. [6]