Of course it is not the assistant that gives us ingenuity, but it is the user that, by the use of tactics, tells the assistant how to build the actual proof. When the user thinks the proof is complete it closes the proof construction procedure and a proof object is produced. At this point the proof object is passed to the second module of the assistant which is a proof checker. If the proof is correct the specification is verified and validated.
Of course the crucial point of this process is the proof checker. If there is an error in the proof checker, then the whole procedure is invalid. And so it is crucial to have proof checkers that could be in a sense trusted. And as de Bruijn - one of the pioneers of this approach to formal proof verification - said, we should prefer systems with a small reliable checker. So, here we a kind of trade-off. From one point of view we would like to have very strong logics, because strong logics allow to give better proofs and to prove them in a more concise way. On the other hand we need small proof checkers. And this apparently is a contradiction.
