À suivre la thèse fascinante d'Hervé Aubron dans Le Génie de Pixar, les films entièrement numériques du studio d'Emeryville en Californie donnent à voir bêtes et machines assistées par ordinateur s'évertuant à donner des leçons d'humanité au genre humain. Cette philanthropie numérique apparaît d'autant plus comme une aporie que, de ce genre humain, il n'y a plus grand chose à sauver dans ces films tant il y est présenté sommairement mécanisé par ces mêmes technologies qui permirent à Pixar de délier irréversiblement le dessin animé de la main humaine tenant le crayon. Dans le monde de Pixar, intelligence et affects ont été complètement transférés — qu'elle soit animal anthropomorphisé, marionnette, ou ordinateur le plus sophistiqué — à la Machine (Wall-E, Cars, Toy Story, etc.) laissant alors l'homme à sa solitude, abandonné par ses images, ses sentiments, son intelligence. Quant aux machines, héritières en ligne directe de HAL, elles rêvent, elles soupirent, elles raisonnent et n'ont d'autre recours que de se pencher amicalement sur le sort de cette humanité qui les a trop bien façonnées à son image numérique.
Tout ça serait-il du cinéma ? Pas tant que ça à en juger par le récent Forum 2011 Microsoft Research -- INRIA, qui présentait un second point d'étape de la collaboration de recherche au laboratoire commun de Microsoft Research et de l'INRIA. (Tout cela organisé de main de maître par Pierre-Louis Xech au siège de Microsoft à Issy-les-Moulineaux, sous la haute surveillance britannique — le laboratoire conjoint dépend, en effet, de MSR à Cambridge, UK — des sujets de sa Gracieuse Majesté, Andrew Blake de MSR et le père fondateur de la logique des preuves et inventeur de Quicksort, Sir Anthony Hoare, histoire de tenir un peu la bride à tous ces français...)
Voyons les sujets de recherche :
- Mathematical Components
- Secure Distributed Computations and their Proofs
- Tools and Methodologies for Formal Specifications and Proofs
- Dynamic Dictionary of Mathematical Functions
- ReActivity
- Adaptive Combinatorial Search for E-Science
- Image and Video Mining for Science and Humanities
- A-Brain
un curieux montage qui se lit comme un storyboard du prochain Pixar à l'heure où le Hollywood numérique réanime Tron.
Assia Mahboubi présentait brillamment, par exemple, le projet Mathematical Components dont on pourrait dire malicieusement qu'il vise à abolir la frontière entre programmer et faire des maths. D'ailleurs son motto n'est il pas : « démontrer que les théories mathématiques formalisées peuvent, comme le logiciel, être bâties à partir de composants » ? Et déjà on ne sait plus si cette démonstration est encore déployée dans le domaine des mathématiques où si elle est désormais de nature informatique. Naguère, en 2005, le centre joint de recherche inaugurait sa naissance par un coup d'éclat : un programme informatique auto-certifiant pour démontrer un théorème mathématique historique, celui dit des quatre couleurs. Comme le Toy Story de 1995, performance inaugurale de Pixar, marquait une première — « depuis les frères Lumière » vantait Steve Jobs, jamais à court d'adynatons, à la conférence SIGGRAPH'95 — le théorème des quatre couleurs constituait une première à plus d'un titre ! Sa démonstration initiale dans les années 1970 avait partagé la communauté mathématique : celle ci exigeait le recours à un programme pour vérifier 1478 cas critiques (plus de 1200 heures de calcul à l'époque). L'équipe de Georges Gonthier produisit en 2005 une démonstration du théorème vérifiée par ordinateur, une nouvelle première ; la démonstration elle-même devient programme capable de s'auto-vérifier. La preuve, comme le dessin de Pixar, se libère de la main de l'homme et prend son autonomie, libre enfin de se pencher sur le mathématicien.
Les quatre couleurs, un jeu d'enfant nous disait Mme Mahboubi — on en vient à Toy Story 3 maintenant — les derniers résultats obtenus par le laboratoire, c'est du lourd ! De la mathématique adulte, sérieuse, épaisse, de l'abstrait, du profond, du matériau à Médaille Fields, de la graine de Crafoord : le théorème de Feit-Thompson dont jadis la preuve remplit entièrement un numéro du Pacific Journal of Mathematics en 1963. (Au passage, quel titre somptueux pour une publication de mathématiques...) Mis en coupe réglée par l'approche orientée objet traditionnelle du programmeur bien élevé mais appliquée à une matière première mathématique, le théorème n'a pas résisté au certificateur de preuves numérique et est en bonne voie d'exfiltration vers le cyberespace. Les ordinateurs commencent enfin à faire des maths concluait joyeusement l'oratrice !
Autre illustration de l'exode mathématique vers les plaines magnétiques des disques durs en nuage, l'extraordinaire outil du Dynamic Dictionary of Mathematical Functions (DDMF), qui est toujours présenté sous les dehors innocents du remplacement moderne et en ligne du vénérable ouvrage de référence, les milliers de pages de papier bible de l'Abramowitz et Stegun. Le DDMF, comme le DLMF son homologue américain, sont en fait bien plus que des outils commodes pour érudits de l'analyse numérique. À chaque requête de l'utilisateur, le programme recalcule ou redémontre le résultat à partir des premiers principes, des définitions d'origine, retraçant en quelques mégaflops accélérés des millénaires d'histoire des mathématiques depuis Aristote. Alors que Leonhard Euler, devenu pratiquement aveugle à Saint-Petersbourg, épuisait de longues années de cécité à calculer des solutions aux équations numériques de degrés élevés, imaginant dans ses ténèbres borgésiennes des nombres « irrationnels » et « imaginaires », le DDMF à la précision chirurgicale emplit en un instant les pages Web des mêmes résultats avec une froideur clinique. Il fera un excellent professeur nous assurent ses créateurs et nous envisageons de nombreuses applications dans l'enseignement des mathématiques !
Le projet Image and Video Mining est à l'évidence inspiré de 2001 de Kubrick et de l'excellent HAL. La scène originelle dans laquelle l'ordinateur schizophrène espionne les astronautes, se croyant à l'abri dans l'étanchéité d'un vaisseau aux rondeurs maternelles pour discuter de l'arrêt de l'ordinateur de bord devenu menaçant, simplement en lisant sur leurs lèvres au travers du hublot, nous était ici re-présentée sous une variante à peine camouflée. Dans le film Coffee and Cigarettes de Jim Jarmusch, le HAL moderne du centre commun de recherche, observe et détecte en temps réel les séquences dans lesquelles un ou plusieurs des personnages boivent ou fument — sans erreur et quels que soient les plans. Si les applications concrètes qui furent invoquées pour ces technologies se voulaient rassurantes et écologiquement correctes, Fluminance pour la détection et l'analyse des écoulements et des turbulences, par exemple, dans la lutte contre la pollution, il n'est pas besoin de beaucoup d'imagination néanmoins pour penser à des applications horteféodales d'inspiration nettement plus orwellienne.
Enfin, apothéose, de la pixellisation de l'homme, le projet A-Brain qui jette dans la mêlée numérique toute la puissance de feu des yottaflops du cloud computing pour forger le chaînon manquant entre variabilité génétique et comportement de l'esprit, tel qu'il est progressivement révélé par la révolution de l'imagerie médicale du cerveau. Dans ces mystères d'Eleusis 2.0, l'esprit méditant et agissant devient image numérique Pixar, animée sur nos écrans, calculée par nos GPU, dont on cherche, par une foudroyante inversion du processus de production des films du studio numérique, à retracer la filiation au patron génétique, au dessin initial de l'alphabet acido-aminé qui nous détermine. Ferme résolution et haute résolution conspirent pour achever la mécanisation de l'homme, faire naître le Simulacre de Baudrillard, intégralement démontrable, auto-vérifié, calculé en ligne et en temps réel — mais est-il encore réel à cette échelle ? — banalement doué d'intelligence et de sentimentalité, n'exprimant plus que bienveillance et empathie à très haut débit.
Bienvenue à l'homme Pixarisé.