This has been on my mind lately! Especially in light of the many incomprehensible but machine-checkable proofs we've been hearing about.

Occam's Razor is a useful heuristic, but it biases us towards simpler explanations.