If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more.
However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof.
This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out.
So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject.
I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.
> I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.
Or to indeed find that simpler proof, I suppose?
(Not disagreeing with anything you're saying, just checking - it's a fascinating story that I didn't know about this topic)
I don't understand this area well at all, but I know the existing classification of finite simple groups is very long and detailed.
Wikipedia says
> The proof consists of tens of thousands of pages in several hundred journal articles
and that the second-generation simplified version might possibly run to only 5,000 pages.
5,000 pages of math is easier to understand and/or believe in than tens of thousands of pages, but it's still a pretty daunting amount even for specialists.
Why would it have to be one person? I would assume that the proof can be presented as mostly modular based on compositing results from the related published work
However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof.
This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out.
So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject.
I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.