Claude aide un logicien d’Helsinki à déchiffrer les cahiers en sténographie de Gödel, révélant des centaines de théorèmes

The Guardian rapporte que Jan von Plato, qui dirige depuis 2017 un projet de l’Université d’Helsinki consacré aux 16 « cahiers » du début des années 1940 de Kurt Gödel (1 009 pages, dont une grande partie rédigée dans l’ancienne sténographie Gabelsberger), a fourni à Claude ses transcriptions, ses ouvrages antérieurs sur Gödel et la littérature secondaire en septembre. Selon von Plato, Claude a produit en quelques jours une explication de 650 pages des cahiers, qu’il dit avoir dû vérifier page par page.

Ce que von Plato dit que Claude a trouvé. À la question de savoir si les cahiers contiennent une preuve de l’indépendance de l’axiome du choix, Claude en a reconstitué une qui, selon von Plato, est « presque » complète, avec une définition erronée que Gödel, lui, avait correctement formulée deux ans plus tôt. Il affirme que la preuve reconstituée a été validée par l’assistant de preuve Coq. Invité à extraire tous les théorèmes que Gödel avait démontrés, esquissés ou envisagés, Claude en a répertorié 663. Von Plato affirme qu’environ 400 ont été vérifiés tels quels dans Coq, qu’environ 200 ont nécessité des corrections et qu’environ 50 étaient faux. Il dit également que Claude a identifié plus d’une douzaine de thèmes logiques qui n’ont pas été explorés.

Réserves. Joel David Hamkins, de Notre Dame, qui n’avait pas vu la reconstitution, a déclaré à The Guardian que si elle résiste à l’examen, elle est « remarquable et historiquement intéressante », mais que la part de Claude et celle de Gödel relèvent d’une question pour les historiens, et que le fait qu’elle ressemble à la preuve de Cohen ne signifie pas que Gödel l’avait trouvée.