Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters
whatshot 12 snips
Sep 24, 2024
Discover how Vlad Tenev and Tudor Achim are aiming to revolutionize math through AI! They discuss the power of adding mathematical code to enhance reasoning in models. The intriguing intersection of Lean, a functional programming language, is highlighted for its role in theorem proving. They also delve into the challenges of the Millennium Prize problems, like the Riemann Hypothesis, and the significance of synthetic data in improving mathematical models. Join the exploration of AI's potential to transform mathematical problem solving!
39:45
forum Ask episode
web_stories AI Snips
view_agenda Chapters
auto_awesome Transcript
info_circle Episode notes
insights INSIGHT
Math as the Foundation of Reasoning
Math underpins all science and engineering fields, serving as a universal language for understanding the universe.
Mastering math enhances quantitative skills, suggesting that AI proficient in math will excel in science and engineering.
question_answer ANECDOTE
Vlad Tenev's Math Journey
Vlad Tenev shares how his strong math background helped him easily transition into entrepreneurship and coding.
This personal experience reinforces the idea that math skills are transferable to other domains.
insights INSIGHT
Math Community's Reaction to AI
The math community is divided on AI's role, with younger mathematicians embracing it while older ones remain skeptical.
Vlad Tenev predicts AI's role in math will evolve similarly to chess, initially assisting humans but eventually dominating.
Get the Snipd Podcast app to discover more snips from this episode
Adding code to LLM training data is a known method of improving a model’s reasoning skills. But wouldn’t math, the basis of all reasoning, be even better? Up until recently, there just wasn’t enough usable data that describes mathematics to make this feasible.
A few years ago, Vlad Tenev (also founder of Robinhood) and Tudor Achim noticed the rise of the community around an esoteric programming language called Lean that was gaining traction among mathematicians. The combination of that and the past decade’s rise of autoregressive models capable of fast, flexible learning made them think the time was now and they founded Harmonic. Their mission is both lofty—mathematical superintelligence—and imminently practical, verifying all safety-critical software.
Hosted by: Sonya Huang and Pat Grady, Sequoia Capital
Mentioned in this episode:
IMO and the Millennium Prize: Two significant global competitions Harmonic hopes to win (soon)
Riemann hypothesis: One of the most difficult unsolved math conjectures (and a Millenium Prize problem) most recently in the sights of MIT mathematician Larry Guth
Terry Tao: perhaps the greatest living mathematician and Vlad’s professor at UCLA
Lean: an open source functional language for code verification launched by Leonardo de Moura when at Microsoft Research in 2013 that powers the Lean Theorem Prover
mathlib: the largest math textbook in the world, all written in Lean
Metaculus: online prediction platform that tracks and scores thousands of forecasters
Navier-Stokes equations: another important Millenium Prize math problem. Vlad considers this more tractable that Riemann
John von Neumann: Hungarian mathematician and polymath that made foundational contributions to computing, the Manhattan Project and game theory
Gottfried Wilhelm Leibniz: co-inventor of calculus and (remarkably) creator of the “universal characteristic,” a system for reasoning through a language of symbols and calculations—anticipating Lean and Harmonic by 350 years!
00:00 - Introduction
01:42 - Math is reasoning
06:16 - Studying with the world's greatest living mathematician
10:18 - What does the math community think of AI math?
15:11 - Recursive self-improvement
18:31 - What is Lean?
21:05 - Why now?
22:46 - Synthetic data is the fuel for the model
27:29 - How fast will your model get better?
29:45 - Exploring the frontiers of human knowledge
Training Data