[neilkk]

The intuition is that a monkey typing randomly on a typewriter can come up with texts which either are or aren't valid proofs of ZFC or not, and each one which is a valid proof either is a proof of a contradiction or not. To check either of these things is mechanical. If ZFC is inconsistent, eventually the monkey should hit on the inconsistency.