Après Leyde

En mai 2026, un modèle interne d’OpenAI a produit un contre-exemple à une conjecture d’Erdős datant de 1946 sur les distances unitaires, un problème qui était resté ouvert pendant quatre-vingts ans. Le résultat est réel : un article complémentaire rédigé par des mathématiciennes et mathématiciens externes l’a vérifié, et Gowers a déclaré qu’il le recommanderait sans hésitation pour publication dans les Annals. Certaines et certains d’entre nous ont été impressionnés, d’autres alarmés; pour ma part, j’ai ressenti les deux. Mais il vaut la peine d’être précis sur ce qui s’est passé, car les détails sont au cœur de l’argument. La machine a trouvé la construction. Des êtres humains l’ont vérifiée, simplifiée et ont retracé les idées sur lesquelles elle reposait jusqu’à des travaux antérieurs d’Ellenberg, de Venkatesh et d’autres — des travaux que le modèle n’a ni identifiés ni cités; établir cette filiation est demeuré une tâche relevant de la recherche humaine. Et quelques mois auparavant seulement, des dirigeants de la même entreprise avaient affirmé sur les réseaux sociaux que son système avait résolu dix problèmes d’Erdős, une affirmation retirée quelques jours plus tard lorsqu’il s’est avéré qu’elle consistait en grande partie à redécouvrir des résultats déjà connus, comme l’a souligné le mathématicien qui tient cette liste à jour. Le triomphe et l’embarras nous enseignent la même leçon : la machine peut maintenant trouver de vraies mathématiques, mais elle ne peut pas, à elle seule, déterminer ce qui est nouveau, ce qui est correct ou sur quels travaux elle s’appuie.

Un deuxième exemple est apparu en juillet, et il prend une tournure différente. Levent Alpöge a annoncé un contre-exemple à la conjecture jacobienne, ouverte depuis que Keller l’a formulée en 1939 : une application polynomiale explicite de C³ dans lui-même dont le déterminant jacobien est la constante −2, mais qui envoie néanmoins trois points distincts sur la même image. La conjecture est donc fausse en dimension trois et, en ajoutant des coordonnées identiques, dans toute dimension supérieure; le cas du plan demeure ouvert. La question lui a été posée par Akhil Mathew, et le contre-exemple est issu de quelques heures de travail avec Claude Fable 5 d’Anthropic. Des mathématiciennes et mathématiciens ont immédiatement vérifié le calcul et, en quelques jours, celui-ci avait été formalisé dans un assistant de preuve, et d’autres conséquences en avaient été tirées.

Deux aspects de cet épisode méritent notre attention. Le premier est que n’importe qui peut le vérifier : il suffit de calculer un déterminant et de constater que trois points se retrouvent sur la même image, et de nombreuses mathématiciennes et nombreux mathématiciens l’avaient fait dans la journée. Une conjecture vieille de quatre-vingt-sept ans a été résolue en un après-midi, non pas parce que quelqu’un faisait confiance à la machine, mais parce que l’objet qu’elle avait produit était facile à vérifier. C’est une propriété qu’il vaut la peine de rechercher dans un résultat et qu’il vaut la peine d’exiger.Le deuxième aspect concerne ce que la vérification ne permet pas d’obtenir. Une fois écrite, l’application semble miraculeuse. Terence Tao l’a ensuite reconstruite : l’application provient de la multiplication de polynômes entre eux et elle n’est pas injective parce qu’un même produit peut provenir de factorisations différentes. Il ne reste alors plus rien de miraculeux — mais le miracle n’a disparu que lorsqu’un être humain l’a expliqué. La machine a produit l’exemple; un être humain en a donné la raison. Cette répartition du travail pourrait être caractéristique d’une grande partie de ce qui nous attend, et c’est pourquoi le reste de cette note s’attarde sur la compréhension plutôt que sur la seule certification.

La Déclaration de Leyde sur l’intelligence artificielle et les mathématiques a été publiée le 2 juin et a reçu l’appui de l’Union mathématique internationale dès le lendemain. Je l’ai signée et je demande à la Société mathématique du Canada de la prendre au sérieux.

Sa principale préoccupation n’a rien de la science-fiction. Les systèmes actuels produisent des arguments qui ressemblent à des démonstrations et qui n’en sont pas : ils sont fluides, plausibles et erronés d’une manière difficile à déceler. Notre littérature est un édifice dont chaque étage repose sur celui qui le précède, et un nombre suffisant d’erreurs bon marché et largement recopiées à la base peut le rendre dangereux. La Déclaration ajoute à cela deux autres préoccupations. Les modèles reproduisent les résultats obtenus par des êtres humains sans mentionner les personnes qui les ont trouvés. Et les démonstrations générées au sein de systèmes propriétaires, auxquels les universitaires ne peuvent pas accéder, confieraient l’orientation des mathématiques à des entreprises plutôt qu’aux mathématiciennes et mathématiciens.Les solutions qu’elle propose sont modestes et justifiées : divulguer l’utilisation de l’IA, continuer à publier dans des revues évaluées par les pairs et exiger qu’un résultat puisse être vérifié sans accès à des systèmes propriétaires. Une démonstration que seul un modèle payant peut vérifier n’est pas une démonstration dont la communauté est réellement maîtresse.

Je veux être prudent ici, car il est facile de mal interpréter mes propos. La Déclaration n’est pas une plainte contre les machines, et cette note non plus. Plusieurs de ses auteurs conçoivent ces systèmes dans le cadre de leur travail. Bien utilisée, une IA est une assistante rapide et infatigable, et je ne souhaite pas la renvoyer. La question de savoir si les mathématiciennes et mathématiciens utiliseront ces outils est déjà réglée; nous les utilisons. Les questions qui restent sont d’ordre pratique : selon quelles règles et qui les établit.

Il existe même une technologie qui s’attaque directement à la première préoccupation. Une démonstration écrite dans un système comme Lean et vérifiée à l’aide de sa bibliothèque, Mathlib, ne peut pas dissimuler une lacune : le noyau n’accepte rien sur la seule base de sa plausibilité. Pour être précis, il garantit l’énoncé tel qu’il a été encodé, et non que nous avons encodé l’énoncé que nous voulions exprimer — cette vérification demeure la nôtre. Mais l’étape simplement plausible, celle qui semble correcte à la lecture et qui pourtant échoue, est précisément ce qu’il refuse.Ce n’est pas encore une solution générale. La majeure partie des mathématiques n’est pas du tout formalisée, et la formalisation d’un théorème sérieux a, jusqu’à récemment, été un travail lent. Cela change rapidement, et pas dans une direction simple : la réfutation de la conjecture sur les distances unitaires a été formalisée dans Lean dans la semaine suivant son annonce, en s’appuyant d’abord sur deux résultats qui ne figuraient pas encore dans la bibliothèque. Cinq semaines plus tard, elle avait été entièrement formalisée, sans rien supposer au-delà des axiomes — par une autre machine, qui a écrit plus d’un million de lignes de Lean en trois semaines, comparativement aux deux millions et un tiers de lignes que neuf années de travail humain ont permis d’ajouter à Mathlib.La vérification devient bon marché. La question de savoir si elle deviendra la nôtre ou la leur est une tout autre question. De plus, une démonstration formelle peut être correcte tout en ne nous apprenant rien sur les raisons pour lesquelles elle est vraie. En plus de la vérification, nous avons besoin d’outils qui aident la lectrice ou le lecteur à comprendre une démonstration et pas seulement à la certifier, et les premiers pas dans cette direction existent déjà.Les blueprints de Patrick Massot transforment déjà une formalisation en un document lisible par des êtres humains, accompagné d’une carte générée automatiquement montrant comment ses différentes parties dépendent les unes des autres. Ils ont servi à des projets allant de l’expérience du tenseur liquide de Scholze aux travaux de Tao sur Freiman–Ruzsa. Son travail actuel vise à produire des documents dans lesquels la lectrice ou le lecteur choisit le niveau de détail qu’elle ou il souhaite voir, d’un résumé en une ligne jusqu’à l’argument complet.C’est une direction qu’une société devrait encourager : non seulement une IA qu’il faut surveiller, mais aussi des mathématiques interactives à construire.

La construction de cet avenir n’est qu’une des tâches de la Société. La Déclaration s’adresse aux organismes subventionnaires, aux revues, aux établissements et aux sociétés savantes, et pour une société nationale, ce ne sont pas des concepts abstraits. La SMC publie des revues, organise des réunions, décerne des prix, soutient un parcours de compétitions et s’adresse au gouvernement. C’est précisément l’endroit où un principe devient une pratique, ou échoue à le devenir. Signer une déclaration ne coûte rien. La mettre en œuvre demande du travail, et ce travail nous revient.

Prenons l’enseignement, qui constitue l’essentiel de notre travail et où la confusion est la plus grande.

La plupart des étudiantes et étudiants que nous enseignons ne deviendront jamais des mathématiciennes ou mathématiciens. Nous enseignons le calcul différentiel et intégral ainsi que l’algèbre linéaire à des ingénieures et ingénieurs, à des économistes et à des biologistes. Pendant des années, nous avons à moitié justifié ces cours en disant aux étudiantes et étudiants qu’un jour, ils devraient calculer eux-mêmes les intégrales. Cela n’a jamais été tout à fait vrai et c’est maintenant clairement faux : pour les intégrales courantes que nous donnons en exercice, les logiciels librement accessibles sont plus rapides que ne le seront jamais nos étudiantes et étudiants, et généralement plus fiables.Il reste la véritable raison, celle qui a toujours été la bonne. Une personne qui ne sait pas raisonner ne peut pas vérifier la machine, et une personne qui ne peut pas vérifier la machine est à sa merci. Le rôle des mathématiques au service d’autres disciplines ne s’est pas affaibli. Il a perdu sa justification, mais a conservé sa raison d’être, ce qui le rend plus important que jamais, et non moins important.

Former des mathématiciennes et mathématiciens est plus difficile, et c’est ici que j’ai moins confiance et davantage de préoccupations. La tentation est de répondre par une liste d’outils — apprendre à utiliser cet assistant de preuve, apprendre à rédiger cette invite — et de confondre la liste avec un plan. Les outils changent tous les quelques mois; la mathématicienne ou le mathématicien que nous cherchons à former prend des années à se développer.Ce qu’il faut protéger, c’est précisément ce que les outils menacent le plus : la lutte longue, pénible et solitaire avec un problème qui refuse de céder. La maturité mathématique ne s’acquiert pas dans les cours magistraux. Elle se construit précisément pendant ces heures-là, et une étudiante ou un étudiant qui les confie à une machine a acheté une bonne note et vendu sa formation.

La résolution de problèmes mérite ici qu’on lui consacre une attention particulière, car elle constitue le terrain d’entraînement de tout cela. Les cours magistraux transmettent des définitions et des théorèmes; seuls les problèmes enseignent aux étudiantes et étudiants comment commencer lorsqu’aucune personne ne leur a montré quoi faire. Ici, mon parcours entre en jeu : je viens de la tradition russe des cercles mathématiques et des olympiades, où la résolution de problèmes n’était pas une préparation aux mathématiques, mais leur première forme, et j’ai vu ce que cette tradition permet de produire.La distinction utile est celle entre un exercice et un problème. Un exercice demande aux étudiantes et étudiants de répéter ce qu’on leur a montré, et les machines font maintenant les exercices instantanément. Cela change leur rôle, mais pas leur valeur : faits honnêtement, les exercices permettent toujours de développer la maîtrise des techniques, comme les gammes pour une musicienne ou un musicien, mais ils ne peuvent plus à eux seuls constituer la formation mathématique, et un exercice remis ne nous permet plus de savoir si l’étudiante ou l’étudiant aurait pu le faire sans aide.Un problème ne leur donne rien d’autre que la question, et le travail nécessaire pour le résoudre développe le jugement, le goût et l’endurance qu’aucune autre activité ne permet de développer. Si nous pensons vraiment ce que nous disons sur l’importance de préserver cette lutte, alors les séminaires et les cercles de résolution de problèmes doivent être au cœur de nos programmes, et non en marge de ceux-ci.

Il y a aussi la question plus difficile de les garder engagées et engagés. On peut comprendre que des étudiantes et étudiants qui voient une machine résoudre en quelques secondes un problème qui leur a demandé une semaine se demandent pourquoi ils devraient se donner la peine d’essayer. Nous leur devons une réponse honnête, et nous en avons une : la récompense des mathématiques n’a jamais été que personne d’autre ne puisse résoudre le problème; c’est la compréhension, et la compréhension n’est pas quelque chose qu’une machine peut avoir à notre place.Notre tâche est de permettre aux étudiantes et étudiants de ressentir cette différence tôt, avant que le découragement ne se transforme en abandon — et pas seulement aux étudiantes et étudiants de premier cycle, car la doctorante ou le doctorant qui se demande à quoi sert une thèse mérite la même réponse. La motivation n’est pas une préoccupation secondaire; sans elle, rien de ce que nous prévoyons n’aura d’importance.

Il y a aussi la question de l’étalonnage, qui est véritablement nouvelle. Les étudiantes et étudiants qui ne touchent jamais à ces systèmes seront bientôt démunis; celles et ceux qui y ont recours au premier signe de difficulté risquent de ne jamais rien construire par eux-mêmes. Ce que nous devons leur apprendre, c’est le bon moment : commencer par chercher par soi-même, puis consulter la machine; l’utiliser pour vérifier et explorer, et non pour réfléchir à notre place; reconnaître le moment où elle cesse de nous aider à réfléchir et commence à réfléchir à notre place.Ils devraient également savoir que ces systèmes sont conçus pour être accommodants. Lorsque Tao a publié le compte rendu de sa propre session avec un modèle alors qu’il travaillait sur l’exemple de la conjecture jacobienne, les lectrices et lecteurs ont été frappés par la constance avec laquelle le modèle lui assurait qu’il avait raison. Un outil qui approuve chaque étape peut nuire davantage au jugement d’une étudiante ou d’un étudiant qu’un outil qui se trompe parfois : une erreur incite à vérifier, tandis qu’un accord passe inaperçu, parce que c’est ce que nous souhaitions entendre.La surutilisation ne produit pas une mathématicienne ou un mathématicien moins compétent. Elle n’en produit aucun. La Déclaration affirme que l’objectif des mathématiques est la compréhension humaine, et en classe, ce n’est pas un slogan : c’est la lutte que nous devons refuser d’automatiser, même si nous enseignons aux étudiantes et étudiants à utiliser l’outil une fois qu’ils ont accompli le travail qui fait de celui-ci un outil plutôt qu’un substitut. Ces deux exigences sont contradictoires, et je ne vois pas de manière simple de les satisfaire toutes les deux. La Société ne résoudra pas cette tension. Elle peut au moins nous obliger à rester honnêtes à son sujet.

La SMC peut agir dès maintenant sur certains de ces points. L’étape la plus importante est aussi la plus simple et celle qui dépend le plus entièrement de nous : exiger, dans le Canadian Journal of Mathematics et les autres revues de la Société, une courte déclaration précisant quels outils d’IA une autrice ou un auteur a utilisés et à quelles fins. La divulgation devrait être proportionnée — c’est l’utilisation substantielle dans la découverte, la démonstration, les calculs ou la rédaction qui importe, et non la correction orthographique — et la politique devrait énoncer ce que la Déclaration tient pour acquis : un système ne peut pas être autrice ou auteur, et la responsabilité d’un article incombe aux êtres humains qui le signent. Cela ne nous coûte rien et permet d’appliquer directement la Déclaration.Ensuite, et c’est plus urgent qu’il n’y paraît, nous devrions fournir aux évaluatrices et évaluateurs des lignes directrices écrites sur les deux aspects d’un même problème : ne pas téléverser les manuscrits en cours d’évaluation vers des services d’IA externes, ce qui représente un risque pour la confidentialité auquel les revues sont déjà confrontées; et veiller à ce que le jugement mathématique exprimé dans un rapport soit le leur — obtenir de l’aide pour la langue est une chose, déléguer l’évaluation en est une autre.Nous devrions faire de la possibilité de vérifier un résultat publié sans accès à des systèmes propriétaires une politique éditoriale. Et la Société devrait entamer une conversation à laquelle elle s’est jusqu’ici contentée d’assister : que devraient signifier le consentement et l’attribution lorsque nos revues et nos archives deviennent des données d’entraînement pour des systèmes propriétaires?

Dans l’enseignement, notre influence est uniquement consultative, puisque les programmes d’études relèvent des départements, mais nulle part les enjeux ne sont plus importants, et la solution n’est pas la même dans toutes les salles de classe. Dans les cours fondés sur les démonstrations, nous pouvons ramener l’essentiel du travail en classe : examens oraux, démonstrations au tableau, étudiantes et étudiants qui défendent leurs propres solutions. Dans les grands cours de service, cela ne peut pas être mis en œuvre à cette échelle. J’ai enseigné le calcul différentiel et intégral à huit cents étudiantes et étudiants, et je ne vais pas faire passer un examen oral à huit cents personnes; dans ce cas, la réponse honnête consiste à faire des évaluations surveillées en classe, ou à admettre franchement que nous n’avons pas encore trouvé de solution simple.Un devoir fait à la maison est désormais un test de l’abonnement de l’étudiante ou de l’étudiant, et non de l’étudiante ou de l’étudiant elle-même ou lui-même — ce n’est plus une preuve de travail effectué sans aide — et prétendre le contraire ne fait qu’enseigner aux étudiantes et étudiants que nous ne prêtons pas attention. Les mathématiques de compétition, notamment le parcours des olympiades que la Société soutient déjà, développent précisément le type de raisonnement qui a pris de la valeur, et devraient être financées en conséquence.

La représentation auprès des décideuses et décideurs est la plus lente de ces démarches, et ici, je veux adopter une perspective canadienne. Il est facile d’écrire que le danger réside dans notre dépendance à trois ou quatre entreprises américaines, et ce n’est pas sans fondement. Mais le Canada a ses propres entreprises et institutions : Cohere est canadienne, et Mila, l’Institut Vecteur et CIFAR sont en grande partie la raison pour laquelle ce pays compte dans ce domaine. Nous ne sommes pas de simples spectatrices et spectateurs de cette technologie, et nous avons une certaine influence sur son orientation; notre problème le plus criant n’est pas une menace étrangère, mais l’exode silencieux de nos meilleures étudiantes et de nos meilleurs étudiants vers des laboratoires qui offrent des salaires plusieurs fois supérieurs à celui d’une professeure ou d’un professeur.La Société devrait faire pression sur le CRSNG et le gouvernement sur les deux fronts à la fois : continuer à financer la formation de mathématiciennes et mathématiciens, et maintenir ouvertes et vérifiables les infrastructures de recherche, afin que l’orientation de la discipline demeure entre les mains de la communauté mathématique plutôt que de dériver vers ceux qui possèdent les machines les plus puissantes.Un dernier point, qui n’est qu’en apparence secondaire : quelles que soient les politiques adoptées par la Société, elles doivent exister dans les deux langues officielles, et nous devrions constater que les modèles eux-mêmes ne sont pas aussi performants dans les deux langues. Si ces outils deviennent partie intégrante de la façon dont les mathématiques sont apprises et pratiquées, un écart entre leurs capacités en français et en anglais constitue un écart d’accès pour nos étudiantes et étudiants et nos départements francophones, et il devrait figurer sur la même liste d’inégalités que celle que la Société surveille déjà.

Dans l’esprit de la Déclaration que je viens d’approuver, je dois faire une divulgation : j’ai utilisé un système d’IA pour critiquer et réviser les brouillons de cette note; son argumentation et ses conclusions sont les miennes.

Je n’ai aucune illusion quant à la durée de vie de ces pages. Étant donné la rapidité des changements au cours des deux dernières années, les détails pourraient être dépassés deux mois après leur impression, et l’ensemble de cette note pourrait sembler naïf dans quelques années. Mais les détails — les outils, les entreprises, les solutions — allaient de toute façon devenir obsolètes. Les principes, eux, ne le seront pas : divulguer ce que la machine a fait, faire en sorte que les démonstrations puissent être vérifiées par n’importe qui et protéger la compréhension humaine qui est au cœur de toute cette entreprise. C’est ce que je demande à la Société d’adopter dès maintenant, ainsi qu’une date pour revoir le reste. Et lorsque cette révision aura lieu et que ces pages sembleront désuètes, cela aussi sera de mon fait.