L'ordinateur est de plus en plus sollicité dans les démonstrations de théorèmes mathématiques. Dans un premier temps, j'introduirai le sujet en parlant du théorème des 4 couleurs, son histoire et sa preuve. Il s'agit du premier résultat important démontré avec l'aide d'un ordinateur, et cet exemple illustre bien les avantages et problématiques de ce genre d'approches. Puis je parlerai du problème de pavages par tuiles convexes, récemment clôturé en utilisant l'aide de l'ordinateur, et qui présente quelques similitudes avec le théorème des 4 couleurs. Quand on cherche à caractériser les formes convexes pouvant paver le plan (en s’autorisant les rotations et miroirs), seul le cas des pentagones restait ouvert. De 1918 à 2015, 15 différents types de pentagones pouvant paver le plan ont été découverts. Je présente une recherche exhaustive de tous les pentagones convexes pavant le plan, qui permet de clore cette question. La preuve se sépare en deux parties : la première montre, en utilisant la compacité, que l'on peut se limiter à un ensemble de 371 familles, et la seconde est une recherche exhaustive par ordinateur, pour chacune des 371 familles, qui ne trouve aucun nouveau type de pentagones que les 15 types connus.
[L'exposé sera en deux parties de 1h chacune, avec une pause au milieu. Un café sera servi dès 9h45 en salle passerelle.]
