The formalized proofs are useful because they allow you to formalize more difficult proofs. That's circular but let me explain. Formalizing all of mathematics i

The formalized proofs are useful because they allow you to formalize more difficult proofs. That's circular but let me explain. Formalizing all of mathematics in a formal, computer verifiable language is theoretically easy. The problem is that you don't want it to take forever to write down a proof because you have to go axiom by axiom. This is a problem of abstraction. Just like we need programming languages which have powerful, high level methods of abstraction, like functions, we need a formal language for mathematics that makes it easy to formalize proofs. You don't want to work with the axioms all the time, but instead use your oreviously proven results. When you have a good setup like this, writing down a proof formally should only take O(n) time, meaning it only takes up to some constant longer than writing down the informal proof. The goal right now is to get this constant down so it becomes appealing for the average mathematician to formalize their proof, without needing deep knowledge of type theory. This is happening right now with the Mathlib of Lean, a database of already formalized theory. So where does this lead? As you build a large database of formalized mathematics you get some snowball effects. We can train language models just like on code to assist us. Formalizing natural language mathematics should merely be a process of translation, if set up correctly, not somwthing computationally advanced. Copilot for formal maths will being the constant lower. As correctness of formal proofs can be automatically checked, at some point you can let the system attempt formalizing Pdf documents by itself. This yields you a larger database, more traininf data etc. In 20 years I hope that we have a database of most.mathematics formalized in Lean, and language models that can translate between natural language math and Lean quite fluently. As any formal language of mathematics is also a programming language, we van start doing some very serious program correctness validation. You will not just run your Euler iteration until it has sufficiently small error, but you will instead run it up to your PROVEN desired error. Because we did all the work of formalizing mathematics, this will not be much harder than just writing the program normally. Mathematicians can also now work with these systems and thereby work quicker, saving time on reviews. Computer verified proofs will.not be unreadable, the database will be open source and constantly refactored and kept clean. Etc. Etc.