Preuves écrites par l'IA : OpenAI et Anthropic paient pour que les mathématiciens les vérifient

Cent soixante-six pages, rédigées par une machine. Le 8 septembre, OpenAI affirmait qu'un de ses modèles internes avait démontré que les équations de Navier-Stokes, qui décrivent l'écoulement des fluides, peuvent « exploser » : dans certains cas rares, la vitesse du fluide deviendrait infinie en un point. C'est l'un des sept problèmes du millénaire du Clay Mathematics Institute, dotés chacun d'un million de dollars. Cinq semaines plus tard, la question n'est plus seulement de savoir si la preuve est juste. Il s'agit aussi de savoir qui va la vérifier, et avec quels moyens.

Une première réponse est arrivée le 15 octobre. La Simons Foundation, grand mécène américain des mathématiques, lance avec OpenAI et Anthropic un programme de 15 millions de dollars en financements et en ressources. Objectif : aider les chercheurs à examiner les résultats obtenus avec l'IA, à apprendre ces nouveaux outils et à fixer des règles communes pour leur usage.

Qui paie, et qui décide ?

La fondation gérera l'argent et choisira elle-même les bénéficiaires, en partie par un appel à projets dont le calendrier n'est pas encore publié. Le programme financera des ateliers, des conférences et des programmes spécifiques. Les deux entreprises fourniront aussi un accès à leurs modèles et à leur puissance de calcul aux chercheurs soutenus, en mathématiques comme en sciences fondamentales. OpenAI a annoncé une contribution de 5 millions de dollars ; la fondation ne détaille pas la répartition du reste.

« La communauté doit piloter les discussions sur la manière dont ces outils sont évalués, adoptés et utilisés », insiste David Spergel, président de la fondation. Une précision utile : la Simons Foundation a financé le développement de Lean, le langage de preuve formelle qui permet aujourd'hui de vérifier mécaniquement les démonstrations produites par une IA.

Une preuve contestée

Le communiqué ne mentionne pas Navier-Stokes. Euronews, en revanche, présente le don d'OpenAI comme une tentative de calmer la colère des mathématiciens. Car la démonstration a déclenché une querelle de paternité. Le mathématicien Tristan Buckmaster (université de New York) affirme qu'OpenAI s'est appuyé sur des travaux non publiés qu'il menait avec Levent Alpöge, chercheur chez Anthropic qui y collaborait à titre personnel. OpenAI dément : selon Sébastien Bubeck, mathématicien de l'entreprise, son équipe n'a utilisé ni leurs consignes ni leurs preuves.

Une association, l'Association for Human Mathematics, accuse OpenAI de plagiat et d'un « mépris total des normes de la recherche scientifique », selon Euronews. D'autres chercheurs sont plus nuancés. Gonzalo Cao-Labora, de l'EPFL, juge les deux approches différentes dans le détail, rapporte The Decoder. Pour Camillo De Lellis, de l'Institute for Advanced Study, une réponse définitive est probablement impossible, car les modèles de langage sont des boîtes noires.

Vérifiée par la machine, pas encore par les humains

La preuve est écrite en Lean, qui contrôle chaque étape logique, ce qui, selon OpenAI cité par Scientific American, garantit presque sa justesse. Mais un texte Lean ne se lit pas comme un article de mathématiques. Le Clay Mathematics Institute l'examine depuis sa publication, sans conclusion annoncée, selon The Decoder. Le même site indique que l'opération a mobilisé environ 10 000 instances du modèle pendant environ 88 heures, et que Noam Brown, chercheur chez OpenAI, reconnaît que personne ne sait ce que chacune a apporté. Début octobre, OpenAI a en outre publié environ 400 autres résultats produits par l'IA, accueillis avec scepticisme par une partie des mathématiciens.

Le programme Simons pose donc une question simple : les mathématiciens auront-ils les moyens de suivre le rythme des machines ? Le verdict du Clay Institute sera le premier vrai test.