Harmonic, the AI startup co-founded by Robinhood CEO Vlad Tenev, has launched the public beta version of its chatbot app “Aristotle” on iOS and Android. The release opens the company’s math-focused large language model directly to users for the first time, allowing them to ask complex quantitative questions and receive answers that are formally verified for accuracy.
The app relies on a hybrid architecture combining natural language processing with symbolic proof generation. When a user asks a question, Aristotle translates the response into Lean, a formal proof language used by mathematicians and logicians, and then validates the solution using a deterministic algorithm. This approach allows Harmonic to guarantee that, within its supported domains, the chatbot provides answers without hallucination—a key challenge in generative AI systems.
Harmonic recently completed a $100 million Series B funding round, bringing its valuation to $875 million. The round was led by major investors in the AI and fintech sectors, including prominent venture capital firms and angel backers from the tech world. This funding is expected to fuel further development of the Aristotle platform and expand its capabilities across new scientific fields.
Aristotle has already made an impression in competitive benchmarks, matching gold-level performance on the International Mathematical Olympiad’s machine-readable problems. Unlike traditional AI benchmarks that rely on subjective, natural-language assessments, Harmonic’s methodology ensures each solution can be independently checked for correctness—offering a more rigorous standard for performance evaluation.
The company plans to release a web-based version of Aristotle soon, alongside an enterprise API aimed at integrating its verified reasoning engine into research, finance, and education workflows. Longer term, Harmonic intends to expand beyond pure mathematics into fields such as physics, data science, and formal logic.
By focusing on reliability over raw fluency, Harmonic is positioning itself as a counterweight to more generalized AI systems. Its emphasis on provable results could make it particularly appealing to users who need precision over prose, and certainty over speed.
