Assia Mahboubi - Mathématiques et preuves formelles

La logique mathématique étudie les preuves comme des objets mathématiques : existence, forme, classification, etc. Ces preuves formelles semblent néanmoins bien éloignées des démonstrations, aussi rigoureuse soient-elles, qui constituent la littérature mathématique contemporaine. Les preuves formelles sont par contre des structures de données manipulables par des programmes informatiques, qui permettent de les construire, de les observer, de les vérifier par des procédés mécaniques. Les assistants de preuves sont des logiciels qui permettent d'effectuer ces opérations, en pratique et à grande échelle. Dans cet exposé, on s'efforcera de donner un aperçu illustré des mathématiques que l'on peut faire avec un assistant de preuve, et des bénéfices de cette activité.
Exposé donné dans le cadre des 150 ans de la SMF en 2022.
smf.emath.fr/150-ans-smf

[@liliandelaveau3891]

Merci beaucoup pour la conf ! C’est très cool de voir ce sujet abordé :)

[@Annabelledelrio]

Elle est super bien nichonnée