Résumé
Le deuxième séminaire a été consacré aux utilisations dans la recherche en mathématiques de l’ordinateur en général, et en particulier des assistants de preuve (Coq, HOL, Mizar, etc.). Depuis longtemps employé comme support d’expériences et aide à l’intuition, le calcul sur ordinateur peut aussi contribuer à part entière à la démonstration de grands théorèmes. L’oratrice a développé l’exemple de la démonstration par Helfgott de la conjecture faible de Goldbach, qui fait appel à des encadrements numériques d’intégrales ; elle et ses coauteurs ont pu démontrer formellement ces encadrements via une arithmétique d’intervalles vérifiée en Coq. Cependant, la formalisation « sur machine » des structures algébriques usuelles pose des problèmes subtils notamment liés à « l’ambiguïté typique » entre une structure et son ensemble support. Après les premiers succès, où l’assistance de l’ordinateur a permis d’achever des démonstrations longues (théorème des quatre couleurs, conjecture de Kepler), verrons-nous un nouveau style de mathématiques émerger de l’utilisation de ces assistants ?
