Recorded 15 February 2023. Patrick Massot of the Université Paris-Saclay presents "Formal mathematics for mathematicians and mathematics students" at IPAM's Machine Assisted Proofs Workshop. Abstract: I will explain how I think formal mathematics will eventually become a useful tool for many mathematicians. Proof verification is not the only expected benefit of formal methods and I will rather focus on how they could impact exposition of mathematics. Demo link - tinyurl.com/LeanIPAM Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/