There has been a lot of talk about formalizing mathematics recently, ever since OpenAI proposed a solution to the famous Navier-Stokes problem formalized in Lean. Since I did some work in mathematical logic in the past, I thought it might be useful to clarify what the talk is all about... Read more.