En septembre, le logicien finlandais Jan von Plato a confié à Claude, le modèle d’IA d’Anthropic, ses transcriptions des carnets de travail du mathématicien Kurt Gödel. En quelques jours, il disposait d’une explication de 650 pages couvrant les 1 009 pages des seize carnets, remplis au début des années 1940. Dans le projet qu’il dirige depuis 2017 à l’université d’Helsinki, son équipe en comprenait jusque-là les mathématiques au rythme d’environ une page par semaine. Von Plato l’a raconté au Guardian dans un entretien publié le 13 novembre 2026.
Il a ensuite demandé à Claude de recenser tous les théorèmes pour lesquels Gödel avait une preuve, une esquisse de preuve ou une simple idée de preuve : Claude en a trouvé 663. Ces théorèmes ont été soumis à Coq, un vérificateur de preuves, autrement dit un logiciel qui contrôle une démonstration étape par étape. Selon von Plato, environ 400 ont été validés tels quels, environ 200 ont dû être corrigés et une cinquantaine se sont révélés faux. Le Guardian ne cite aucun article, aucune prépublication ni aucun fichier Coq, et rien n’avait été rendu public au 14 novembre.
La première question de von Plato à Claude portait sur l’axiome du choix, un principe de base des mathématiques, et le modèle a reconstitué une preuve de Gödel sur ce sujet. Joel David Hamkins, professeur de logique à l’université Notre-Dame (Indiana), n’a pas vu cette preuve. Il juge pour le Guardian que, si elle tient, le résultat est « remarquable et intéressant pour l’histoire ». La part qui revient à Claude et celle qui revient à Gödel, ajoute-t-il, « c’est aux historiens de la déterminer ».
Une page par semaine, dans une sténographie disparue
Gödel a publié en 1931 ses deux théorèmes d’incomplétude. Ils établissent que tout système de règles mathématiques sans contradiction, assez puissant pour l’arithmétique ordinaire, contient des énoncés qu’on ne peut ni démontrer ni réfuter. Après les années 1930, Gödel a très peu publié, alors que ses papiers inédits comptent des dizaines de milliers de pages, rappelle le Guardian. Il a quitté l’Autriche en 1940, s’est installé à Princeton, aux États-Unis, et est mort en 1978.
Les seize carnets (Arbeitshefte en allemand) sont en grande partie écrits en Gabelsberger, une sténographie allemande déjà tombée en désuétude à l’époque de Gödel. CORDIS, la base de données de la Commission européenne sur les projets de recherche, qualifie cette écriture abrégée de « vraie énigme » pour qui s’intéresse à son contenu. Von Plato a appris seul à la lire et affirme être l’une des six personnes au monde qui en sont capables. Le Conseil européen de la recherche a financé le projet à hauteur d’environ 2,1 millions d’euros de 2018 à 2024, selon CORDIS.
« Les humains lisent une page à la fois et nous oublions des choses », explique von Plato au Guardian. « Il nous faut un an pour lire une cinquantaine de pages. »
Claude livre une synthèse de 650 pages en quelques jours
En août, lors d’un colloque en France sur l’IA et la démonstration automatique de théorèmes par ordinateur, des informaticiens ont suggéré à von Plato d’essayer Claude. De retour à Helsinki, il a fourni au modèle ses transcriptions des carnets, les six livres qu’il a écrits sur Gödel et d’autres travaux universitaires. Selon le récit du Guardian, Claude a donc travaillé à partir de ces transcriptions, et non des pages en sténographie. Le journal ne précise pas quelle version de Claude a été utilisée.
« En quelques jours, j’ai pu voir une explication de 650 pages des carnets », raconte von Plato. « Il a fallu la contrôler page par page, mais c’est en gros un travail impossible à faire pour des êtres humains. » Il attribue ce résultat à la mémoire de la machine : « L’IA peut relier tous les morceaux sur un millier de pages. »
Au rythme d’une page par semaine, les 1 009 pages des carnets auraient demandé environ 19 ans de travail. Les deux chiffres mesurent des tâches différentes : la compréhension complète des mathématiques par un spécialiste, et un premier passage qu’il a fallu ensuite contrôler page par page.
L’axiome du choix, puis 663 théorèmes
La première question posée à Claude renvoyait à une vieille revendication de Gödel. En 1966, Paul Cohen a reçu la médaille Fields, la plus haute distinction en mathématiques, pour un résultat sur la théorie des ensembles, la branche qui étudie les collections d’objets. Il avait montré que deux énoncés ne peuvent être ni démontrés ni réfutés à partir des règles habituelles de cette théorie. Le premier, l’hypothèse du continu, porte sur la taille des ensembles infinis ; le second, l’axiome du choix, permet de choisir un élément dans chaque ensemble non vide d’une collection, même infinie.
D’après le Guardian, Gödel a alors affirmé avoir démontré ce résultat dans les années 1940. Quand ses collègues lui ont demandé la preuve, il n’a pas réussi à la reconstituer à partir de ses notes. Von Plato a demandé à Claude si les carnets contenaient une telle preuve pour l’axiome du choix. Selon le journal, la réponse a été : « oui, presque ».
« Il n’était qu’à un pas », précise von Plato. « Il y a une définition sur laquelle Gödel s’est trompé, mais il avait la bonne deux ans plus tôt. » Von Plato a soumis à Coq la preuve reconstituée par Claude, et elle a passé le contrôle.
L’équipe d’Helsinki avait repéré ce résultat avant de consulter Claude. La page de présentation du projet décrit ses travaux tels qu’ils étaient en 2019. Elle cite « sa preuve de 1942 de l’indépendance de l’axiome du choix » parmi les résultats que l’on pouvait en partie prévoir. L’indépendance désigne ici le fait que l’axiome ne peut être ni démontré ni réfuté.
Sur les 663 théorèmes relevés par Claude, « environ 400 ont été vérifiés tels qu’énoncés, environ 200 ont été réparés, c’est-à-dire qu’il a peut-être fallu préciser l’énoncé du théorème ou ajouter une hypothèse », détaille von Plato. « Environ 50 étaient faux, ce qui n’a rien d’étonnant. » Gödel lui-même annotait parfois ses notes d’un « falsch! » (faux) en marge.
Coq s’appelle aujourd’hui Rocq Prover. Anthropic s’en est servi en octobre, quand Claude a écrit des preuves d’absence de plantage, vérifiées par machine, dans 123 bibliothèques logicielles à code source ouvert.
Selon von Plato, les carnets étudiés contiennent aussi « des dizaines d’anticipations de résultats inconnus jusqu’aux années 1970 et 1980 » et « 14 thèmes de logique qui n’ont pas été approfondis ». Une fois ses projets de logique en cours terminés, il compte s’attaquer aux carnets de Gödel consacrés à la physique et à la cosmologie.
D’autres résultats d’IA passés au vérificateur cette année
Un autre résultat de Gödel était déjà passé au vérificateur avec l’aide de Claude en 2026. Le 1er juin, Thierry Coquand, professeur d’informatique à l’université de Göteborg, en Suède, a déposé un article sur arXiv, un site où les chercheurs mettent leurs articles en ligne sans attendre leur parution dans une revue. Il y décrit une preuve du second théorème d’incomplétude de Gödel, selon lequel un système cohérent assez puissant pour l’arithmétique ne peut pas démontrer sa propre cohérence. Écrite dans Agda, un autre vérificateur de preuves, elle compte environ 50 000 lignes, n’admet aucune hypothèse sans preuve et a été entièrement produite en dialogue avec Claude.
L’auteur précise n’avoir écrit aucune ligne de code Agda. Une première tentative avait échoué : elle reposait sur un lemme faux, un résultat intermédiaire tiré d’un article plus ancien. Claude avait fini par démontrer un énoncé qui ressemblait seulement au théorème de Gödel.
Le 10 novembre, dans un autre domaine, Google DeepMind, le laboratoire d’IA de Google, a annoncé un résultat en sécurité informatique. Ses agents, des programmes d’IA qui enchaînent des tâches, ont démontré des propriétés de sécurité clés du code compilé du protocole Signal, un travail mené en quatre semaines. Ce protocole chiffre les messages de l’application Signal ; le code compilé est la version du programme que l’ordinateur exécute. Les agents ont écrit plus de six millions de lignes de Lean, un vérificateur de preuves comparable à Coq et à Agda.
Selon l’entreprise, ce travail prenait des années à des équipes d’experts. Il s’agissait d’une preuve de concept, une démonstration de faisabilité qui ne couvrait pas toute l’application Signal, a rapporté le magazine américain WIRED dans un article repris par le site Ars Technica.
Lean a aussi servi à contrôler deux autres travaux d’IA cet automne. En octobre, la jeune entreprise Axiom a converti en 24 jours une preuve de 15 000 pages en code Lean avec des agents d’IA. Le 10 novembre, un comité présidé par un prix Nobel a validé une preuve de physique produite par une IA en s’appuyant sur les vérifications de Lean.
Les limites de l’entretien
Tous les chiffres sur le travail de l’IA viennent d’un seul entretien, celui de von Plato au Guardian. Von Plato n’a publié ni la synthèse de 650 pages, ni la liste des 663 théorèmes, ni les fichiers Coq, si bien que personne en dehors de son équipe ne peut les contrôler. Les trois résultats du contrôle (environ 400, environ 200 et une cinquantaine) sont arrondis et totalisent 650, soit 13 de moins que 663. L’entretien ne dit pas ce que sont devenus les autres théorèmes.
Les quelque 200 énoncés réparés posent une autre question. Ils ont été rendus plus précis ou complétés d’une hypothèse, c’est-à-dire d’une condition supplémentaire, avant de passer le contrôle. Pour être soumis à Coq, un énoncé doit être réécrit dans le langage du logiciel : on parle de sa version formelle. Le Guardian ne dit pas qui a rédigé ces versions formelles, von Plato ou Claude.
L’article de Coquand montre pourquoi cette étape pèse. Un vérificateur confirme qu’une preuve correspond à son énoncé, sans juger si cet énoncé traduit bien l’idée de départ. La première tentative de Coquand, bâtie sur un lemme faux, montrait qu’un modèle peut « raisonner correctement à partir d’une spécification formelle incorrecte ».
Reste la question du mérite. À propos de l’axiome du choix, Hamkins observe dans le Guardian que, chez Gödel, des éléments qui ressemblent à la preuve de Cohen « ne veulent pas dire qu’il l’avait. Cela montre qu’il était sur la voie. On n’obtient pas le mérite d’un travail dont on ne parle à personne ».
Avant Claude, le projet avait publié dans des revues scientifiques, dont un article de von Plato et Akihiro Kanamori paru en septembre 2025 dans History and Philosophy of Logic. Il porte sur la première preuve, par Gödel, de la cohérence de l’axiome du choix, c’est-à-dire du fait que cet axiome ne contredit pas les autres règles de la théorie des ensembles.
Notre analyse
Pendant neuf ans, la lecture a limité l’étude des carnets de Gödel. Une poignée de personnes savaient déchiffrer la sténographie, et les mathématiques se comprenaient au rythme d’une page par semaine. Si le récit de von Plato se confirme, un modèle d’IA peut désormais faire en quelques jours un premier passage complet sur les transcriptions. Un vérificateur de preuves contrôle ensuite chaque énoncé, un par un.
Le travail qui exige des spécialistes se déplace donc vers l’étape suivante. Il faut énoncer chaque théorème avec précision, vérifier les 650 pages de la synthèse contre la source et décider à qui revient chaque idée. Selon les chiffres de von Plato, environ 200 des 663 énoncés, soit environ 30 %, ont dû être réparés.
Les 1 009 pages des seize carnets ne forment qu’une petite partie des dizaines de milliers de pages inédites laissées par Gödel. Trois points sont à suivre : la publication éventuelle des fichiers Coq et de la liste des théorèmes, l’avis des historiens sur la preuve reconstituée par Claude à propos de l’axiome du choix, et ce que révéleront les carnets de physique et de cosmologie.
Sources
- ‘Ahead of his time’: AI helps unlock discoveries hidden in notebooks of man who transformed maths, Alex Bellos, The Guardian, 13 novembre 2026
- The Gödel Enigma: Unveiling a Hidden Logical Heritage (GODELIANA), ERC Advanced Grant 787758, CORDIS, Commission européenne, consulté le 14 novembre 2026
- Project description, Gödel Enigma research group, Université d’Helsinki, consulté le 14 novembre 2026
- Auto formalisation of Goedel’s Second Incompleteness Theorem in Binary Recursive Arithmetic, Thierry Coquand, arXiv, 1er juin 2026 (révisé le 2 juin 2026)
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Pushmeet Kohli et Swarat Chaudhuri, Google DeepMind, 10 novembre 2026
- Google DeepMind just mathematically verified key parts of Signal, Lily Hay Newman (WIRED), Ars Technica, 11 novembre 2026
Image d’en-tête : graphique MACCUS, données de Jan von Plato, interrogé par The Guardian, 13 novembre 2026
