Harmonic
Mathematical superintelligence via formally verified reasoning
Harmonic, co-founded by Robinhood CEO Vlad Tenev and Tudor Achim, builds Aristotle, an AI system that produces formally verified mathematical reasoning in Lean. Aristotle achieved formally-verified gold-medal-level performance on the 2025 IMO.
Aristotle: formally verified IMO gold-level performance
| Website | harmonic.fun |
|---|---|
| Domains | Math |
| Location | Palo Alto |
| Team size | 26-50 |
| Founded | 2023 |
| Funding | Series B, $100M at ~$900M valuation (Kleiner Perkins, 2025) |
| Founders | Tudor Achim, Vlad Tenev @vladtenev |
Similar startups
Also listed under Math.
| Name | Domains | Location | Team | Funding | Raising |
|---|---|---|---|---|---|
| Rise Data Labs US-based expert human data and custom RL environments for enterprise AI | Computer Use, Coding, Finance, Cybersecurity, Legal, Data Labeling, Enterprise, Multi-Domain, RLHF, Custom Environments | United States | - | - | Yes |
| Axiom Math Self-improving AI mathematician with formally verified reasoning | Math | San Francisco | 11-25 | Series A, $200M at $1.6B valuation (2026); $264M total | - |
| Epoch AI Nonprofit research institute behind FrontierMath and AI capability benchmarks | Math, Machine Learning | Remote | 11-25 | Philanthropic grants (nonprofit) | - |
| Hillclimb Math environments emphasizing verifiable correctness | Math | San Francisco | 1-10 | - | - |
| Math, Inc. Autoformalization agents for verified mathematics | Math | Palo Alto | 1-10 | Seed, $15M (Torch Capital, Robot Ventures, Chapter One) | - |
| Ulam Math RL environments and RLVR trajectories | Math | Warsaw, London | 1-10 | - | - |