Formalization of mathematics is the process of translating it from human language into the language of a computer proof assistant such as Lean. Ten years ago it was mostly computer scientists doing it, but now both mathematicians and machines have joined in. I will talk about the following questions. What is the point of doing it? Should humans or computers be doing it (related question: is it a science, or an art)? What are the pain points? And what does the future hold?
