Mizar documentation / Mizar Checker / Automatical proof writing

[Olivier TEYTAUD <oteytaud@eimi.imi.ras.ru>]

Hi everyone,

 I've just got a short outline about mizar,
and I'd like to read a complete documentation.
Could someone give me references about it ? 

 Will the checker of Mizar be improved later or not ?

 And I'm interested in every information about what
has even been done about automatical proof writing
of simple lemmas.

 Thanks in advance,
  Olivier