L’IA, nouvelle alliée des mathématiciens ?

Les pro­grès récents du rai­son­ne­ment auto­ma­tique placent l’intelligence arti­fi­cielle au cœur de nou­velles inves­ti­ga­tions en mathé­ma­tiques. Des sys­tèmes comme Goe­del-Pro­ver, conçus pour géné­rer et vali­der des preuves for­melles, ont mon­tré en 2025 une pro­gres­sion notable en attei­gnant des niveaux de per­for­mance éle­vés sur des jeux de tests spé­cia­li­sés¹. Dans le même temps, APOLLO a mis en avant la capa­ci­té d’un modèle à col­la­bo­rer avec l’assistant de preuve Lean pour pro­duire des démons­tra­tions véri­fiables, tout en révi­sant auto­ma­ti­que­ment cer­taines étapes erro­nées².

Les enjeux liés à ces avan­cées ont été exa­mi­nés lors de la confé­rence IA et Mathé­ma­tiques orga­ni­sée en avril 2025 par Hi ! PARIS, qui a mis en avant le rôle crois­sant de la véri­fi­ca­tion for­melle dans les recherches actuelles³. Ces tra­vaux rejoignent cer­taines ana­lyses publiées dans la presse scien­ti­fique. Le Monde a sou­li­gné en 2024 le poten­tiel de ces outils pour accé­lé­rer la pro­duc­tion de résul­tats, en évo­quant un recours impor­tant aux modèles pour son­der des pistes dif­fi­ciles d’accès par les approches tra­di­tion­nelles⁴. De son côté, Science & Vie a rap­por­té en 2025 que cer­tains sys­tèmes avaient obte­nu des scores éle­vés à des com­pé­ti­tions de type olym­piade, ce qui témoigne de leur capa­ci­té à trai­ter des pro­blèmes struc­tu­rés⁵, même si ces scé­na­rios ne reflètent que par­tiel­le­ment les exi­gences de la recherche mathématique.

Pour cir­cons­crire ces dyna­miques tout en démê­lant le vrai du faux, Amau­ry Hayat, pro­fes­seur à l’École des Ponts Paris­Tech (Ins­ti­tut Poly­tech­nique de Paris), cher­cheur en mathé­ma­tiques appli­quées et en intel­li­gence arti­fi­cielle, livre son exper­tise. Il dirige le pro­jet DESCARTES, consa­cré aux méthodes d’apprentissage dans des contextes de don­nées rares, ain­si qu’à plu­sieurs tra­vaux por­tant sur l’apprentissage par ren­for­ce­ment appli­qué à la démons­tra­tion auto­ma­tique. Ses ana­lyses per­mettent d’examiner les évo­lu­tions actuelles du rai­son­ne­ment auto­ma­ti­sé en mathé­ma­tiques en s’appuyant sur des don­nées, des outils et des résul­tats publiés.

Amau­ry Hayat. L’intelligence arti­fi­cielle, notam­ment les modèles capables de rai­son­ner en lan­gage natu­rel ou for­mel, peut déjà pro­duire des preuves au niveau d’un étu­diant en thèse de pre­mière année dans cer­tains cas. Il existe des situa­tions simples qu’elle ne sait pas encore trai­ter, mais aus­si des pro­blèmes com­plexes qu’elle peut résoudre.

Nous ne dis­po­sons pas encore de sys­tèmes capables de géné­rer, du début à la fin, des preuves sur­pas­sant le niveau des mathé­ma­ti­ciens humains. Cepen­dant, les IA peuvent déjà four­nir des preuves très inté­res­santes et, par­fois, résoudre des pro­blèmes res­tés ouverts depuis long­temps. Dans ces cas, elles exploitent sou­vent des frag­ments de solu­tions épar­pillés dans dif­fé­rents articles ou domaines, que l’IA par­vient à com­bi­ner effi­ca­ce­ment grâce à sa capa­ci­té à accé­der et orga­ni­ser la connais­sance dis­po­nible sur Inter­net. Par exemple (figure 1), GoedelProver‑v2, un modèle for­mel, a été entraî­né sur 1,64 mil­lion d’énoncés for­ma­li­sés et atteint, en 2025, une pré­ci­sion de 88,1 % sans self‑correction et de 90,4 % avec self‑correction sur le bench­mark MiniF2F⁶.

Les prin­ci­paux obs­tacles sont davan­tage liés aux méthodes de l’IA qu’aux mathé­ma­tiques elles-mêmes. Dans des domaines de recherche très spé­cia­li­sés, les don­nées sont extrê­me­ment limi­tées. Or, avec les méthodes actuelles d’entraînement des IA, cette rare­té consti­tue un frein impor­tant. L’apprentissage par ren­for­ce­ment peut théo­ri­que­ment pal­lier ce pro­blème, mais il exige tout de même un nombre signi­fi­ca­tif d’exemples pour être effi­cace, et il est sur­tout per­ti­nent lorsque la véri­fi­ca­tion auto­ma­tique est possible.

Aujourd’hui, cette véri­fi­ca­tion peut se faire soit en lan­gage natu­rel, ce qui limite les types de pro­blèmes abor­dables, soit en lan­gage for­mel, où un ordi­na­teur peut confir­mer direc­te­ment si une preuve est cor­recte. Le défi est que les IA actuelles qui s’expriment en lan­gage for­mel ne sont pas encore au niveau des IA qui s’expriment en lan­gage naturel.

Deux axes sont explo­rés pour pro­gres­ser : aug­men­ter la quan­ti­té de don­nées en tra­dui­sant auto­ma­ti­que­ment du lan­gage natu­rel vers le lan­gage for­mel et amé­lio­rer les méthodes d’apprentissage par ren­for­ce­ment. Cette approche per­met de com­bi­ner la puis­sance des modèles en lan­gage natu­rel avec la rigueur des véri­fi­ca­tions for­melles, en four­nis­sant un feed­back auto­ma­tique pour l’entraînement par essais et erreurs.

Godel-Pro­ver est inté­res­sant, car il a rapi­de­ment atteint les per­for­mances de notre modèle sur le data­set Put­nam­Bench, ini­tia­le­ment obte­nu avec un nombre très limi­té d’exemples. Les ver­sions ulté­rieures, ain­si que Deep­Seek-Pro­ver, sont extrê­me­ment per­for­mantes, notam­ment pour des exer­cices de type olympiade.

Notre objec­tif avec DESCARTES est dif­fé­rent : nous visons des pro­blèmes de niveau recherche, carac­té­ri­sés par un régime de faibles don­nées. L’enjeu est donc de déve­lop­per des modèles capables de tra­vailler dans ces condi­tions, contrai­re­ment aux méthodes clas­siques qui exploitent de très grandes quan­ti­tés d’exemples.

Pour la majo­ri­té des pro­blèmes que je teste, même les meilleurs modèles ne four­nissent pas de solu­tion com­plète. Cepen­dant, il arrive que l’IA four­nisse des réponses inté­res­santes, et ce, assez régu­liè­re­ment. Même si ce n’est pas aus­si fiable que de consul­ter un col­lègue expert, l’avantage est qu’on obtient une inter­face unique capable de trai­ter plu­sieurs domaines simul­ta­né­ment, ce qui fait gagner beau­coup de temps. Par­fois, cela équi­vaut presque à avoir un col­lègue très expé­ri­men­té à dis­po­si­tion pour éva­luer ce qui est fai­sable. Par exemple, Gauss de Math_inc a for­ma­li­sé le Théo­rème des Nombres Pre­miers fort (PNT) en Lean, pro­dui­sant envi­ron 25 000 lignes de code et plus de 1 000 théo­rèmes et défi­ni­tions⁷, tan­dis que Pro­ver Agent uti­lise une boucle de feed­back pour géné­rer des lemmes auxi­liaires et com­plé­ter des preuves⁸. Ces modèles per­mettent de réduire consi­dé­ra­ble­ment le temps consa­cré à l’exploration et à la véri­fi­ca­tion, tout en ren­for­çant la rigueur des résultats.

Pour le pro­jet DESCARTES, nous tra­vaillons direc­te­ment en lan­gage for­mel, ce qui per­met à l’ordinateur de véri­fier la cor­rec­tion des preuves. En revanche, lorsque j’utilise des LLM clas­siques pour des articles mathé­ma­tiques hors de ce pro­jet, je dois lire et véri­fier manuel­le­ment les preuves. Cela fait gagner beau­coup de temps, mais il sub­siste un risque : les erreurs pro­duites par les modèles sont par­fois sur­pre­nantes, inat­ten­dues, et ne cor­res­pondent pas à celles qu’un humain ferait. Elles peuvent par­fois paraître très cré­dibles tout en étant fausses, ce qui néces­site une vigi­lance particulière.

Il faut dis­tin­guer deux niveaux dans l’enseignement des mathé­ma­tiques : la for­ma­tion jusqu’au niveau mas­ter et la recherche post-mas­ter. Pour l’apprentissage des bases et la com­pré­hen­sion des preuves, la capa­ci­té d’une IA à démon­trer des théo­rèmes ne remet pas fon­da­men­ta­le­ment en ques­tion l’enseignement clas­sique. L’entraînement humain à repro­duire des preuves reste essen­tiel pour déve­lop­per le raisonnement.

En revanche, dans le cadre de pro­jets de recherche ou d’examens où les étu­diants dis­posent de toutes les res­sources, l’IA peut jouer un rôle d’assistant per­son­nel. Par exemple, dans un pro­jet de mas­ter, elle pour­rait aider à pro­duire des preuves sur des pro­blèmes ouverts, ce qui enri­chi­rait l’expérience d’apprentissage et la créa­ti­vi­té des étudiants.

À court terme, les cher­cheurs uti­li­se­ront des pla­te­formes comme ChatGPT, Gemi­ni ou Mis­tral pour géné­rer et véri­fier des preuves rapi­de­ment, gagnant ain­si un temps consi­dé­rable. Des outils spé­cia­li­sés com­mencent éga­le­ment à émer­ger, comme Google Labs pour explo­rer Google Scho­lar ou Alpha Evolve pour la construc­tion de struc­tures mathé­ma­tiques, tan­dis que Gemini‑3, Deep Think et GPT-5-pro (modèles de lan­gage) génèrent d’abord une ébauche, puis uti­lisent, selon les indi­ca­tions dis­po­nibles, des outils de véri­fi­ca­tion pour iden­ti­fier cer­taines erreurs éventuelles.

À moyen ou long terme, des sys­tèmes pour­raient com­bi­ner géné­ra­tion auto­ma­tique et véri­fi­ca­tion for­melle, accé­lé­rant la recherche et influen­çant les modes de publi­ca­tion et les attentes aca­dé­miques. Les modèles actuels sont déjà capables de pro­duire des articles presque com­plets sur la base de publi­ca­tions pré­cé­dentes, ce qui pour­rait trans­for­mer la pro­duc­tion d’articles “incré­men­taux” et libé­rer du temps pour des recherches plus ambi­tieuses. Par exemple, des tests com­pa­ra­tifs montrent que sur le bench­mark miniF2F, APOLLO atteint 75 % de suc­cès pour les preuves géné­rées auto­ma­ti­que­ment, alors que Goe­del-Pro­ver atteint 57,6 %⁹. Tou­te­fois, cer­tains modèles peuvent pro­duire des erreurs concep­tuelles sub­tiles ou des pas­sages répé­ti­tifs, ren­dant la super­vi­sion humaine indis­pen­sable pour vali­der la fia­bi­li­té scientifique.

Il fau­dra cer­tai­ne­ment repen­ser cer­tains aspects de la car­rière des cher­cheurs, notam­ment le sys­tème de publi­ca­tion, la relec­ture par les pairs et l’écriture des articles. Les modèles sont aujourd’hui capables de pro­duire des preuves et des articles de qua­li­té, et cela pour­rait modi­fier la nature et la fré­quence des publi­ca­tions scientifiques.

Propos recueillis par Aicha Fall