The proof is a human interaction: it is a series of papers written by one person to transmit their ideas to other people.

If it were a giant Coq term then sure, you can ignore those pesky details like "understandability".