|
Une journée de séminaires en hommage à V.A.Veovodsky (1966-2017), mathématicien russe qui rêvait d’une pratique mathématique où les résultats seraient vérifiables par un assistant de preuve.
Après sa médaille Fields en 2002, il s’est attelé à étendre la théorie des types au coeur de l’assistant de preuve COQ (interview).
Son projet “fondements univalents” est en train de créer une révolution des fondements mathématiques et des assistants de preuve.
|