Kurt Gödel dejó mucho más de lo que publicó, y casi todo ha sido prácticamente ilegible. Un proyecto de Helsinki del que informa The Guardian indica que un modelo de lenguaje ha hecho en días lo que a un estudioso le llevaría años: exponer el contenido de 1.009 páginas de cuadernos y extraer cientos de teoremas. Es uno de los casos más claros hasta ahora de un modelo de IA útil en la investigación histórica, no en la escritura o el código.
El material son 16 cuadernos que Gödel llenó a principios de la década de 1940, en gran parte en Gabelsberger, una taquigrafía alemana que ya estaba obsoleta cuando él la usaba. Jan von Plato dirige el proyecto en la Universidad de Helsinki desde 2017 con una beca de 2,5 millones de euros del Consejo Europeo de Investigación, y dice ser una de las seis personas en el mundo capaces de leer esa escritura. Tras un congreso sobre IA y demostración de teoremas en agosto, entregó a Claude sus transcripciones, seis libros propios sobre Gödel y otra literatura secundaria. En un par de días tenía una explicación de 650 páginas que, según él, hubo que revisar página por página.
Los resultados más llamativos vienen después. Al preguntarle si los cuadernos contenían una demostración de la independencia del axioma de elección, resultado por el que Paul Cohen ganó la medalla Fields en 1966 y que Gödel afirmaba haber alcanzado antes, Claude encontró un argumento al que le faltaba un paso: una definición era errónea, aunque Gödel tenía la correcta dos años antes. Von Plato dice que la demostración reconstruida pasó la comprobación en el asistente de demostraciones Coq. Después Claude enumeró 663 teoremas que Gödel había demostrado, esbozado o intuido. En Coq, unos 400 se verificaron tal como estaban, unos 200 necesitaron reparación, como un enunciado más preciso o una hipótesis añadida, y unos 50 eran falsos.
Para quien usa Claude con documentos largos, la lección está en la combinación. La ventaja del modelo, en palabras de von Plato, es tener mil páginas a la vista a la vez; la garantía es un verificador formal que no se fía de la palabra del modelo. Es la misma lógica que hay detrás de las herramientas de Lean que cubrimos para matemáticas y verificación.
Las dudas son reales. La reconstrucción no se ha publicado ni revisado, y el lógico de Notre Dame Joel David Hamkins, que no la había visto, advierte que parecerse a la demostración de Cohen no es lo mismo que tenerla, y que cuánto es de Claude y cuánto de Gödel lo tendrán que decidir los historiadores. La afirmación de que hay más de una docena de temas sin explorar procede de Claude, todavía no de personas.