durée : 00:58:23 - La Science, CQFD - par : Natacha Triou, Antoine Beauchamp - Un projet collaboratif s’est donné pour objectif de formaliser la preuve du théorème de Fermat afin de pouvoir l’apprendre à un ordinateur. Quel est l’enjeu de cette formalisation ? Pourquoi est-ce si compliqué ? Qu’est-ce qu’un assistant de preuve et quel est son rôle en mathématiques ? - réalisation : Olivier Bétard - invités : Riccardo Brasca Maître de conférences au département de mathématiques à l'Université de Paris-Cité; Assia Mabhoubi Directrice de recherche à l’INRIA à Nantes