Acteurs
Kenneth Appel (1932-2013)
Mathématicien américain. Il sert un temps pour l’armée américaine, suit un programme doctoral à l’université de Michigan et où il obtient son doctorat en 1959. Il travaille pour l’institut pour l’analyse de défense où il mène des recherches de cryptographie. Il rejoint le département de mathématiques de l’université de l’Illinois où il y devient professeur en 1977. C’est pendant cette période qu’il travaille en collaboration avec Wolfgang Haken sur une démonstration du théorème des quatre couleurs qu’ils présentent en 1976.
David Aubin
Historien des sciences mathématiques Il est également chercheur affecté au projet "Histoire des Sciences Mathématiques" de l’Institut de mathématiques de Jussieu. Il est associé au Centre Alexandre Koyré depuis 2002. Ses principaux thèmes de recherche s’articulent autour de l’Histoire des sciences du monde physique aux XIXème et XXème siècles, que ce soient les sciences mathématiques et physiques ou les sciences de la terre et de l’univers. Il s’intéresse particulièrement au métissage des pratiques scientifiques, notamment dans les observatoires ou pendant les deux conflits mondiaux. Voir l'entretien.
Alonzo Church (1903-1995)
Mathématicien, logicien, philosophe et historien de la logique américain Professeur de mathématiques à l'université de Princeton, il apporte une formulation rigoureuse des conditions que doit satisfaire un critère d'assomption ontologique. Il est connu pour avoir développé la notion de lambda-calcul, et pour ses travaux sur la décidabilité dans les systèmes formels.
Pierre-Evariste Dagand
Chercheur en informatique. Il entre à l’ENS à Rennes, où il étudie les systèmes et les télécommunications, et s'intéresse aux systèmes distribués. Puis, il effectue un post-doctorat à l’Inria où il intègre l’équipe Gallium dont les travaux s’orientent vers le design, la formalisation, l'implémentation des langages et des systèmes de programmation. Il devient par la suite chercheur au CNRS au LIP6 (Laboratoire d'informatique de Paris 6). Ses recherches s’articulent autour de la création de systèmes logiciels sécurisés, mais concernent également la vérification formelle et notamment les usages des assistants de preuves en informatique. Voir l'entretien.
Kurt Gödel (1906-1978)
Logicien et mathématicien autrichien, naturalisé américain. Physicien de formation, il s'oriente rapidement vers les mathématiques. Il obtient son titre de docteur en 1929. Sa thèse, et surtout un article publié en 1931 intitulé "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme" soit "De l'indécidabilité formelle des Principia Mathematica et des systèmes équivalents", donneront à Gödel une réputation internationale : il y présente ses deux théorèmes d'incomplétude, qui réduisent à néant les espoirs de Hilbert.
Georges Gonthier
Chercheur canadien en informatique. Ses domaines d'intérêt sont la conception des langages de programmation et leur sémantique, ainsi que la vérification formelle des programmes informatiques et des théories mathématiques. Il est notamment connu pour le développement complet, mécaniquement vérifié par ordinateur de la démonstration du théorème des quatre couleurs. Après avoir travaillé pour le centre Inria et le laboratoire de recherche Microsoft à Cambridge, il participe à la création du laboratoire commun Inria – Microsoft Research. Il rejoint par la suite l’équipe SPECFUN du centre Inria Saclay, où il poursuit ses projets de recherche, notamment la démonstration informatisée du Théorème de Feit-Thompson.
Wolfgang Haken
Mathématicien allemand, spécialiste de la topologie. Il ne reçoit pas une éducation classique de mathématicien. À l’université de Kiel, le département de mathématiques est tenu par un unique professeur, qui enseigne sans ouvrages de référence (à cause des destructions liées à la guerre). Il est cependant introduit aux conjectures principales de sa génération, dont le théorème des quatre couleurs. Il travaille pour Siemens en tant qu’ingénieur électrique en poursuivant parallèlement ses recherches sur la conjecture de Poincaré, le problème des nœuds, et le théorème des quatre couleurs, dont il propose une démontration en 1976 avec son collègue Kenneth Appel.
David Hilbert (1862-1943)
Mathématicien allemand. En 1900, il présente ving-trois problèmes tenant les mathématiciens en échec, prémisses du "programme" qu'il développe dans les années 1920. Cependant, ses espoirs se heurtent au paradoxe de Russell et aux théorèmes d'incomplétude de Gödel. Ses recherches et ses découvertes recouvrent un vaste domaine s'étendant de la théorie des invariants à la métamathématique et à la théorie de la démonstration, en passant par la théorie du corps de classes, la géométrie algébrique, le calcul des variations et les équations intégrales.
Donald MacKenzie
Sociologue britannique et professeur de sociologie à l'université d'Édimbourg. Ses travaux constituent une contribution importante au domaine des Sciences, Technologies et Société. Il s’intéresse principalement à l'histoire des statistiques, de l'eugénisme, des armes nucléaires et de l'informatique, et plus précisément à l’histoire de la mécanisation des preuves mathématiques dans son ouvrage Mechanizing Proof.
Assia Mahboubi
Mathématicienne chargée de recherche à l’Inria. Elle étudie les mathématiques à l’ENS de Lyon, et se forme en parallèle aux mathématiques discrètes et à la logique informatique, avant d’effectuer un master 2 consacré à la théorie des langages de programmation. Elle rejoint l’équipe de Georges Gonthier, et travaille sur la formalisation à l’aide du logiciel Coq, notamment dans sa démonstration du théorème de Feit-Thompson. Voir l'entretien.
Robert Pollack
Mathématicien américain et professeur assistant à l’Université de Boston. Ses thèmes privilégiés de recherche s’articulent autour de la théorie des nombres, des courbes elliptiques, des formes modulaires et de la théorie d’Iwasawa. Par ailleurs, il bâtit une réflexion sur l'impact des assistants de preuves en mathématiques et tente de comprendre la façon dont il est possible de se fier aux preuves assistées par ordinateur (machine-checked proofs) en proposant une approche pour croire les preuves formelles.
Casey Rufener
Philosophe des sciences et épistémologue américain. Titulaire d’un double diplôme en philosophie et en neurosciences du Macalester College à Saint Paul, ses principaux intérêts de recherche résident dans les liens entre la philosophie du langage, la philosophie des mathématiques, la logique et des fondements épistémologiques de la modalité. Il s’intéresse également à la métaphysique de la conscience, aux fondements philosophiques de la science cognitive, à la mécanique quantique, et à la sémantique.
Bertrand Russell (1872 - 1970)
Mathématicien, logicien, philosophe et épistémologue britannique. À Cambridge, Russell travaille avec Whitehead aux fondements des mathématiques, en cherchant à concevoir un système de logique mathématique s'appuyant sur une analyse abstraite de la pensée. En 1902, il découvre son célèbre paradoxe, l'ensemble de Russell. Pour le résoudre, il souhaite réduire les mathématiques à une logique constituée d’un nombre restreints d’axiomes. Inspirés par Peano et Frege, Russell et Whitehead réussissent à faire dériver les principaux résultats de théorie des ensembles et d'arithmétique, d'une liste bien définie d'axiomes et de règles de déduction, en utilisant un langage logique-symbolique particulier. Ils publient ces résultats dans l'oeuvre monumentale Principia Mathematica, qui fonde la théorie des types.
Jean-Jacques Szczeciniarz
Directeur du département Histoire et Philosophie des Sciences de l’Université Paris Diderot. Les travaux de ce chercheur ont la particularité d’être ceux d’un philosophe et mathématicien. Après avoir enseigné à l’université de Nanterre puis de Bordeaux, il devient professeur à l'Université Paris Diderot où il contribue à la création du département d’histoire et de philosophie des sciences. En parallèle, il mène plusieurs projets de recherche au sein du laboratoire SPHERE, où il dirige un groupe de recherche sur la philosophie des mathématiques et s’intéresse pour la géométrie complexe. Voir l'entretien.
Alan Turing (1912-1954)
Mathématicien et cryptologue britannique, considéré comme le père fondateur de l'informatique. Durant ses études au King’s College, Turing s'intéresse aux travaux de mécanique quantique de John Von Neumann, ce qui l'amène à étudier les probabilités et la logique. En 1935, il met au point le concept d'une machine universelle, qui formalise la notion de problème résoluble par un algorithme. Pendant la guerre, il rejoint l'équipe de scientifiques chargés de décoder la machine Enigma utilisée pour crypter les communications nazies, et contribue à mettre au point un des premiers calculateurs, "la Bombe".
Thomas Tymoczko (1943-1996)
Philosophe spécialiste de la logique et des mathématiques. Il obtient un diplôme à Harvard et un doctorat de philosophie en 1972. Enseignant au Smith College (Massachusetts) de 1971 à sa mort il publie nombre d’articles en rapport au théorème des quatres couleurs, notamment “Le théorème des 4 couleurs et sa signification philosophique” où il rejette la validité d’une preuve par informatique. Selon lui, ces preuves ne répondent pas à l’impératif d’a priori d’une preuve traditionnelle.
Vladimir Voevodsky
Mathématicien russe. Il est connu pour ses travaux sur la notion d'homotopie, qui lui ont valu une médaille Fields en 2002. Par crainte que la théorie axiomatique des ensembles se révèle inconsistante au sens de Gödel, il entreprend depuis plusieurs années de formaliser l'ensemble des mathématiques existantes en théorie des types homotopiques.
Théo Zimmermann
Chercheur en informatique. Après une classe préparatoire il intègre l’ENS-Ulm pour y suivre un parcours en informatique. Il s'intéresse d'abord à la vérification de programmes et de composants matériels, comme une application de Coq en particulier ou des systèmes de preuves en général. Il est actuellement en thèse au sein des équipes πr² et PPS de l’Institut de Recherche en Informatique Fondamentale (IRIF) à l’Université Paris-Diderot. Il travaille à la mise au point d’un outil d’aide à la rédaction de démonstrations mathématiques reposant sur Coq. Par ailleurs, il s’intéresse aux enjeux du crowdsourcing, et plus précisément à la collaboration de masse sur le web grâce à l’open research. Voir l'entretien.
