This is why we need to move
away from depending on just humans to verify proofs. The goal shouldn't be "does a human fully understand the whole thing" but "is it proven to be true?"
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's required for publication: http://www.cs.ru.nl/%7Efreek/100/
I do a lot with Metamath. The largest Metamath database, which uses classical logic & ZFC set theory, can be seen here: http://us.metamath.org/mpeuni/mmset.html 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 "what is meant"), check that the claims are what is desired, and in general humans need to create at least part of the proofs. But no one needs to "understand everything". Instead, you can see whatever you want to see, and be confident that every step is thoroughly verified.
A Metamath-specific video overview is here: https://www.youtube.com/watch?v=8WH4Rd4UKGE
THAT is where we need to go. We aren't ready for it yet, but part of the problem is that we need to agree that this the proper destination.
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's required for publication: http://www.cs.ru.nl/%7Efreek/100/
I do a lot with Metamath. The largest Metamath database, which uses classical logic & ZFC set theory, can be seen here: http://us.metamath.org/mpeuni/mmset.html 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 "what is meant"), check that the claims are what is desired, and in general humans need to create at least part of the proofs. But no one needs to "understand everything". Instead, you can see whatever you want to see, and be confident that every step is thoroughly verified.
A Metamath-specific video overview is here: https://www.youtube.com/watch?v=8WH4Rd4UKGE
THAT is where we need to go. We aren't ready for it yet, but part of the problem is that we need to agree that this the proper destination.