I have been watching Terry Tao's lecture on machine-assisted proofs https://www.youtube.com/watch?v=AayZuuDDKP0&t=1460s. However in terms of the formalization of proofs via systems like Lean or Coq that Tao talks about I still do not really get the point of why this is important or what this is good for. I feel like Tao actually never specifies in an intuitive way why these very very advanced proofs need to be formalized.
This is because they are so difficult and dependent on so many assumptions, theorems, mathematical structures etc. right? They are too large basically to keep an overview? Is it this? Or there any other benefits that go beyond verification of systems too large to comprehend for a single individual?
Because I wonder, it would not be of benefit to formalize the proof for the fact that $\sqrt{2}$ is not a rational number, right? Just because it is so small and clear to most beginners even? Or would there also be any benefit in that case?
Mathematicians anyway check each other's proofs, and anyway we/they use a formal language for that, that is mathematics, so using the computer is basically just like having another mathematician on board for the proof who is better informed of all the necessary steps. Is that interpretation correct? Or am I missing something fundamental?
I don’t think there is something like ‘the’ reason or a number of reasons that are the ‘right’ reasons. But sure, there are reasons we do this.
A big one is the one you mention: sometimes proofs do get so complicated or long and tedious that a computer can really help to make sure the proof is correct.
For example, in the 1800's a number of 'proofs' of the four color theorem were offered that turned out to be incorrect .. but sometimes it took more than 10 years before we found the mistake. Presumably if we had tried to formalize it in the first place, we might have found those mistakes earlier.
Indeed, it can be easy for us humans to make mistakes. Think of the infamous 'proof' that all horses are the same color. It can initially be hard to spot the mistake in the proof. And when proofs get more complicated, it gets harder to spot any mistakes yet.
Indeed, you can imagine that after picking the 'low hanging fruit', mathematical proofs get more and more complicated, and I like to think that one impetus for the development of modern formal logic in the 1800's was because of the mistakes that started to occur more and more often.
I also want to note that even though providing a formal proof (whether computer-assisted or not) often feels like an after-the-fact formalization of a proof that we already firmly grasp 'in our head', we oftentimes do rely on symbolic systems to help us think about problems. Notational systems don't just express our already completed thoughts, but help us guide and organize our thinking. Without it, mathematics wouldn't be what it is today.
In this vein, I often wonder to what extent the very formalization of set theory led to Russell's Paradox, and thus to the realization that we can't just make a set out of 'anything you want'.
Other than helping with really complicated proofs, computers can also help us with just very long and tedious proofs. Again we can point to the four color theorem. In 1976 a very long proof was created that relied on checking a very large number of cases: too many for a human to feasibly do. So, they relied on a computer to systematically go through all those cases.
Interestingly, this proof was still looked at with some suspicion, since it wasn't grounded in a purely formal logic system like Coq or Lean. So in 2005 they managed to do the whole thing in such a logic-based proof system.
More recently a good example is the proof of the Sphere Packing Conjecture. In 1998 the mathematician Thomas Hales submitted a gigantic proof of this conjecture (involving lots of computer code) to a journal, but the referees (who did spend a good bit of time trying to work through it) came back and said that they were '99% sure' the proof was correct ... which of course is not acceptable to a mathematician! So then Hales and a team of other people spent a good number of years formalizing the proof in Isabella and HOL light, two other logic-based computer-assisted proof systems, and they completed this in 2014. A few years later, the journal then accepted this proof as well.
With these last 2 examples you might think: Why spend so much time on formalizing one specific proof? Well, especially when a logic-based approach is used, the eventual proofs that were generated are likely to be built up from various lemma's and sub-theorems that they also had to formalize. And those can now be used for other proofs as well.
And finally, some will find it just a fun challenge to try and formalize a proof, even if that it is as simple as the proof that the square root of 2 is an irrational number, or that there are infinitely many prime numbers ... and doing so again can sometimes provide some deeper insight as to how the proof works, what axioms it relies on , etc.