Intuition may not be the right word but there's a massive gap between proofs mathematicians find acceptable and proofs generated by automated proof systems like

Intuition may not be the right word but there's a massive gap between proofs mathematicians find acceptable and proofs generated by automated proof systems like coq. Mathematicians need to be convinced that in principle a proposition could be stripped down to axioms and syllogisms. It turns out that it's quite hard to do that stripping-down in practice.