Why is formalization needed in mathematics?
Why is formalization needed in mathematics?
There is no formalization required for mathematics and in fact, almost all mathematics is developed, learned and written completely informal. The problem which formalization tries to resolve, is enormous amount of mathematical texts and publications waiting for review. And some of them are really big papers consisting of large amount of ideas not quite clear. For reviewer, who always is working mathematician, it us challenging to make investment into understanding others ideas just to produce review while stopping, for a while, its own research.
Formal methods may, in theory, make at least, problem of the checking of ogical correctness, automatic.
However, who want to create this formall mathematical texts at the first move? Mathematicians want to describe his ideas on informal way, and till today, except rather exotic topics, most of the community did not adopted any of formal standards ( and even maybe not agree of formal logical framework to build one)