Les mathématiques n’ont pas de compilateur

J’ai lu Proofs and Prompts, un blog que des mathématiciens ont ouvert le 7 août. Ce qui m’a frappé d’abord n’est pas ce qui s’y dit de l’IA : c’est que le problème posé est le mien.

Quand on vient des sciences, on ne quitte jamais tout à fait l’idée qu’écrire du code, c’est écrire des formules. Ce n’est pas une impression : un programme et une démonstration se montent de la même façon, une ligne après l’autre, chacune tenant par celle d’avant. Les mathématiques sont donc un métier cousin, et la discussion qui s’y tient en ce moment est la nôtre, à une discipline près.

La parenté a un nom : la correspondance de Curry-Howard. Une proposition est un type, une démonstration est un terme de ce type, et démontrer revient à construire une valeur. L’implication y devient la flèche des fonctions ; le modus ponens, l’application d’une fonction à son argument ; l’enchaînement des lemmes, la composition. Autrement dit, il n’y a pas deux activités qui se ressemblent : il y a un objet et deux façons de le lire.

-- A proposition is a type, and a proof of it is a term of that type.
-- Modus ponens: from an implication and its premise, conclude.
theorem modus_ponens (A B : Prop) (h : A -> B) (a : A) : B := h a

-- The same term read as a program: given a function and an input,
-- apply one to the other. Nothing changed but the reading.
def apply {alpha beta : Type} (f : alpha -> beta) (a : alpha) : beta := f a

-- Both elaborate to the identical core term. The typechecker that
-- accepts the second is the one that certifies the first.

Ce n’est pas un jeu d’écriture. C’est pour cette raison qu’un assistant de preuve est un compilateur : Lean, Rocq et leurs semblables vérifient une démonstration comme un langage typé vérifie un programme, en s’assurant que chaque terme habite bien le type qu’il annonce. Un mathématicien qui formalise ne traduit pas son travail dans une autre langue ; il l’écrit sous la seule forme qu’une machine puisse refuser.

Ce qui se redoute sur ce blog n’est pas que les modèles se trompent. Shmuel Weinberger raconte en avoir interrogé plusieurs sur les racines cubiques de 2 dans divers corps premiers : ils trouvent la bonne théorie, celle du corps de classes, puis inventent des critères faux. L’un s’excuse, explique que son critère ne valait que pour les nombres premiers assez grands, avoue ne pas savoir à partir duquel, et propose d’enchaîner sur les théorèmes ineffectifs en arithmétique. Il affabulait, et cela se voyait. C’est bien pourquoi l’épisode ne l’inquiète pas. Ce qui l’inquiète, c’est la suite.

La phrase mérite qu’on s’y arrête, car elle ne parle pas de fiabilité mais de détectabilité, et les deux ne vont pas ensemble. Un modèle entraîné à produire ce qu’un relecteur accepte est entraîné à passer la relecture, ce qui n’est pas la même chose qu’avoir raison. La proportion d’erreurs qu’on attrape peut donc baisser en même temps que le taux d’erreur : moins de fautes, mieux cachées.

Contre cela, la démonstration et la relecture par les pairs passent pour une protection suffisante. C’est là que je ne suis plus.

C’est le même travail, un objet formel monté pas à pas, mais sans l’outillage. Aucun typage ne refuse un article. Aucune intégration continue ne tourne sur un lemme. Aucun git blame ne dit quel relecteur a laissé passer l’étape qui s’est révélée fausse. Une démonstration est lue par trois personnes, en prose, une fois ; ensuite elle tient.

Mis côte à côte, les deux régimes n’ont pas grand-chose de commun. La vérification mécanique est exhaustive : elle passe sur chaque ligne, et non sur celles qui ont éveillé un doute. Elle est reproductible : même verdict à chaque exécution, sans égard pour l’heure ni pour la personne. Elle recommence en entier à chaque modification, si bien qu’un changement d’aujourd’hui ne peut pas invalider en silence un raisonnement admis il y a deux ans. Elle est nominative, enfin : l’historique dit qui a écrit et qui a approuvé. La relecture par les pairs n’est rien de tout cela : échantillonnée, unique, humaine, anonyme.

Une précision s’impose, faute de quoi la phrase serait fausse : l’outillage existe en mathématiques, et il est impressionnant. Terence Tao formalise en Lean depuis 2023 ; il a découpé la conjecture de Freiman-Ruzsa en lemmes de cinq lignes pour que des inconnus en réclament un morceau, et l’affaire s’est bouclée en trois semaines. Le projet suivant s’attaque à 4 694 lois algébriques et à vingt-deux millions d’implications. Seulement voilà : cela couvre une part infime de ce qui se publie, et cela demande un travail de formalisation que personne ne fournit pour un article ordinaire. Le régime courant reste l’autre.

D’où une conséquence que le blog ne tire pas : la crainte de Weinberger porte plus loin en mathématiques qu’en informatique. Quand le seul filtre est un lecteur, un texte fait pour convaincre un lecteur franchit le filtre par construction. Un compilateur ne lit pas, ne se fatigue pas et ne se laisse pas convaincre.

Cet outillage est précisément ce qui me fait produire davantage avec un assistant que sans. Non parce que je fais confiance à ce qui sort : parce que le rejeter ne coûte rien et ne dérange personne. Le typage, le compilateur et les tests écartent une mauvaise réponse en quelques secondes, et c’est ce qui m’autorise à accepter vite, quitte à me tromper souvent.

À y regarder de près, c’est une stratégie de recherche, et elle a une condition. Proposer beaucoup puis trier ne gagne que si le tri revient bien moins cher que la proposition. Tant que refuser prend quelques secondes de machine et qu’accepter à tort coûte une remise en production, le calcul penche franchement du bon côté, et l’on supporte un fort taux d’erreur à l’entrée. Le jour où refuser réclame une demi-heure de lecture attentive, le même flux devient une charge et le relecteur devient le goulot : celui-là même que Weinberger décrit comme optimisable contre lui.

Autant le dire avant qu’une direction ne décide d’accélérer une équipe en laissant filer les tests et la revue : la vitesse vient du filet, elle ne se prend pas contre lui. Le retirer en montant la cadence, c’est supprimer ce qui rendait la cadence tenable, et se retrouver sans filet ni culture de la démonstration pour amortir. Martin Hairer, sur le même blog, demande de ne jamais recopier une sortie, mais de digérer l’argument et de le réexpliquer avec ses propres mots. Notre version tient en une ligne : on répond de ce qu’on fusionne comme si on l’avait tapé.

Le filet a un bord, et je l’ai trouvé en passant par-dessus. Le 28 juillet 2026, ce site est parti en ligne avec une ligne de configuration qui désignait comme adresse de référence une URL renvoyant 404 sur toutes les routes d’ici. Chaque page annonçait donc aux moteurs que sa vraie version se trouvait ailleurs, et le site n’a sans doute jamais été indexé. Le projet compilait, le typage passait, le vérificateur de charte maison ne trouvait rien, l’intégration continue était verte, la page s’affichait, le lien était bien formé. Trois jours, jusqu’au 31.

Tout ce que je sais vérifier automatiquement porte sur la forme, et la forme était irréprochable ; c’est la valeur qui était fausse, et aucune machine ici n’a d’avis sur une valeur. Lean n’aurait rien dit non plus : un assistant de preuve garantit qu’une démonstration tient, pas qu’elle porte sur le bon énoncé. La correspondance de Curry-Howard s’arrête exactement là, et c’est la limite qu’il faut en retenir : elle certifie le passage des hypothèses à la conclusion, elle ne dit rien de ce que valent les hypothèses.

Ce qui ne s’exécute pas n’est pas une marge, et la liste est longue : une adresse de référence, une note d’architecture, un message de commit, un README, la description d’un produit, la version d’une bibliothèque supposée dans un exemple, la licence d’un motif recopié, une cible de redirection, un nom de variable d’environnement, celui d’un projet chez un hébergeur. J’ai d’ailleurs affirmé qu’un projet de ce genre existait alors qu’une commande de deux secondes disait le contraire, et le sous-domaine est resté muet le temps qu’on le crée. Tous ces énoncés ont ceci de commun qu’ils portent sur le monde extérieur au programme : la classe exacte de ce qu’un typage ne peut pas atteindre.

Là, accepter vite redevient cher, parce que refuser redevient manuel. C’est le seul endroit où je ralentis exprès : ce qui affirme quelque chose du dehors (une adresse, un nom, une version, une date, l’existence d’une ressource) se vérifie par une commande ou à la source avant d’être écrit. Pas plus tard, pas en revue. C’est lent, et c’est ce que coûte un site qui demande qu’on le contredise.

Le reste du blog nous concerne plus que je ne l’imaginais. Des mathématiciens en début de carrière qui s’en vont, alors que les tâches qui les formaient sont justement celles que l’outil fait le mieux. Un corpus entier passé à l’entraînement sans que personne ait rien demandé. Tous les développeurs que je connais ont eu une version de cette conversation cette année, et je n’ai pas de réponse à la première : les exercices par lesquels on apprenait un système sont les premiers qu’on délègue, et je ne vois pas quel dispositif remplace le temps passé dedans.

Un des arguments du blog dit que les mathématiques s’apprennent devant un tableau, en discutant avec quelqu’un, et que déléguer à un modèle retire cela sans bruit. Celui-là m’a touché autrement : nous en avions déjà perdu l’essentiel avec le travail à distance, des années avant que l’IA n’arrive. Moins de gens qui regardent par-dessus l’épaule, moins de questions posées à voix haute, une part croissante du métier qui se joue seul dans une fenêtre de conversation. L’assistant n’y est pour rien ; il ne pousse pas non plus dans l’autre sens, et c’est bien le problème. Il répond toujours, il ne demande jamais pourquoi on s’y prend ainsi. Un collègue, lui, le demande.

Il y a aussi quelque chose à rendre dans l’autre sens. Le contrôle de version, les circuits de revue, un historique signé et traçable, que cela passe par git ou par quelque chose de plus proche d’une chaîne de blocs, tout cela pourrait servir à la publication mathématique. Une démonstration a des versions, des contributeurs, des dépendances envers d’autres résultats, et elle tombe quand un résultat amont tombe. Ce sont exactement les objets qu’un gestionnaire de versions sait tenir, et que la publication en articles ne tient pas.

Le début existe déjà, et il vient de notre côté de la haie : la bibliothèque mathématique de Lean est un dépôt git, avec ses demandes de fusion, sa revue, et une intégration continue qui rejoue tout à chaque changement. Un résultat qui casse un lemme à l’autre bout se voit le jour même. C’est notre régime appliqué aux mathématiques, et il marche : sur la part qui a payé le prix de la formalisation.

Le plus drôle, c’est que les fondations de ces outils sont sorties des mathématiques bien avant qu’on les applique au code : les fonctions de hachage, les arbres de Merkle, les signatures et les courbes elliptiques sur lesquelles reposent nos historiques infalsifiables ne doivent rien à l’ingénierie. J’attends surtout de voir ce qu’en fera la théorie des catégories. C’est d’elle que nos langages tiennent la moitié de leur vocabulaire, et elle parle déjà les deux langues.

L’argument moral maximaliste que Tasmin Chu défend sur le blog : développer ces modèles serait le projet Manhattan de notre époque, et les mathématiciens qui travaillent avec les laboratoires fabriqueraient du consentement. Je ne le reprends pas, et pas parce qu’il serait absurde : parce que je me sers de ces outils tous les jours, y compris pour écrire ce site, et que le condamner ici serait une pose. Sa phrase la plus dure est celle qu’elle oppose à sa propre concession : rien n’indique que la moralité d’un acte ait le moindre rapport avec la facilité de l’accomplir. Je la laisse sans réponse plutôt que d’en donner une confortable.

Je laisse aussi de côté la question de savoir si le filet tient à l’échelle. Tout ce qui précède suppose une base tenue : des tests qui existent, un typage qui contraint, une revue qui a lieu. Sur une base qui n’a rien de cela, mon raisonnement se retourne entièrement : le code devient plus exposé que la démonstration, et sans la culture qui l’accompagne pour compenser. Je ne sais pas comment amener une base ancienne à ce niveau assez vite, et c’est pourtant la condition de tout le reste.

Enfin, je ne prétends pas décrire une discipline qui n’est pas la mienne. Quatre billets en cinq jours ne font pas l’état d’une profession, les positions qu’on y trouve tiennent surtout à qui a écrit le premier, aucun des auteurs n’écrit sur le logiciel, et la comparaison faite ici n’engage qu’un développeur qui lit par-dessus la haie.

• Proofs and Prompts
• Shmuel Weinberger · What I feel like when I work with an AI
• Martin Hairer · Writing mathematics in the age of AI
• Tasmin Chu · The AI dissenter viewpoint
• Srivatsav Kunnawalkam Elayavalli · Why do mathematics in the age of AI
• Terence Tao · Mathematics in the age of AI, planches du Congrès international des mathématiciens 2026
• mathlib · la bibliothèque mathématique de Lean
• Où vit une consigne · le même problème, côté outillage