Latest / Le centre de gravité / Quand la preuve devient code

Transcript

Quand la preuve devient code · Le centre de gravité

0:00
Épisode quand la preuve devient code chapitre un l'orange est la
0:05
machine, une orange une machine et 4 siècles entre les 2.
0:10
Année 1611, Johannes Kepler regarde un marchand d'oranges
0:13
quelque part en Allemagne. La pile est parfaitement
0:16
régulière, classique, c'est celle qu'on retrouve sur tous
0:20
les étals d'Europe. Et Kepler, qui n'est pas
0:22
marchand de fruits mais astronome impérial, en tire une
0:25
conjecture brève. Aucune façon d'empiler des
0:28
sphères identiques ne sera jamais plus dense que celle-là 3
0:32
lignes dans un carnet et un problème ouvert pour 4 siècles
0:36
avance rapide. Le 23 février 2026, une équipe
0:39
rassemblée autour de l'E PFL et d'une boîte californienne nommée
0:43
mass incorporated publie un communiqué technique.
0:46
La preuve de Marina Viazovska Fields Medal 2022, version la
0:51
plus aboutie de ce que Kepler avait pressenti, mais en
0:54
dimension 8. Vient d'être intégralement
0:56
vérifié par une machine. Le mot qui compte ici n'est pas
1:00
preuve, c'est machine. Pour mesurer le saut, il faut
1:04
connaître l'épisode d'avant. En 2003, Thomas Hales,
1:06
mathématicien à Pittsburgh, lance un projet baptisé Fly
1:10
spec. L'objectif est de transcrire sa
1:12
propre démonstration de la conjecture de Kepler en
1:15
dimension 3, cette fois dans un langage formel que la machine
1:19
peut vérifier ligne par ligne. Son estimation à l'époque, selon
1:24
ses propres mots, à un séminaire. 20 ans, homme de
1:27
travail. Le projet achève sa course en
1:29
20001411 ans de chantier collectif sur 2 continents.
1:33
Pour viazovska dimension 8, mathématiquement beaucoup plus
1:37
complexe, l'agent d'autoformalisation de mass
1:40
incorporated, baptisé Ghost, a finalisé les derniers verrous en
1:44
5 jours, le codebase est passé de 20000 à 60000 lignes dans cet
1:48
intervalle, et la Communauté qui regardait n'en revient pas.
1:52
L'histoire ne dit pas seulement que l'i a est devenue très
1:54
forte, elle dit que la mathématique vient de changer de
1:57
régime pendant 2000 ans. Un théorème est vrai parce
2:00
qu'une poignée de gens malins l'ont lu et trouvé bon.
2:03
C'est ce qu'on appelle dans le métier la preuve sociale.
2:05
Une Convention silencieuse, jamais écrite nulle part et un
2:10
jour de février 2026 sans tambour, cette convention vient
2:12
de prendre un coup qu'on avait pas vu venir la machine arbitre.
2:15
La question qui ouvre cet épisode est simple.
2:21
À qui profite ce basculement et pourquoi ?
2:23
Des investisseurs qui ne savent pas faire un point fixe viennent
2:26
de poser près de 300000000 de dollars sur la table pour qu'une
2:29
machine fasse de la formalisation chapitre. 2 le Bug
2:35
dans la preuve, plus on regarde de près, plus l'édifice tremble.
2:39
Vladimir voïvodsky, médaille Fields 2002, l'un des esprits
2:45
les plus respectés de sa génération.
2:47
En 1999, woevotski relie l'un de ses propres papiers publiés
2:50
plusieurs années plus tôt, et il découvre que son résultat
2:53
principal est faux, un lem central de sa théorie de la
2:57
Cohomologie Motivique se révèle invalide, aucune coquille de
2:59
surface, un trou structurel au cœur de la démonstration.
3:03
Personne ne l'avait vu pendant 15 ans, pas même lui.
3:07
Wayvotski ne s'en remet jamais vraiment.
3:10
Il consacre la suite de sa carrière à un projet qu'il
3:13
baptise les fondements univalents.
3:17
Conçu pour rendre ce type d'erreur impossible à publier,
3:21
il meurt en 2017 sans l'avoir terminé.
3:22
Voïvodski n'est pas un cas isolé, souvenez-vous d'Andrew
3:26
Wiles juin 1993 à Cambridge, Wils annonce avoir résolu le
3:29
grand théorème de ferma, ouvert depuis 350 ans.
3:33
Standing ovation et reprise médiatique mondiale, héros
3:35
instantané en 40 08h04 mois plus tard, un référé tombe sur un
3:41
trou dans son argumentation. Pas une faute frontale, une
3:48
lacune, un endroit où wiles a sauté un pas.
3:51
Il faut 14 mois supplémentaires et l'aide de Richard Taylor pour
3:54
combler le manque. La preuve définitive sort en 95.
3:58
La première, elle n'en était pas une.
4:00
Et puis il y a hales 1998, Kepler résolu en dimension 3.
4:04
Le journal de référence en mathématiques pures, les annales
4:08
of mathématics, prend 2 ans à statuer quand le comité de
4:12
relecture rend enfin son verdict.
4:16
Il fait quelque chose qu'aucun journal n'avait jamais fait
4:19
avant lui. Il publie la preuve en précisant
4:22
qu'il n'est convaincu qu'à 99%. C'est inédit dans l'histoire de
4:24
la discipline. La méthode classique vient
4:26
d'avouer qu'elle ne suit plus la complexité moderne.
4:29
Ces 3 histoires racontent la même chose.
4:32
La mathématique vit depuis euclide sur un pari implicite,
4:35
le pari que des humains, en se relisant les uns les autres,
4:39
finissent toujours par attraper les erreurs.
4:41
La méthode fonctionnait quand une preuve faisait 40 pages.
4:46
Quand elle en fait 700 comme chez Wils ou qu'elle dépend de
4:49
vérifications numériques sur des centaines de milliers de cas
4:52
comme chez Hales, le pari devient une fiction confortable.
4:55
Et c'est exactement ce que la formalisation en line rend
4:59
visible. Lean, c'est un système où chaque
5:02
pas de raisonnement est mécaniquement vérifié par un
5:04
compilateur. On ne croit plus, on contrôle.
5:08
Le théorème devient un objet binaire vrai ou faux, sans
5:11
intermédiaire interprétatif. Conséquences très concrètes.
5:16
Selon les statistiques publiques de la bibliothèque matlib, la
5:20
base commune des théorèmes lignes contient aujourd'hui
5:22
environ 2,1 1000000 de lignes de code étalées sur 8000 fichiers.
5:26
Chaque ligne est une certitude définitive et chaque ajout vaut
5:30
un théorème de plus qu'on n'aura jamais besoin de revérifier.
5:33
Une cathédrale numérique pousse à vue d'œil et la presse
5:37
économique mainstream n'en parle pas.
5:39
Le Bug dans la preuve n'est pas une anecdote, c'est une
5:42
condition de possibilité. Sans l'aveu collectif que la
5:47
méthode classique vacille, la formalisation reste un caprice
5:50
théorique. Avec cet aveu, elle devient une
5:53
nécessité industrielle. Chapitre 3, on s'est trompé de
5:58
héros. Ce n'est pas l'i a qui pense le
6:00
mieux qui empoche le marché. Quand un grand modèle
6:03
d'intelligence artificielle résout un problème de
6:05
mathématiques olympique, vous le savez, le titre passe en une de
6:08
toutes les médiathèques et on convoque les grands mots, génie
6:11
et AGI. Quand un agent d'auto
6:12
formalisation finit de transcrire la preuve de
6:14
viazovska en 5 jours, vous ne le savez pas.
6:16
Quanta magazine couvre I triple E spectrum suit et le reste du
6:20
monde regarde ailleurs. Cette asymétrie d'attention est
6:23
trompeuse parce que là où va l'argent, ce n'est pas dans la
6:26
première catégorie, c'est dans la 2nde.
6:28
Regardez les chiffres, d'après les données de levée publiées
6:30
par Silicon Angel, Harmonic artificial intelligence a levé
6:34
295000000 de dollars en moins de 15 mois.
6:37
La start-up a été cofondée en 2023 par Vlad Tnef.
6:40
Vous le connaissez peut être ? C'est le patron de Robinhood. 3
6:43
tours enchaînés de 75000000 en septembre 24 à 120000000 en
6:46
novembre 25, avec une valorisation finale d'un ,45
6:48
milliards de dollars. Le produit, baptisé Aristotle,
6:51
est un modèle d'i a qui traduit du langage mathématique naturel
6:54
vers du code Line, formellement vérifiable.
6:59
Médaille d'or aux olympiades internationales de mathématiques
7:02
2025. En face, math Incorporated,
7:05
l'auteur de gauss qui vient de boucler viazovska levée plus
7:08
discrète mais investisseur tout aussi tierwan.
7:11
Et ce n'est pas tout. Deep mind a son projet Alpha
7:13
Proof qui a obtenu une médaille d'argent aux mêmes olympiades.
7:16
La maison mère alphabet considère désormais la preuve
7:19
formelle comme un terrain prioritaire de recherche.
7:22
Pourquoi cet argent ? Parce que la formalisation est,
7:24
du point de vue de l'i. A, la tâche la plus dure qu'on
7:27
puisse imaginer. Tolérance à l'erreur égale à 0,
7:29
le compilateur vérifie immédiatement et toute
7:32
hallucination est rejetée à la racine.
7:34
C'est le banc d'entraînement idéal pour ce que la Communauté
7:36
appelle aujourd'hui les modèles de raisonnement, ceux qui sont
7:39
supposés faire le saut entre prédiction de textes et
7:41
résolutions de problèmes vraiment difficiles.
7:44
En d'autres termes, Maaf Incorporated et Harmonic ne sont
7:47
pas des boîtes de maths déguisées en start-up IA.
7:49
C'est l'inverse, ce sont des laboratoires dit a général, qui
7:52
se servent des mathématiques comme d'un terrain
7:54
d'entraînement particulièrement propre.
7:56
Quand Vlad tnef investit là-dedans, il ne parie pas sur
7:58
le marché des théorèmes vérifiés.
8:00
Il parie sur le fait que celui qui apprend à raisonner en ligne
8:03
apprendra à raisonner. Et tout court.
8:04
Et c'est ici que le grand public se trompe d'épisode.
8:07
Tout le monde attend la nouvelle IA qui découvrira un théorème
8:10
révolutionnaire, le moment Einstein de la machine.
8:12
Mais ce moment, s'il vient, viendra tard et il viendra une
8:16
seule fois. Pendant ce temps, l'i a qui
8:18
formalise s'attaque à des centaines de milliers de
8:20
théorèmes par an, est l'audit et son audit passe à l'échelle.
8:23
Imaginez la scène, un mathématicien à Berlin publie un
8:27
papier. Le lendemain, un agent d'i a
8:29
prend le PDF, le traduit en ligne et signale 3 limes
8:31
intermédiaires non démontrées au passage.
8:34
La revue n'a pas encore commencé son cycle de relecture humaine.
8:37
La machine a déjà rendu son verdict.
8:39
Voilà ce qui arrive pas demain cette décennie, et c'est
8:42
exactement pour ça que les capitaux sont déjà en place.
8:48
Chapitre 4, le dual use, que personne ne nomme.
8:51
Du théorème au noyau militaire, l'outil est le même.
8:54
Sortez 2 Min du laboratoire de mathématiques et Regardez où
8:57
line ou ses cousins directs coke et Isabelle, est déjà utilisé.
9:01
En dehors des théorèmes. Tout commence avec SEL4.
9:04
C'est un noyau de système d'exploitation développé dans
9:06
les années 2000 par une équipe australienne avec financement de
9:09
la Darpa, l'Agence de recherche du Pentagone SEL4A une
9:12
particularité unique au monde, sa correction est
9:14
mathématiquement prouvée ligne par ligne dans un assistant de
9:18
preuve. Cousin de l'Hyne conséquence
9:22
opérationnelle, ce noyau tourne aujourd'hui dans des drones
9:25
militaires et des systèmes embarqués critiques, là où un
9:28
bug ne peut tout simplement pas faire péter le pilote
9:31
automatique. Garanties mathématiques, pas
9:33
garantie probabiliste, même logique côté cryptographie post
9:37
quantique, les nouveaux algorithmes choisis par
9:39
l'Institut américain des standards, le nist, pour
9:42
résister aux ordinateurs quantiques font tous l'objet de
9:44
preuves de sécurité formellement vérifiables.
9:47
La doctrine d'attaque change, on ne fait plus confiance aux
9:50
mathématiciens. Individuelle, on demande la
9:52
preuve binaire que l'algorithme tient sur les blockchains.
9:55
De niveau institutionnel, le sujet est remonté plus vite que
9:58
prévu quand un protocole gère plusieurs milliards de dollars.
10:02
L'audit humain d'un Smart contract ne suffit plus.
10:04
Les acteurs sérieux Ethereum Foundation et aztèque en tête.
10:08
Formalisent lean entre dans les couches d'infrastructures
10:11
financières sans passer par la presse économique.
10:13
Et puis il y a la Chine. Huawei a une équipe dédiée à la
10:17
vérification formelle qui contribue activement aux
10:20
écosystèmes lean. Des coques, la compétition
10:22
stratégique sur le raisonnement machine, on l'observe sur le
10:25
codage des grands modèles d'i a, mais elle se joue aussi très
10:28
intensément et très discrètement sur les preuves formelles.
10:31
Mettons les pièces ensemble. La même technologie qui vient de
10:34
boucler viazovska peut, sans changer d'architecture,
10:37
certifier un firmware d'armes ou un protocole crypto
10:40
institutionnel. Maf Incorporated n'a pas signé
10:43
pour ça harmonique non plus, mais leur outil est exactement
10:47
le bon outil. Et l'État américain qui finance
10:49
la darpa depuis 10 ans sur. Ces sujets le sait, pour un
10:52
dirigeant européen, la question pratique est la suivante, vous
10:55
achetez aujourd'hui des produits, un cloud, un système
10:58
embarqué critique dont la sécurité repose sur un audit
11:01
humain. Dans 5 ans, vos contreparties
11:03
américaines vendront ces mêmes produits avec une preuve
11:06
formelle de correction. Une garantie qualitativement
11:09
différente. êtes-vous prêt à acheter le produit non certifié
11:12
quand le concurrent vend le produit certifié ?
11:15
La réponse est non et l'effet de cascade commence à peine.
11:18
L'i a formelle n'est pas un sujet académique, c'est un.
11:21
Changement d'étalon de qualité pour toutes les couches
11:23
critiques du numérique et l'industrie européenne, qui a
11:26
très peu investi sur l'in va sentir le décalage avant la fin
11:30
de cette décennie. Chapitre 5, la dimension 4, ce
11:33
qui se perd et ce qui s'ouvre. Reprenons le geste de viadovska.
11:37
Sa preuve sur papier est célèbre dans le métier pour une raison
11:40
qui dépasse l'exactitude, elle est belle, elle construit ce
11:43
qu'on appelle une fonction magique par intégration d'une
11:46
série très subtile venue de la théorie des formes modulaires.
11:50
Et cette fonction, comme par grâce, satisfait pile poil les
11:53
conditions qu'il fallait. Les mathématiciens qui la
11:55
racontent en séminaire ont les yeux brillants en ricartant.
11:58
Le grand topologue français disait des formes modulaires
12:01
qu'elles étaient, je cite des objets si riches qu'on se
12:04
demande comment ils peuvent exister.
12:06
Viazovska a fait apparaître l'une des plus belles.
12:09
Cette beauté dans la version lean n'est plus accessible,
12:12
60000 lignes de codes que personne ne lira jamais comme un
12:15
texte. La preuve est devenue une boîte
12:17
noire qu'on exécute. On a gagné la certitude, on a
12:21
perdu la lecture. C'est la première fracture
12:23
qu'ouvre la formalisation. Le théorème change de statut, il
12:27
n'est plus un objet de pensée partagée, il est un module
12:30
logiciel qu'on importe. Matlib devient une
12:32
infrastructure au sens où Linux est une infrastructure avec ses
12:36
mainteneurs et ses dépendances en cascade, contrôlés par une
12:39
poignée d'acteurs qui en gardent silencieusement les clés.
12:42
Pour les mathématiciens, cela pose une question intime, si la
12:45
preuve d'après n'est plus lisible, comment va-t-on trouver
12:48
la preuve d'après d'après l'histoire de la discipline
12:51
montre que les grands théorèmes naissent souvent du regard porté
12:54
sur un autre plus ancien, quand le plus ancien n'est plus
12:57
regardable mais seulement exécutable.
12:59
Où va l'intuition ? Personne ne sait.
13:02
Et puis il y a l'autre côté, celui qui s'ouvre.
13:04
Viazovska a résolu les dimensions 8 et 24 parce qu'il y
13:08
existait par chance des objets mathématiques exceptionnels.
13:12
Les réseaux e, 8 et 2 leachs dans les dimensions
13:15
intermédiaires de 4 à 7. Aucun objet de ce type n'est
13:18
connu, personne ne s'est empilé des sphères de manière optimale.
13:22
Dans ces dimensions, le problème reste ouvert.
13:24
Or, c'est exactement le terrain où une IA qui a digéré la preuve
13:27
de viazovska pourrait peut être proposer des candidats pour la
13:31
fonction magique manquante, pas en cherchant à l'aveugle, mais
13:34
en exploitant la structure formelle d'un théorème déjà
13:37
prouvé. C'est ce que qanta magazine a
13:40
baptisé en avril 2026. La révolution silencieuse des
13:43
maths, le moment où l'i a passe de la vérification à la
13:47
suggestion, voilà la grille de lecture que cet épisode voulait
13:50
poser. La preuve passe du texte au
13:52
programme. Sa validation autrefois sociale
13:55
devient mécanique et le mathématicien individuel n'est
13:59
plus l'unité de production, il rédige le cahier des charges
14:02
qu'une machine exécute. L'i a dans cette nouvelle
14:05
économie gagne sa place non pas par des coups d'éclat de
14:07
découverte, mais par le travail patient d'audit que personne ne
14:11
voulait faire. En 1611, Kepler regardait des
14:14
oranges. En 2026, une machine vient de
14:17
fermer la question qu'il avait posée en 5 jours, la prochaine
14:21
en dimension 4, elle pourrait l'ouvrir toute seule.
14:24
Et c'est là que l'histoire devient intéressante.
14:28
Vous écoutiez quand la preuve devient code.
14:31
Merci d'avoir écouté jusqu'au bout.
14:32
Si cet épisode vous a parlé, partagez le.