Title: Formalization in Analysis and PDE
Abstract: I will discuss several of my recent works in analysis and PDE, all of which have been entirely formalized in Lean. The talk will be introductory and focus on the main motivations for my works and how mathematicians without prior Lean experience can now formally verify their papers in a relatively short period of time.