Conjectures par LLM vs vérification de preuves

Entre le deuxième et le troisième café, beaucoup de spécialistes de la complexité ont récemment lu une phrase qu'ils ne pensaient jamais lire : un algorithme déterministe qui compte les affectations satisfaisantes d'une formule booléenne quelconque en temps environ 2^(n/√(log n)) — sous-exponentiel, au sens technique précis qui réfute l'Exponential Time Hypothesis, l'une des hypothèses porteuses du domaine. L'annonce n'est pas sortie sur arXiv d'un groupe universitaire. Elle vient d'un laboratoire d'IA, avec une preuve développée en collaboration avec un grand modèle de langage. Quoi qu'on pense de l'annonce, elle marque le moment où la génération de conjectures — des machines qui proposent de nouvelles mathématiques au lieu de simplement les corriger — a quitté le stade de la démo.

Le laboratoire a regroupé trois résultats : la bombe en théorie de la complexité évoquée plus haut, une preuve revendiquée de la conjecture de Kakeya en toutes dimensions, et un résultat de physique présenté comme une complétion unifiée du Modèle standard, gardé au secret en attendant une vérification formelle. La réaction a suivi un schéma familier : une vraie stupéfaction devant le fond, une vraie agacement devant l'emballage. Des critiques ont comparé cela à un fabricant de vélos qui annoncerait ses propres victoires en course cycliste. Bien vu — et pourtant le fond mérite un regard plus lent, car cette annonce cache une vraie leçon sur les deux façons très différentes dont les modèles de langage touchent aujourd'hui les mathématiques, et sur celle à laquelle vous devriez réellement faire confiance.

Ce que l'annonce mathématique de l'IA revendique réellement

Commençons par le résultat en complexité, car ce sont les enjeux les plus clairs. L'Exponential Time Hypothesis affirme, en gros, que 3-SAT ne peut pas être résolu en temps 2^o(n) — aucun algorithme ne peut être significativement sous-exponentiel en nombre de variables. Des centaines d'articles en complexité paramétrée et à grain fin s'appuient sur l'ETH pour prouver des bornes inférieures ; c'est le genre d'hypothèse sur laquelle on empile une carrière entière de théorèmes « sous réserve de l'ETH ». La nouvelle prépublication décrit un algorithme de comptage déterministe pour les formules k-CNF qui utilise un espace polynomial et tourne en temps 2^(n/(log n)^(1/2+o(1))) multiplié par un facteur polynomial. Cet exposant est o(n), ce qui est exactement ce que l'ETH interdit. L'algorithme reste d'une lenteur brutale — personne ne le fera tourner sur une instance réelle — mais asymptotiquement, c'est décisif. Si la preuve tient, une hypothèse qui a structuré deux décennies d'arguments de bornes inférieures cesse tout simplement d'exister.

La deuxième affirmation vise la conjecture de Kakeya, un problème de théorie géométrique de la mesure sur les plus petits ensembles contenant un segment unitaire orienté dans toutes les directions. Le cas tridimensionnel n'est tombé qu'en 2025, avec une preuve célébrée de Hong Wang et Joshua Zahl que beaucoup ont considérée comme l'aboutissement d'une carrière. L'annonce revendique une preuve en toutes dimensions, ce qui absorberait entièrement cette percée. Le troisième résultat, en théorie quantique des champs, est le plus flou des trois : présenté comme une « complétion unifiée du Modèle standard » mais pas encore publié, apparemment en attente d'une formalisation vérifiée par machine. Les physiciens qui ont lu les teasers soupçonnent une construction de la famille des théories grand-unifiées plutôt qu'une véritable théorie de tout, et la formulation mérite à juste titre quelques regards sceptiques.

Deux aspects du lancement méritent d'être salués. Le laboratoire a impliqué des mathématiciens et des physiciens en activité avant de rendre l'annonce publique — une réponse directe à la polémique qui a suivi une annonce mathématique précédente, plus maladroite, après laquelle Terence Tao et d'autres ont réclamé publiquement ce type de collaboration. Et le résultat de physique a été retenu jusqu'à la fin de sa formalisation, ce qui est le bon ordre des priorités. Mais des questions restent sans réponse : personne à l'extérieur ne connaît la facture de calcul, ni si un financement équivalent confié à des chercheurs humains aurait produit les mêmes théorèmes, ni si un laboratoire à but lucratif continuera à financer des travaux guidés par la curiosité le jour où ses actionnaires voteront. Il y a aussi la boucle inconfortable que les critiques ont relevée immédiatement : ces modèles sont en partie entraînés sur les questions, brouillons et messages de forum de cette même communauté de recherche qu'on invite maintenant à applaudir le résultat.

Vérification de preuves contre génération de conjectures : deux métiers différents

Une fois le battage médiatique écarté, tout système d'IA pour les mathématiques remplit l'un de deux rôles. Le premier est la vérification de preuves : étant donné un argument candidat, décider s'il est valide. Le second est la génération de conjectures : étant donné un domaine de problèmes, proposer ce qui vaut la peine d'être tenté — un lemme, une construction, un algorithme, un contre-exemple. Ils ressemblent à deux moitiés d'une même compétence. Ce n'est pas le cas. Ce sont des problèmes de calcul différents, avec des oracles différents, des modes de défaillance différents et des profils de confiance radicalement distincts, et les confondre mène soit à surestimer un communiqué de presse, soit à rejeter de vrais progrès.

La vérification dispose d'un oracle. Une preuve écrite en Lean se compile ou non face au noyau, et le noyau se moque de l'assurance avec laquelle l'auteur s'exprime. La vérification échoue bruyamment — un bloc de tactiques rejeté ne laisse aucune ambiguïté. La génération n'a pas d'oracle. Une conjecture proposée peut être vraie, fausse, trivialement vraie, ou vraie mais publiée en 1987 sous une autre notation. La génération échoue discrètement, et ses modes de défaillance sont sociaux : des absurdités plausibles, ou de véritables résultats déguisés en nouveauté. La qualité se mesure ici par l'importance et l'originalité, des propriétés définies par le goût humain plutôt que par un critère décidable.

Pourquoi la génération est-elle soudainement devenue assez bonne pour compter ? Parce que les modèles de raisonnement modernes sont entraînés à produire de longues chaînes de pensée, et non simplement incités à le faire — l'apprentissage par renforcement sur des récompenses vérifiables, surtout en mathématiques et en code où les réponses se vérifient mécaniquement, a appris à ces systèmes à explorer réellement un espace d'étapes plutôt qu'à compléter un texte pas à pas. Voici l'analogie que je garderais en tête : le vérificateur de preuves est un compilateur, le générateur de conjectures est un designer. Les deux sont précieux. Vous ne laisseriez jamais, au grand jamais, le designer certifier son propre travail.

Une preuve que vous ne pouvez pas vérifier est un sermon ; une conjecture que vous ne pouvez pas tester est une rumeur.

Là où la vérification automatique de preuves gagne

Le vérificateur l'emporte partout où existe une vérité de référence formelle et où l'artefact examiné est trop long ou trop fastidieux pour être audité ligne par ligne par un humain. Lean 4 et sa bibliothèque communautaire Mathlib sont devenus l'arène de référence : vous écrivez définitions et preuves dans un langage de programmation, et un petit noyau, auditable séparément, décide si chaque étape d'inférence est légale. La base de confiance est minuscule par rapport à la montagne de mathématiques bâtie dessus, et c'est exactement l'asymétrie qu'on veut.

La boucle pratique ressemble à ceci : le modèle rédige des étapes de preuve au niveau des tactiques, le noyau accepte ou rejette chacune, et les messages de rejet sont réinjectés comme contexte pour la tentative suivante. C'est le seul cadre où contraindre la sortie du modèle à une grammaire stricte rapporte immédiatement : vous n'échantillonnez que des tactiques syntaxiquement valides, donc des classes entières d'hallucinations deviennent impossibles par construction. Un exemple minimal, le genre de lemme qu'un modèle traite aujourd'hui en quelques secondes :

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

Remarquez ce que l'exemple montre de la répartition des tâches. Le geste créatif consiste à choisir le témoin k + l ; le geste de vérification consiste pour ring à vérifier l'algèbre. Humains et modèles sont tous deux assez bons pour le premier. Seul le noyau est digne de confiance pour le second, et il ne se fatigue jamais, ne survole jamais, et ne note jamais à l'intuition. L'élément le plus crédible de toute l'annonce est précisément ce filtre : l'affirmation selon laquelle l'article de physique a été retenu jusqu'à la fin de sa formalisation dans Lean. Si ce récit est exact, c'est le flux de travail qui fonctionne exactement comme prévu — la machine propose, la machine dispose, et le communiqué de presse attend son tour.

Là où la génération de conjectures gagne

La génération gagne partout où l'espace de recherche est combinatoire et où l'évaluation est peu coûteuse. FunSearch de DeepMind a posé le modèle dès 2023 : un modèle de langage propose des hypothèses sous forme de programmes, un évaluateur rapide les note, et une boucle évolutionnaire garde les meilleures — un dispositif qui a produit de nouvelles constructions pour les cap sets et de meilleures heuristiques de bin packing que des décennies de réglages manuels. AlphaEvolve a poussé la même idée plus loin et, parmi d'autres résultats, a réduit d'une multiplication un algorithme de multiplication de matrices 4×4 qui tenait depuis l'époque de Strassen. Personne ne prétend que ces systèmes comprennent la géométrie. Ils n'en ont pas besoin. Ils doivent proposer, et l'évaluateur doit être honnête.

L'algorithme de l'ETH s'inscrit presque suspectueusement bien dans ce schéma. L'espace des « idées algorithmiques » est immense, et les chercheurs humains l'explorent avec de forts a priori — ce qui est une façon polie de dire des angles morts. Une construction qui exige de composer une astuce de représentation précise avec une structure de récursion précise peut rester inexplorée pendant trente ans simplement parce que le chemin de recherche de personne n'est jamais passé à proximité. Une recherche exhaustive, sans a priori et un peu bête, c'est exactement ce que les machines apportent. La même logique alimente les boucles de génération-puis-réfutation : proposer une conjecture, la tester aussitôt pour la faire tomber par une recherche informatique de contre-exemples sur de petits cas. La plupart des conjectures meurent en quelques minutes, et c'est très bien — chaque réfutation affine la proposition suivante, et les survivantes sont celles qui valent l'après-midi d'un humain.

Il y a aussi une asymétrie psychologique qu'il faut respecter. La preuve tridimensionnelle de Kakeya par Wang et Zahl a demandé des années d'efforts concentrés au sommet du domaine. Si une recherche assistée par modèle a réellement produit un argument valable en toutes dimensions, elle a presque certainement trouvé un chemin différent dans le paysage — pas forcément plus profond, mais différent. La différence est précisément l'objet de la recherche. Le danger n'est pas que les machines génèrent des conjectures ; c'est que quelqu'un publie une conjecture générée sans l'outillage qui la soutient. Ce qui nous amène à la partie du pipeline qu'il vous faut réellement construire.

Construire une boucle de vérification pour les preuves générées par l'IA

Si vous voulez les bénéfices des mathématiques générées par machine sans la gêne, le flux de travail compte davantage que le modèle. Voici le pipeline que je ferais tourner, dans l'ordre :

1. Générer largement et à moindre coût. À ce stade, la diversité l'emporte sur la profondeur ; vous voulez couvrir l'espace des idées, pas une tentative soignée unique.
2. Dédoublonner par rapport à la littérature. La recherche dans arXiv et MathOverflow évite le piège le plus courant : une « nouvelle » conjecture qui n'est qu'un résultat connu sous une notation inhabituelle.
3. Appliquer des filtres empiriques bon marché. Tester numériquement de petits cas, chasser les contre-exemples par le calcul, et laisser mourir vite les énoncés manifestement faux.
4. Formaliser les survivantes. Lean, Isabelle ou Rocq — choisissez votre assistant de preuve, mais sachez que c'est l'étape coûteuse, et qu'une preuve en langage naturel n'est qu'une esquisse, pas un résultat.
5. Relecture humaine pour la nouveauté et le cadrage. Est-ce important ? L'énoncé est-il le bon ? Les modèles optimisent ce qui est prouvable ; les humains décident ce qui vaut la peine d'être prouvé.

La collaboration annoncée a à peu près suivi cette structure — des chercheurs ont été associés avant la publication, ce qui revient à occuper de fait l'étape cinq. C'est une vraie amélioration par rapport à l'ancienne méthode consistant à déposer une prépublication et laisser les réseaux sociaux l'arbitrer. Mais remarquez l'asymétrie du pipeline : les étapes un à trois sont bon marché et évoluent avec le calcul, l'étape quatre est le goulot d'étranglement, et l'étape cinq ne passe pas à l'échelle du tout. Si vous construisez des outils dans ce domaine, investissez dans le goulot — une meilleure autoformalisation, un meilleur retour d'erreurs vers le générateur — plutôt que dans un générateur plus gros et plus sûr de lui.

Pourquoi les mathématiciens humains gardent encore le contrôle de la correction

Aucun vérificateur ne peut vous dire qu'un théorème compte. Le choix des problèmes relève du goût, et le goût est une technologie sociale bâtie sur des décennies — séminaires, rapports d'arbitrage, consensus lent sur les questions qui ouvrent des portes et celles qui sont des impasses. Le scepticisme de la communauté de recherche envers les annonces des éditeurs n'est pas un simple corporatisme ; c'est un système immunitaire, et les systèmes immunitaires réagissent parfois trop fort, précisément parce que ne pas réagir serait fatal.

Reste la question de la provenance. Ces modèles sont entraînés sur les questions, brouillons et messages de forum de la communauté elle-même, ce qui fait planer la possibilité inconfortable qu'une « découverte » célébrée ne soit qu'une recombinaison de choses que ses futurs relecteurs ont écrites. La crainte de se faire devancer par son propre outil n'a rien de paranoïaque : c'est un problème de traçabilité des données, et tant que les laboratoires ne peuvent pas démontrer cette traçabilité, les relecteurs humains restent les seuls détecteurs de plagiat qui fonctionnent. Ajoutez la politique de la paternité — qui est invité à vérifier, dont le nom figure dans l'annonce, accusations de favoritisme — et vous comprendrez pourquoi la barrière humaine ne peut pas être supprimée. Choisir cinq scientifiques éminents pour bénir un résultat est autant un acte politique qu'épistémique.

Une dernière mise en garde pour quiconque serait tenté de lire les classements comme une mesure de la capacité de recherche : les médailles d'or des compétitions mesurent la performance sur des problèmes conçus pour être résolus en quelques heures. La recherche suit la distribution inverse — des problèmes choisis précisément parce que personne ne sait s'ils sont solubles. C'est la même raison pour laquelle les benchmarks passent à côté de l'essentiel du travail réel en génie logiciel : la métrique récompense le problème mis en forme, pas le problème désordonné. Un modèle qui réussit les problèmes d'olympiade a démontré quelque chose de réel. Il n'a pas démontré son jugement.

La recommandation : faire confiance à la boucle, pas au modèle

Voici ma position, dite franchement. La génération de conjectures est réelle, utile, et ne fera que s'améliorer ; mais la génération de conjectures non vérifiée ne vaut rien, et les preuves en langage naturel sans soutien formel doivent être traitées comme du marketing tant qu'on ne prouve pas le contraire. La vérification de preuves l'emporte à chaque fois que l'artefact doit être cru. La génération l'emporte à chaque fois que le goulot d'étranglement est l'imagination plutôt que la rigueur. Les annonces qui comptent sont celles où les deux sont boulonnés ensemble.

Traitez donc le modèle comme un collaborateur junior prolifique, à l'énergie infinie et sans jugement : tout ce qu'il vous remet passe par l'assistant de preuve avant d'entrer dans l'article, puis par un humain doté de goût avant d'arriver dans l'introduction. Si vous êtes chercheur, apprenez correctement un assistant de preuve — la formalisation est le goulot d'étranglement, et ceux qui savent la piloter vont bientôt être très occupés. Si vous construisez des outils, construisez la boucle, pas la démo. Et la prochaine grande annonce, passez le communiqué, ouvrez la prépublication et vérifiez si le dépôt Lean existe. Les affirmations qui tiennent sont celles qui arrivent déjà vérifiées par machine.