Thursday 4 November 2021, 10:30 AM, room 3U47: Récit d’exploration libre d’un traducteur humain dans les galaxies formelles d’univers mathématiques, Roland Coghetto.

1) Comment j'en viens à utiliser Mizar et pourquoi je continue...

2) Huit années de traduction de mathématiques pour la bibliothèque MML : du code et rien que du code ?

3) Tentative de retranscription manuelle de GeoCoq dans Isabel/Hol : un regard naïf sur la complexité complémentaire, concurrente et antagoniste de la traduction manuelle et automatique.

4) Vers d’autres explorations ou un retour sur terre ?