Découverte d’une Anomalie dans le Vérificateur de La Conjecture de Collatz

Les intelligences artificielles génératives détectent des erreurs de code là où on les attend le moins, y compris dans Lean, un vérificateur automatique de démonstrations mathématiques réputé. Le 25 juillet 2026, Ramana Kumar a publié sur GitHub une formalisation dans Lean, prétendant réfuter la célèbre conjecture de Collatz. Cet énoncé, produit par une IA, affirmait que personne ne croyait qu’il existait un entier positif dont l’orbite de Collatz ne rejoignait jamais 1. Bien que l’affirmation soit sans véhémence, elle s’est révélée incorrecte car elle n’avait pas été correctement démontrée. Le 28 juillet, Kiran Gopinathan a découvert que cette démonstration exploitait un bug dans le noyau de Lean. Ce bug, identifié comme le #14576, permettait de prouver que Faux est Vrai, ce que Gopinathan a illustré par un exemple simple. Suite à cela, l’équipe de Lean a renforcé son noyau pour déjouer des bugs similaires. Cependant, en informatique, l’incertitude demeure ; on ne sait jamais quand un nouveau bogue apparaîtra. Par conséquent, la validation par Lean ou d’autres logiciels doit toujours être confirmée de manière indépendante par des systèmes variés.

Kumar, un expert reconnu dans le domaine des méthodes formelles et des langages de vérification, est connu pour son travail sur CakeML, un langage fonctionnel vérifié. Il a utilisé une IA pour identifier les faiblesses du noyau de Lean et, en conséquence, a trouvé une « réfutation sans erreur » (ce qui est accepté par le vérificateur automatique, mais ne devrait pas l’être). L’utiliser pour prouver que Faux est Vrai relevait du trivial, ce qui l’a incité à publier quelque chose de plus spectaculaire : la réfutation de la conjecture de Collatz. Selon Leonardo de Moura, dans son article « Postmortem for Kernel Soundness Bug #14576 », un métaprogramme dans Lean a manipulé la représentation interne des expressions, permettant d’introduire une déclaration en utilisant des constructions telles que mkApp ou mkProj. Grâce à cela, il était possible de déclarer Faux comme Vrai, entraînant des conséquences dévastatrices. Heureusement, le bug a été résolu rapidement et de manière transparente.

Les métaprogrammes sont essentiels pour simplifier l’écriture de démonstrations, permettant un passage fluide entre des théorèmes et des expressions internes. Bien que ces outils puissent contenir des bugs sans affecter le fonctionnement du noyau, ils sont généralement considérés comme sûrs, car toute expression mal typée devrait être rejetée par celui-ci. Toutefois, le bug #14576 a contourné ce mécanisme de sécurité. Gopinathan a pu démontrer la nature du bogue exploité par la fausse réfutation de Collatz, soulignant comment le noyau acceptait simultanément que T soit vrai et faux, rendant la démonstration de toute proposition possible.

En somme, la découverte du bug #14576 est d’une complexité fascinante. Non seulement il a été identifié dans Lean, mais il a également été retrouvé dans Nanoda, une autre implémentation de Lean, ce qui est peu courant. Bien que les détails du travail de Kumar avec l’IA restent obscurs, il est possible qu’il ait cherché un bug similaire à celui trouvé dans Nanoda, utilisant son trouvaille pour attirer l’attention sur la conjecture de Collatz dans les réseaux sociaux. Ce phénomène confirme l’importance d’un audit vigilant et continu des logiciels, car dans le domaine de l’informatique, les défis techniques sont constants.