You are asking a lot of great questions:
[Are computer proof assistants] any use for a mathematician like me?
Yes. Here is how these systems can help you:
On a very basic level, these systems prevent you from making mistakes. Subsequently, it spares one from the peer review process. One of the proofs of Jordan Curve theorem was carried out by Thomas Hales, as part of his attempt to automatically verify the correctness of the Kepler Conjecture. Hales is basically resorting to automated theorem proving because he feels that his proof, which involves establishing that 50,000 linear programming problems are infeasible (last time I checked) cannot possibly be verified by human peer review.
Most systems (Coq, Isabelle, HOL-Light) built in automation. This helps to inform the informal notion that mathematicians have for what constitutes a trivial, mechanical derivation and what is nontrivial - my rule of thumb is, if a computer can't automatically derive a certain, it's probably something I should illustrate explicitly.
Isabelle/HOL lets you use the automated theorem provers E, SPASS and Vampire to automatically prove propositions, employing the entirety of Isabelle/HOL's Library at their disposal. As Isabelle's library grows, this gains more and more power.
But how to make sure that a machine verified the proof correctly?
As Neel Krishnaswami mentioned above, one way one may be convinced is to learn how to program in pure, functional programming languages such as OCAML or SML and read the source code of systems like HOL-light or Isabelle. In both of these systems I have mentioned, there is a file thm.ml that contains the declarations of theorem constructors. These systems also have facilities for declaring new types. HOL-Light has, along with the basic rules and type constructors, three axioms: extensionality (Liebniz's Law), the axiom of infinity and the axiom of choice.
Moreover, HOL-Light has been designed by the author to exhibit relative self-consistency proofs, just like in set theory. You may read about them here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&rep=rep1&type=pdf
(Here he shows HOL-Light-Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal)
Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?
They all require training to learn. However, for LCF style systems like Coq, Isabelle, and HOL-Light, its like programming languages - once you learn one, you've learned the principles necessary to understand all of them.
Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called "Isar". These systems aren't for dummies, sadly -- one really needs a bit of special training to master these systems. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that its infancy, but it might make Coq better.
In the case of systems that express higher order logic, I assume you are aware that all complete ordered field are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy-Sequences, and has in its library an equivalent formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Algebraically, all of these formulations equivalent, so in practice how the reals are constructed does not matter.
If the syntax is reasonable, it should be easy to write a program verifying that another stream of bytes represents a deduction of the stated theorem from the listed axioms. Can systems like Mizar, Coq, etc, generate input for such a program? Can they produce proofs verifiable by cores of other systems?
The answer is complicated. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in Higher Order Logic. To formulate set theory in Isabelle/HOL and HOL-Light use, one needs to postulate that a kind of object that makes true the axioms of Zermelo Fraenkel set theory exists (this is the route that Isabelle/HOLZF takes). On the other hand, one may embed HOL into ZFC without such difficulty - here is a paper where a translation system for Isabelle/HOL into ZFC is given using the theorem prover LF: http://kwarc.info/frabe/Research/RI_isabelle_10.pdf
Chantal Keller imported HOL-Light into Coq for a MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf, but again the reverse is difficult. Coq has a much more expressive type system than HOL.
HOL-Light and Isabelle/HOL can be inter-translated, however:
- Isabelle/HOL to HOL-Light: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
- HOL-Light to Isabelle/HOL: http://www.springerlink.com/content/m7621r5258r8n711/
One cannot convert Mizar proofs to any other system because it is closed source and not based on an LCF system like the other provers :(