OpenAI indique qu'une version interne de son nouveau modèle a résolu dix problèmes mathématiques jusqu'ici ouverts, en faisant collaborer plusieurs agents sur une longue durée. En juillet, une conjecture vieille de cinquante ans avait été traitée avec soixante-quatre sous-agents. Ces démonstrations existent. Elles sont longues, techniques, et le nombre d'humains capables de les vérifier entièrement se compte parfois sur les doigts d'une main. Une preuve que presque personne ne peut lire est-elle une preuve ?
Nous avons abordé la capacité de ces systèmes à avoir des idées. Voici la question suivante, et elle est plus ancienne qu'on ne croit.
Ce qu'est une preuve, et pour qui
On imagine volontiers qu'une preuve est un objet : une suite d'étapes logiques, valide ou non, indépendamment de qui la lit. C'est vrai en principe, et ce n'est pas ainsi que fonctionnent les mathématiques réelles.
Une preuve est acceptée quand une communauté l'a lue, comprise, et n'y a pas trouvé de faille. Ce n'est pas seulement un objet logique, c'est un acte social : quelqu'un convainc d'autres personnes, qui engagent leur crédibilité en validant.
Ce point était théorique tant que les preuves restaient lisibles. Il ne l'est plus quand elles dépassent ce qu'un humain peut absorber.
Le précédent, et ce qu'il enseigne
Le problème n'est pas nouveau. En 1976, le théorème des quatre couleurs a été démontré avec l'aide d'un ordinateur qui vérifiait des milliers de cas. Une partie de la communauté a longtemps refusé de considérer cela comme une preuve, précisément parce qu'aucun humain ne pouvait la parcourir.
La solution qui s'est imposée depuis est instructive : plutôt que de lire la preuve, on vérifie le programme qui la vérifie. Des assistants de preuve, des logiciels dont la logique est suffisamment simple pour être elle-même auditée, contrôlent mécaniquement chaque étape. La confiance se déplace de la démonstration vers l'outil de vérification.
C'est le même déplacement que nous décrivions dans notre article sur la confiance : on ne comprend pas l'objet, on comprend le dispositif qui l'a contrôlé.
Les assistants de preuve existaient avant les modèles de langage, et leur combinaison est prometteuse : un modèle propose, un vérificateur formel valide. Dans cette configuration, on n'a pas besoin de faire confiance au modèle, seulement au vérificateur. Le problème est que ce n'est pas toujours ainsi que les résultats sont annoncés. Une preuve produite en langage naturel par un modèle, non traduite en forme vérifiable, repose sur la même chose qu'une preuve humaine trop longue : la parole de celui qui l'a produite. Et nous avons documenté à quel point cette parole est mal calibrée.
Le problème de l'abondance
Il y a une difficulté que le précédent de 1976 ne pose pas : le volume.
Une preuve exceptionnelle mobilise l'attention de toute une communauté. Cent preuves par mois ne la mobiliseront pas. Si des systèmes produisent des résultats plus vite que les humains ne peuvent les examiner, une part croissante de ce qui est annoncé ne sera jamais vérifiée, et ne sera pas non plus contredite.
Cela crée une zone grise inédite : des résultats qui ne sont ni établis ni réfutés, qui s'accumulent, et sur lesquels d'autres résultats viennent se construire. C'est exactement le mécanisme que nous décrivions à propos du code scientifique modernisé : ce qui a l'air juste est repris avant d'être vérifié.
Ce qui semble tenir
Deux exigences, et elles sont plus modestes que la vérification humaine complète.
La forme vérifiable. Un résultat produit par un modèle devrait être exprimé de manière à ce qu'un vérificateur formel puisse le contrôler. Sans cela, ce n'est pas une preuve, c'est une affirmation.
La distinction publique. Il faudrait pouvoir distinguer, dans ce qui est annoncé, ce qui a été formellement vérifié de ce qui ne l'a pas été. Aujourd'hui, les communiqués mêlent les deux.
Ce qu'il faut retenir
La question du titre a une réponse, et elle est ancienne : une preuve que personne ne peut vérifier n'est pas encore une preuve, mais elle peut le devenir si l'on peut vérifier ce qui la vérifie.
Ce que les modèles ajoutent n'est pas un problème philosophique nouveau, c'est un problème de rythme. Les mathématiques ont mis trente ans à accepter une preuve assistée par ordinateur, en construisant les outils qui la rendaient acceptable. Elles n'auront pas trente ans cette fois.
Il reste une chose qui ne change pas, et qui vaut au-delà des mathématiques. Un résultat n'est établi que lorsque quelqu'un d'autre a pu le contester et n'y est pas parvenu. Tant que la contestation reste possible, la connaissance avance. Le jour où l'on accepterait des résultats parce qu'ils sont trop nombreux pour être contestés, on aurait cessé de savoir pour commencer à croire.