An enormous theorem: the classification of finite simple groups (2006)
This is why we need to move <i>away</i> from depending on just humans to verify proofs. The goal shouldn&#x27;t be &quot;does a human fully understand the whole thing&quot; but &quot;is it proven to be true?&quot;<p>There are a number of computer-based tools that can verify proofs, including HOL Light, Isabelle, Coq, Mizar, ProofPower and Lean. We should be working towards the day where running a proof through that kind of tool is what&#x27;s required for publication: <a href="http:&#x2F;&#x2F;www.cs.ru.nl&#x2F;~freek&#x2F;100&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.cs.ru.nl&#x2F;~freek&#x2F;100&#x2F;</a><p>I do a lot with Metamath. The largest Metamath database, which uses classical logic &amp; ZFC set theory, can be seen here: <a href="http:&#x2F;&#x2F;us.metamath.org&#x2F;mpeuni&#x2F;mmset.html" rel="nofollow">http:&#x2F;&#x2F;us.metamath.org&#x2F;mpeuni&#x2F;mmset.html</a> Every one of its proofs routinely verified by 5 different programs written in 5 different programming languages by more than 5 different people. Humans still need to check the axioms and definitions (to ensure they are &quot;what is meant&quot;), check that the claims are what is desired, and in general humans need to create at least part of the proofs. But <i>no</i> one needs to &quot;understand everything&quot;. Instead, you can see whatever you want to see, and be confident that every step is thoroughly verified.<p>A Metamath-specific video overview is here: <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=8WH4Rd4UKGE" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=8WH4Rd4UKGE</a><p>THAT is where we need to go. We aren&#x27;t ready for it yet, but part of the problem is that we need to agree that this the proper destination.