Harmonic, an AI startup co-founded by Robinhood CEO Vlad Tenev, has launched a beta version of its AI chatbot app for iOS and Android, giving users access to its AI model, Aristotle. The company is broadening access to Aristotle, which it claims offers “hallucination-free” answers for mathematical reasoning questions.
Harmonic’s core mission is to create “mathematical superintelligence” (MSI). The startup plans to expand Aristotle’s capabilities to assist users with various fields that rely on mathematics, including physics, statistics, and computer science. Harmonic CEO and co-founder Tudor Achim stated that Aristotle is “the first product available to people that does reasoning and formally verifies the output,” adding, “Within the domains that Aristotle supports, which are quantitative reasoning domains, we actually do guarantee that there’s no hallucinations.”
The company also intends to release an API for enterprises to access Aristotle and a web app for general consumers in the future. Harmonic announced that Aristotle achieved gold medal performance on the 2025 International Math Olympiad (IMO) through a formal test, where problems were translated into a machine-readable format. This achievement places Aristotle alongside AI models developed by Google and OpenAI, which also attained gold medal performance in this year’s IMO via informal tests in natural language. Despite this, Harmonic has not released other benchmarks for Aristotle at this time.
This beta launch follows Harmonic’s successful Series B funding round, which raised $100 million. The round was led by Kleiner Perkins, valuing the company at $875 million. Achim indicated that Harmonic is “advancing very rapidly along” its path to achieving MSI, and investors believed the valuation was fair given the scope of the startup’s ambition.
Several leading tech companies are actively focused on training AI models to solve mathematical problems. The ability of AI to perform mathematics is valuable in itself, and math is also considered a uniquely verifiable domain that demands core reasoning skills. Systems capable of developing these skills could prove useful in other domains as well. Achim explained that Harmonic achieves its high accuracy by having Aristotle produce responses in Lean, an open-source programming language. Before providing an answer to users, the model algorithmically double-checks the solution for correctness, a process that does not involve AI. Achim noted that similar verification technology is used in high-stakes fields such as medical devices and aviation.
Achieving hallucination-free performance from an AI model, even within a narrow domain, is an incredibly difficult task. Studies have shown that even leading AI models frequently hallucinate, and this problem has not shown signs of significant improvement, with some of OpenAI’s latest reasoning models even exhibiting more hallucinations than their predecessors.
