Logo


- Nom Commun - ÉDUCATION-Enseignements Supérieurs | SANTÉ-Médecine | COMMUNICATIONS MÉDIATIQUES-Presse - Position médiale - Morphosémantique - 29/02/2016 - Les Echos - AUTEUR NON IDENTIFIÉ - Lien -
Contexte : "et embrouillée . Un travail de titan , six ans , 170.000 lignes de code . En même temps que cette annonce , paraissait un ouvrage très particulier , « Homotopy Type Theory » : 600 pages écrites de façon collective en six mois par 40 scientifiques de tout âge et de toute origine , conçues en utilisant les nouvelles technologies collaboratives , d' usage courant en logiciel libre . Sous-titré « Univalent Foundations of Mathematics » , c' est le compte rendu d' une année de travail collectif au fameux Institute for Advanced Study de Princeton , autour de mathématiciens-logiciens-informaticiens de haute volée tels Vladimir Voevodsky , médaille Fields 2002 , ou encore Thierry Coquand , pionnier , entre autres , des logiciels de vérification de preuves . Objectif du travail : « Développer de nouvelles fondations pour les mathématiques adaptées aux démonstrations assistées par ordinateur et facilitant la formalisation des mathématiques . » "