What formalized mathematics is all about

Many people think that formalizing mathematics is mainly about the formal verification of theorems. Yes, that's one of the motivations, but there are so many more. One such motivation is that it allows for new ways of organizing mathematical knowledge in large cohesive libraries of formalized mathematics. For instance, Lean's main mathematical library, called mathlib, currently has over 1.5 million lines of formalized mathematics, with over 300 contributors, which, by the nature of the system itself, is guaranteed to be consistent at all times, across all its subcomponents.
While this library is not yet at the level of research mathematics, it is now possible to *define* some objects which are of interest in this community, including absolute Galois groups and étale fundamental groups. I will discuss how Lean sees such objects during the talk.
More generally, this talk will provide an introduction to what this subject of formalized mathematics is all about, how it helps organize and even facilitate mathematical knowledge, and how it might reshape the future of mathematics as a whole.