This is a November 15 talk by Kevin Buzzard at the Collège de France discussing the discrepancies between formal proof and actual mathematical practice, the problems with bouncing between the two and the role of proof assistants like Lean. Even if you already know about Buzzard's work, the lecture discusses some new developments and is overall a good introduction to the topic.