SMF

Mathématiques et preuves formelles par Assia Mahboubi

Conférence donnée dans le cadre du colloque anniversaire de la SMF.

Assia Mahboubi
INRIA

Laboratory of Digital Sciences of Nantes
Vrije Universiteit Amsterdam, Pays-Bas

 

" 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é.

 

Voir le programme

En savoir plus sur le colloque

 

 

16.03.2022
11:00 - 12:00
IHP, Paris IHP, Paris