Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters

Harmonic's Core Thesis: Vlad Todorovic (CEO of Robinhood) and Tudor (co-founder) aim to create mathematical superintelligence by explicitly teaching AI to reason through math, rather than treating math as an emergent property of scale.

• They view math as the foundational language of the universe, applicable to modeling phenomena from black holes to atoms and engineering designs.
• Their hypothesis is that proficiency in rigorous mathematical reasoning transfers to superior performance in broader scientific and engineering domains.

Data Strategy & The "Data Wall": Harmonic relies heavily on synthetic data generated through internal self-play and reinforcement learning, contrasting with traditional foundation models that rely on static internet data.

• Existing open-source repositories like mathlib (written in the Lean programming language) provide human-written proofs, but the volume is insufficient for training, necessitating AI-generated data.
• The company argues that the "data wall" encountered by general-purpose AI (exhaustion of high-quality internet content) is a primary reason for their approach.
• Synthetic data generation allows for the creation of problems with increasing complexity, mirroring how human mathematicians break large problems into smaller, solvable chunks.

Technology Stack (Lean & Formal Verification): The system utilizes Lean, a programming language created by Leonardo de Moura (Amazon), where mathematical statements are encoded in the type system.

• Compilation in Lean acts as a formal verification step, providing an objective, binary reward function (correct/incorrect) essential for reinforcement learning.
• This eliminates the ambiguity of human feedback loops, enabling rapid, recursive self-improvement cycles similar to AlphaGo Zero.
• The mathlib library has grown organically into a massive open-source repository of formalized mathematics, surpassing usage for its original purpose of software verification.

Timeline & Predictions for Major Milestones:

• IMO (International Mathematical Olympiad): The speakers predict winning the IMO by 2024 or 2025 with AI assistance.
• Millennium Prize Problems:
  • Hybrid human-AI solutions for easier Millennium problems are estimated by 2026.
  • A fully AI-aided or AI-solved Riemann Hypothesis is estimated by 2029.
  • The current speaker estimates a 43% chance the next Millennium Prize is solved by AI or significant AI assistance, believing this figure is an underestimate.
• Superhuman Reasoning: The team anticipates achieving reasoning capabilities exceeding top human mathematicians (e.g., Terry Tao) within two years, with models reaching the 99.99th percentile in the next year.

Future of Mathematics & Human Roles:

• The role of the mathematician will shift from calculation to strategic direction: defining problems, selecting which areas to attack, and interpreting AI-generated results.
• The field is expected to evolve past the "human + AI assist" phase toward fully autonomous systems, though human guidance will remain in the loop for problem selection.
• Unlike zero-sum games like chess where optimal strategies eventually cap progress, math has no upper bound, allowing for continuous, unbounded improvement via increased compute.

Broader Applications Beyond Pure Math:

• Software Engineering: The speakers predict a future where the vast majority of software is provably correct and verified by AI, shifting the industry focus from code review to rigorous specification.
• Physics: Harmonic aims to accelerate theoretical physics research, potentially helping to deduce fundamental laws of the universe and design experiments to test them.
• General Reasoning: If the core premise that "math is reasoning" holds, the technology could eventually apply to any domain requiring logical deduction, including humanities (e.g., history essays), though this is a secondary focus.

Historical & Strategic Context:

• Why Now: The convergence of recent advancements in autoregressive language models (capable of infinite action spaces) and the maturity of the Lean formal verification tool (released officially in September 2023) created a viable inflection point.
• Community Sentiment: The math community is split; younger mathematicians are generally pro-AI and pro-formal methods, while older practitioners remain skeptical.
• Inspirational Figures: Vlad Todorovic cites John von Neumann (for his transition from math to computer science and game theory) and Gottfried Leibniz (for his 17th-century prediction of a "universal characteristic" or formal deductive language) as key intellectual influences.