Harmonic is an artificial intelligence-based company that aims to reduce AI hallucinations and to improve AI mathematical skills through the development of a "mathematical superintelligence".
History Harmonic was co-founded in 2023 by Tudor Achim and Vlad Tenev, who is also the executive chairman. It is based in Palo Alto, California. Its aim is to reduce AI hallucinations for applications in sectors like automotive, aerospace, and medicine by generating and checking Lean code, and also to improve AI's mathematical skills. When prompted, the company’s chatbot, Aristotle, outputs answers to mathematical queries, along with the reasoning behind its answer. Harmonic's model is trained by mathematicians hired by the company.
As of June 2024, Harmonic posted an 83% success rate on F2F, a mathematical benchmark, aided by computer algebra systems. The chatbot was trained on synthetic math proofs, a computer-generated example that’s used to teach problem solving, and it displayed a "top-level performance" at the International Mathematical Olympiad in July 2025. In that same month, Harmonic raised $100 million in Series B funding, with the round being led by Kleiner Perkins, with participation from Sequoia Capital, Index Ventures and Paradigm. The additional funding raised the company's value to $875 million.
Through November 2025, Harmonic had raised $295 million in total capital, creating a valuation of $1.45 billion. In January 2026, it was reported by Axios that Nvidia had backed the company, joining the funding round.
Also in January 2026, amateur mathematicians used Harmonic's AI program, Aristotle, to solve an Erdos problem in collaboration with OpenAI’s GPT-5.2 Pro.
In March 2026, Harmonic released its AI system, Aristotle Agent. The company described it as an agentic "autonomous mathematician", interpreting written math problems to convert them into formal proofs. Harmonic claimed that Aristotle Agent ranked first in formal mathematics when compared to ProofBench, a benchmark developed by Vals AI, as of March 2026.
In July 2026, Harmonic partnered with the American Institute of Mathematics to create a new mathematical benchmark to test AI models against, intending to measure if models both "produce correct answers" and if "they help mathematicians make progress on difficult research problems."
References