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 GuthTerry Tao: perhaps the greatest living mathematician and Vlad’s professor at UCLALean: an open source functional language for code verification launched by Leonardo de Moura when at Microsoft Research in 2013 that powers the Lean Theorem Provermathlib: the largest math textbook in the world, all written in LeanMetaculus: online prediction platform that tracks and scores thousands of forecastersMinecraft Beaten in 20 Seconds: The video Vlad references as an analogy to AI mathNavier-Stokes equations: another important Millenium Prize math problem. Vlad considers this more tractable that RiemannJohn von Neumann: Hungarian mathematician and polymath that made foundational contributions to computing, the Manhattan Project and game theoryGottfried 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!