Interopérabilité pour les mathématiques synthétiques dans un assistant à la preuve · Laboratoire Méthodes Formelles, Doctorat · La Géode