Robinhood CEO Develops Math AI, Valuation Nears $900 Million Tackling Millennium Problems

Stock trading platform Robinhood’s CEO, Vlad Tenev, has once again attracted significant investment for his AI company. On July 9, Harmonic, the AI startup co-founded by Tenev, announced a $100 million B轮融资, bringing the company's valuation to $875 million, close to unicorn status. This round was led by renowned venture capital firm Kleiner Perkins, with additional investments from Paradigm and other institutions. Founded just two years ago, Harmonic focuses on a highly innovative and challenging field known as Mathematical Superintelligence (MSI). Unlike mainstream Large Language Models (LLMs), Harmonic aims to address the fundamental issue of AI "hallucinations," where models generate false or misleading information. Their solution involves equipping AI with rigorous mathematical reasoning capabilities, ensuring each step is verifiable through formal methods. Tenev’s deep mathematical background significantly contributes to Harmonic’s success. Born to Bulgarian parents, he moved to the United States at age five. After graduating from Thomas Jefferson High School for Science and Technology in Virginia, Tenev pursued a bachelor’s degree in mathematics at Stanford University, where he met Baiju Bhatt, his future co-founder of Robinhood. Tenev later enrolled in the mathematics Ph.D. program at the University of California, Los Angeles (UCLA), under the guidance of renowned mathematician Terence Tao. Terence Tao is famous for his groundbreaking contributions across various fields of mathematics, including number theory, combinatorics, and harmonic analysis. He has also been actively promoting the Lean programming language, which forms the core of Harmonic’s technology. Despite his strong academic foundation, Tenev left the UCLA Ph.D. program to co-found two fintech companies, Celeris and Chronos Research, in New York. These early ventures paved the way for the eventual creation of Robinhood in 2013, which disrupted the brokerage industry with its zero-commission trading model. Tudor Achim, Harmonic’s other co-founder, boasts impressive credentials as well. Achim holds a bachelor’s degree in computer science from Carnegie Mellon University and completed his doctoral studies at Stanford University, focusing on AI applications in perception. He is also a former co-founder and CTO of Helm.ai, an autonomous driving company that provides AI solutions to top automotive manufacturers. Achim’s expertise in machine learning and algorithms complements Tenev’s mathematical skills. Achim and Tenev share a vision of using AI to solve one of the Millennium Prize Problems. Recognizing the limitations of traditional AI methods, they turned to the Lean programming language. Developed by Microsoft researcher Leonardo de Moura, Lean is designed for software verification but has become unexpectedly popular in the mathematics community. Its strength lies in translating mathematical theorems into verifiable code, ensuring logical correctness in every proof verified in Lean. Harmonic’s flagship product, the Aristotle model, leverages Lean 4 to achieve this. When users pose mathematical questions in natural language, Aristotle converts them into Lean 4 code, performs rigorous logical reasoning, and outputs answers in both natural language and Lean code. This "automatic formalization" capability enables collaboration between Aristotle and mathematicians or educators unfamiliar with Lean, helping to verify and elaborate on their work. The Aristotle model has shown exceptional performance in mathematical reasoning. On the MiniF2F benchmark, which includes 488 problems from international math olympiads and undergraduate courses, Aristotle achieved a 90% accuracy rate, surpassing previous records set by DeepSeek-Prover and LEGO-prover. This benchmark tests a wide range of problem-solving skills, from simple calculations to complex proofs, making Aristotle's results particularly noteworthy. Key breakthroughs in Harmonic’s technical approach include recursive self-improvement and synthetic data generation. Aristotle can iteratively improve through reinforcement learning and self-play, thanks to Lean’s objective verification standards. Additionally, Harmonic can generate vast amounts of synthetic mathematical data, simulating human learning processes to train the model on increasingly complex problems. Harmonic envisions its technology being applied in high-stakes, accuracy-critical industries like aerospace, chip design, industrial systems, and healthcare. Formally verified software is essential in these sectors, where traditional AI’s unpredictability often makes it unsuitable. In blockchain and financial services, where security is paramount, Harmonic’s formal verification capabilities offer significant value. Tenev anticipates that, within the next 5 to 10 years, most software will be formally verified and provably correct, a forecast shared by many in the investment community. Kleiner Perkins partner Ilya Fushman, a physicist, expressed strong confidence in Harmonic’s approach: “Harmonic has laid a new foundation for verifiable, scalable reasoning that can be trusted in high-risk environments. I am excited about the potential applications of Aristotle, not only in software but also in accelerating scientific and engineering advancements.” Index Ventures partner Jan Hammer, who will join the board as an observer, believes mathematical superintelligence could have a transformative impact, similar to how Google revolutionized access to simple information. He sees Harmonic enabling the easy execution of complex numerical solvers, optimization of industrial processes, and code verification. Harmonic’s emergence is timely, aligning with recent advancements in autoregressive language models and the release of Lean 4. The company plans to use the latest funding to accelerate Aristotle’s development and commercialization. Harmonic is actively recruiting AI researchers, mathematicians, and distributed systems experts to maintain its lead in the field of mathematical superintelligence. Later this year, Aristotle will be made available to researchers and the public, marking a crucial milestone in validating its technical approach.