Pourquoi la preuve mathématique d'OpenAI sur la conjecture de Connes a échoué

OpenAI a annoncé début août avoir résolu dix problèmes mathématiques ouverts, dont la réfutation de la conjecture de rigidité de Connes — un énoncé formulé vers 1980 par Alain Connes. La démonstration, rédigée en 37 000 lignes de Lean 4, avait été validée ligne par ligne par le kernel, rapporte le média 36 Kr. Vingt-quatre heures plus tard, J. L. Nielsen, du Center for Topological Physics de l'Université du Kansas, publiait une réfutation: le contre-exemple proposé par l'IA ne satisfait pas les conditions que la conjecture exige. Une piqûre de rappel utile sur ce que « vérifier » veut vraiment dire.

Ce que Lean certifie, et ce qu'il ne certifie pas

Lean est un assistant de preuve: il vérifie que chaque étape découle formellement de la précédente, et il le fait bien. Ce qu'il ne fait pas, c'est juger si l'énoncé qu'on lui demande de prouver correspond à l'énoncé qu'on voulait prouver. Le diagnostic de Nielsen tombe exactement là: ce que le code démontre n'est pas ce que la conjecture de Connes demande. En clair, ta rédaction peut être syntaxiquement irréprochable et néanmoins répondre à côté de la question.

Remonter aux définitions, méthode Nielsen

Nielsen a reconstitué la chaîne complète du code publié — un fichier unique où les noms d'origine du code modulaire avaient disparu. Il a construit un tableau reliant chaque objet à son numéro de ligne: le cocycle supérieur à la ligne 13 700, le groupe tordu à la ligne 14 069, la preuve d'isomorphie des deux algèbres à la ligne 36 712, le théorème principal à la ligne 36 954. Puis il a remonté toute la chaîne prouvant la condition ICC, des lignes 31 430 à 31 610.

Sa conclusion: les lemmes portent sur des objets après transformation duale, pas sur le groupe d'origine avec ses éléments centraux — la preuve ne couvre donc pas directement ce qu'elle prétend couvrir. Nielsen identifie aussi un décalage entre la définition de la propriété (T) codée et la définition mathématique originale de Kazhdan. Deux chemins de défaillance indépendants, pour un même résultat: l'IA prouve autre chose que ce qui était à prouver.

Ce que tu en tires pour ta copie

Deux réflexes à importer dans ton brouillon, du brevet au supérieur.

D'abord, tracer au brouillon ce que l'énoncé exige réellement — conditions, hypothèses, quantificateurs — avant d'écrire la moindre ligne de justification. Ton correcteur cherche à lire une démonstration qui répond à la question posée, pas une démonstration voisine. Si tu prouves une propriété approchante mais pas celle demandée, tu perds les points de la conclusion, même si chaque ligne intermédiaire est juste.

Ensuite, quand un énoncé renvoie à une définition, retourner à cette définition. Nielsen a trouvé la faille précisément parce qu'il a comparé la définition codée à la définition mathématique originale. À ton échelle: si un exercice parle de « triangle isocèle », vérifie sur ta figure que tu utilises bien les deux côtés égaux — pas la médiane, pas la hauteur — avant d'invoquer le théorème.

Reste à suivre: OpenAI n'a pas indiqué si la démonstration sera révisée ou si le contre-exemple sera abandonné. Le débat, lui, reste ouvert.