Kevin Buzzard and Big Proof

Kevin Buzzard explains how proof assistants check mathematical arguments against axioms and logical rules. The discussion covers the interactive process of formalizing a proof, the collaborative communities around these tools, and the project to formalize Fermat’s Last Theorem. It also examines how proof assistants might work with AI to strengthen mathematical practice.