Not an expert, but I think your question is roughly analogous to asking why there isn't one programming language. There are many different approaches to writin

Not an expert, but I think your question is roughly analogous to asking why there isn't one programming language. There are many different approaches to writing formalization systems, and so far we don't have one that has won out as clearly superior (though from the outside it looks like Lean has the most momentum, and is the only one that has been used on cutting edge mathematics as far as I know). On your question why there isn't more of a movement to formalize proofs: Proofs as written are for communicating and convincing other humans. Humans are _very_ good at filling in gaps. You can say things like: "In what follows we need this minor property to hold, it can be proven easily using Properties 4, 5, and 6 established above by using the strategy X". Here easily means "easy for a specialist who has dedicated 10 years to study this stuff", which is the target audience for your writing. If you instead need to explain this minor result to a formalization engine, you have to spell out every. single. last. detail. That's tedious and it adds very little rigor. https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y022904/1 https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y0... Kevin Buzzard got a 5 year grant to get started on formalizing the proof of Fermats Last Theorem. Thats the amount of extra effort we are talking.