Opening Discussion on AI Solving Millennium Prizes

• 43% chance next millennium prize solved by AI or human with significant AI assist (metaculus prediction)
• Speaker believes this is underestimate
• Larry Guth potentially on path to Riemann hypothesis
• Next millennium prize by human would need to be very near future
• Next next one will probably be significantly solved by AI

Company Introduction and Core Philosophy

• Harmonic: AI research lab founded by Vlad Tenev (Robinhood CEO) and Tutor
• Mission: create mathematical superintelligence to push frontiers of human knowledge
• Core belief: math is reasoning
• Contrarian approach: directly teach models math vs allowing math to emerge from scale

Mathematical Foundation as Universal Language

• Math underlies almost all fields of science and engineering
• Universe explainable by math - compact set of symbols explain phenomena
• Enables shared cognitive theories that are objective, clear, transparent
• Deductive rules provide agreed-upon ground rules for modeling
• Humans good at math tend to be good at other quantitative areas
• Bet: systems really good at math will excel at scientific/engineering tasks

Vlad's Mathematical Background

• Studied under Terry Tao at UCLA (world's greatest living mathematician)
• Previously worked with Larry Guth at Stanford on honors thesis
• Tao's breadth: contributions to number theory, combinatorics, harmonic analysis, applied math
• Leading lean contributor, active in community
• Vlad: math PhD dropout after one year at UCLA
• Example of math transferring to monetizable skills in entrepreneurship

Math Community's AI Reception

• Split reception: younger mathematicians pro-AI and verification tools like lean
• Older mathematicians more skeptical
• Evolution similar to chess: lengthy period of human + AI assist
• Eventually AI will get better, humans will guide algorithms
• Role of mathematician will fundamentally change
• Future: prompting and guiding AIs to solve problems

AI Capabilities and Millennium Prize Predictions

• AI should be able to solve Riemann hypothesis or prove it's undecidable
• Great mathematicians synthesize papers, find connections, create complex theories
• AI models excel at synthesizing large amounts of information, finding patterns
• Recursive self-improvement capability
• 43% metaculus prediction considered underestimate

Recursive Self-Improvement in Mathematics

• Unlike board games with optimal strategies, math has no upper bound
• Continuous improvement with more compute
• Will solve problems much harder than Riemann hypothesis
• Problems beyond human conception to write down
• Minecraft AI analogy: incomprehensible speed/method

Lean Programming Language and Formal Verification

• Created by Leo de Moura at Amazon AWS
• Originally software verification tool, not designed for math
• Mathematical statements encoded in type system
• Input types = theorem assumptions, output types = conclusions
• Compiling program proves theorem validity
• Mathlib: organic library built by thousands of mathematicians
• Open source on GitHub, growing rapidly

Why Now: Timing and Technology Convergence

• Autoregressive language models handle infinite action spaces (vs finite moves in Go)
• Lean 4 officially released September 2023
• Combination of improved AI + mature lean ecosystem
• 2015-2016: no great AI systems for infinite action spaces
• Lean flexibility attracted large mathematician community

Data and Synthetic Data Generation

• Mathlib provides human-written lean code but not optimized for problem solving
• Data-poor regime compared to most AI areas
• Primary data source: agents solving problems and generating training signals
• Must progress through intelligence levels recursively
• Less math data on internet than cat videos
• Advantage: can generate most required training data vs hoping for emergent math

Data Wall and Quality Ceiling

• Foundation models exhausted internet data
• Internet data quality provides ceiling for model intelligence
• Need self-reinforcing self-play regime to surpass human mathematicians
• Alpha Go to Alpha Zero approach inevitable
• Math advantage: can measure problem complexity by lines of lean code
• Problems solved by breaking into smaller, manageable chunks

Rate of Model Improvement

• Primary limiting factor: energy/compute resources
• More energy = more parallel attempts = faster data generation
• No fundamental constraint on improvement speed
• Additional limitations: mathlib completeness (lacks geometry, very theoretical)
• Future unlock: models creating new theories, expanding domains
• Auto-formalization capability needed (baseball team example)

Future Applications and Vision

• Mission: explore frontiers of human knowledge
• Close all millennium prize problems and go beyond
• Software engineering: proven correct code
• Safety-critical software verification
• General software proven correct
• Software engineering shift: less code collaboration, more spec collaboration
• Theoretical physics acceleration
• Understanding universe fundamentals

Scope and Reasoning Transfer

• Math as reasoning foundation
• Natural extension to computer science
• Belief: really good math systems will handle scientific/engineering tasks
• Even history essays potentially in scope long-term
• Focus on math and math-adjacent areas initially

Rapid Fire Predictions

• IMO win: 2025 (maybe 2024)
• Millennium prize: 2029 (2028 for human-AI hybrid)
• Easy millennium prizes: Navier-Stokes 2026
• Riemann hypothesis: 2029
• Human-level mathematical reasoning: couple years away
• 99.99th percentile performance: within next year

Inspirational Figures

• Von Neumann: mathematician discouraged by father, friend couldn't talk him out of it
• Pioneered computer science, Von Neumann machine blueprint
• Manhattan Project contributions, Game Theory canonical text
• Leibniz: competing with Newton on calculus
• Universal characteristic concept (late 1600s): predicted automated deduction language
• Essentially predicted 2024 developments with lean and AI