A one-line proposition $A$ can generate a 100-page proof $p(A)$. Since the proof is very long, it's highly suspectable that there is a mistake in it, which cannot be found out even after careful proofread by many people.
So we should write a proof $p(p(A))$ to make sure $p(A)$ is correct. By a similar argument, we should have $p(p(p(A))), p(p(p(p(A)))), \dots$.
This seems ridiculous because $1+1=2$ is commonly known as correct, which doesn't need a complicated proof. So (from my own point of view) it's better to regard a proof as a decomposition of a proposition into a series of axioms. But there are two problems:
How many axioms do we need? Are they consistent?
What is the structure of this decomposition (that makes it hard for a machine to do automatic proof)?
It seems the first problem has something to do with Gödel's Incompleteness Theorem. I'd sincerely thank those who recommend me very clear and illustrative materials about it. I'd also like to know what background will be needed to understand it. I tried to read the original paper but didn't quite understand what are the more fundamental facts that we can rely on to prove this theorem. (Maybe Peano Arithmetic and ZFC?)