No, I think you're not granting enough charity to what I'm saying.
1. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt.
2. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. Not only that, but the theorem needs to connote something useful. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack.
3. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray.
Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians.