Translating Mizar into some standard FOPL-like format?

Hi,

I haven't kept up with this list lately, and I'm curious what is the current
state of efforts to translate the Mizar corpus of theorems and proofs into
some fairly standard first-order-predicate-logic-like formalism?

Has this been done by now?  If so is the translated version of Mizar
available?

If not, what is your general thinking about the most desirable "target
formalism" for the translation effort ... and, what is the status of
partially-complete efforts?

thanks
Ben Goertzel