It's absolutely easier for humans to prove complex theorems than it is to encode it on a computer. Consider if your computer proof system only knows about finite numbers, when your proof deals with transfinite numbers. (There is a one-to-one mapping from each integer to each rational fraction, but there no such mapping exists from the integers to the reals, showing that size of the set of reals is fundamentally larger than the size of the set of integers, despite both being "infinite" in size. -- there is more than one type of infinity.) How do you encode that information
Complicated theorems, like the four-color theorem, are different point. Note there though that the original proof of the four-color theorem, which was based on a computer enumeration, was not convincing to many mathematicians when it first came out, in part because it wasn't feasible to verify manually. Researching now, I see that a proof verified by Coq now exists, which I think reduces the amount of distrust.
Yes, mathematicians "come to a consensus." And they make mistakes. Proofs are sometimes believed to be correct for several decades before being shown to be incorrect, though for important proofs - proofs that others depend on - that's extremely rare. But it isn't super handwavy. They've developed processes over time to help identify flaws. This link outlined a few of them: many people work in the same area, so they can cross-check, and workshops and other meetings serve as a way to spread knowledge and get feedback. Note how it will be a couple of years before the proof is published.
If there's a missing crucial aspect, then that may reveal new types of math. Consider the work of Cantor. Quoting Wikipedia, it was "so counter-intuitive—even shocking—that it encountered resistance from mathematical contemporaries such as Leopold Kronecker and [others], while Ludwig Wittgenstein raised philosophical objections. Some Christian theologians (particularly neo-Scholastics) saw Cantor's work as a challenge to the uniqueness of the absolute infinity in the nature of God ... The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics, and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth.""
Nowadays, Cantor's work is considered the origin for set theory.
Part of the training in math is to make those "semantic things" well-defined.
If you go further into the philosophy involved, then you start dealing with formalism, where everything is reduced to symbols manipulated by a grammar (hence how Stephenson's 'Anathem' refers to computers as 'syntactic devices'), and with Zermelo–Fraenkel set theory, which is one of the most common foundations of mathematics. However, then you have things like the continuum hypothesis and the axiom of choice which are not part of the the ZF set theory, leading to ZFC set theory. And at this point I'm well beyond what I know about the philosophy of mathematics.
Suffice it to say that a full formalist description of a theorem, such that it can be reduced to a machine proof, is hard. Take a look at "Principia Mathematica" by Whitehead and Russell. Among other things, it used logic to show that 1+1=2. (See the end of the proof at http://en.wikipedia.org/wiki/File:Principia_Mathematica_theo... - "The above proposition is occasionally useful.") That might give you a idea of what the effort looks like.