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 it's author John Harrison 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 Harrison shows HOL-Light$-$Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal.

> The definitions should be chosen
> carefully - I don't want to dig
> through a particular construction of
> the reals from rationals to make sure
> that this is indeed the reals that I
> know.

I assume you are aware that all complete ordered fields are isomorphic to one another?  Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another 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.  Since algebraically all of these formulations are provably isomorphic, in practice the details of their construction are hidden from the users. 

> 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 them.  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 in its infancy, but I expect it will ultimately make Coq much easier to use.

> 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 short answer is **YES**, the long answer is **YES, but it's 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 has imported HOL-Light into Coq in her MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf

Importing back from Coq 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][1]
 - HOL-Light to Isabelle/HOL: [http://www.springerlink.com/content/m7621r5258r8n711/][2]

  [1]: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
  [2]: https://doi.org/10.1007/11814771_27

One cannot convert Mizar proofs to any other system because it is closed source, and does not have a small kernel one can use to produce proof code readable by other engines :(