What is Georges Gonthier's language?
It's the language that he developed on top of Coq for the formalization of the four color theorem. It's very compact and very nice. It's also very much not like Mizar (I remember Georges saying to me that he doesn't like the Mizar/Isar style of having a statement with each proof step; he thinks that that is completely the wrong approach; I don't think I agree, but I'm not 100% certain about that...)