Inside xAI, and the Bet on AI Math - with Christian Szegedy (Math Inc)

Christian Szegedy, co-inventor of Inception networks and batch normalisation and a founding scientist at xAI, explains why he moved to Math Inc to work on formal mathematics. He argues that Lean and autoformalisation could provide a machine-checkable layer beneath AI reasoning, so that proofs are guaranteed correct without human reading. The episode discusses his wager that AI will reach superhuman mathematical ability, and what verified reasoning could unlock beyond mathematics, including verified software and more trustworthy AI systems.