Mathematics without proof assistants will be bizarre

Proof assistants provide a way to write fully formalized proofs of mathematical theorems. Mathematics is continuously being formalized using tools like Isabelle, Lean and Rocq. Projects like AlphaProof use formalized mathematics to back AI-based proving efforts. In this talk I will explain the basics of Type Theory-based proof assistants using the Curry-Howard correspondence. Then I will explain how proof assistants are changing the way we do mathematics today. Finally, I will elaborate why I think in 50 years we will look at doing mathematics without a proof assistant as being a bizarre thing.