Vlad Tenev, co-founder of Robinhood, is now steering his focus on AI's potential to revolutionize mathematics. Alongside Tudor Achim, who tracks the rise of Lean, an esoteric programming language, they delve into the possible integration of AI in solving complex mathematical challenges. They discuss the impact of mathematical superintelligence, the significance of synthetic data, and how Lean is transforming proofs. Their ambitious vision includes tackling Millenium Prize problems, all while emphasizing the importance of mentorship in shaping mathematical minds.