This is for CoQ, which is only one of many theorem provers/checkers. Differences between them aren't only notational; they also can also be in the set of axioms they build from.
I don't believe what you believe though. Certainly, the 'many people could understand the proof' is only true in the 'could, if they were willing to spend years studying them' sense. For example, I think I could understand Wiles' proof of Fermat's last theorem, but as it stands, I bet it could take me a month to even understand what its first paragraph is talking about. There will be thousands, maybe even millions, of people in the same boat.
I don't think so. For example, great project at Github's got success based on great documentation. Mathematical theorem's proofs are also delivered with full documentation. It's called documentation when implicitly anyone interested in can understand the documentation. For the Wiles' proof, we don't know the proof/theorems in it before we know it. In short, we need standards to the modern math.
This is for CoQ, which is only one of many theorem provers/checkers. Differences between them aren't only notational; they also can also be in the set of axioms they build from.
I don't believe what you believe though. Certainly, the 'many people could understand the proof' is only true in the 'could, if they were willing to spend years studying them' sense. For example, I think I could understand Wiles' proof of Fermat's last theorem, but as it stands, I bet it could take me a month to even understand what its first paragraph is talking about. There will be thousands, maybe even millions, of people in the same boat.