The space of proofs is enormous. Model checkers and proof assistants will probably become user friendly much sooner than they'll get good enough heuristics to navigate such spaces.