Claude ajuda um lógico de Helsinque a decifrar os cadernos em taquigrafia de Gödel e encontra centenas de teoremas

O The Guardian informa que Jan von Plato, que lidera desde 2017 um projeto da Universidade de Helsinque sobre os 16 “cadernos” do início da década de 1940 de Kurt Gödel (1.009 páginas, muitas delas escritas na obsoleta taquigrafia Gabelsberger), forneceu a Claude suas transcrições, seus livros anteriores sobre Gödel e a literatura secundária em setembro. Segundo von Plato, Claude produziu uma explicação de 650 páginas dos cadernos em poucos dias, que, afirma ele, precisou ser conferida página por página.

O que von Plato diz que Claude encontrou. Perguntado se os cadernos contêm uma prova de que o axioma da escolha é independente, Claude reconstruiu uma que, segundo von Plato, está “quase” completa, com uma definição incorreta que Gödel havia acertado dois anos antes. Ele diz que a prova reconstruída passou pelo assistente de provas Coq. Quando solicitado a extrair todos os teoremas que Gödel provou, esboçou ou teve a ideia de provar, Claude listou 663. Von Plato diz que cerca de 400 foram verificados como enunciados em Coq, cerca de 200 precisaram de correções e cerca de 50 eram falsos. Ele também afirma que Claude identificou mais de uma dúzia de temas de lógica que ainda não foram investigados.

Ressalvas. Joel David Hamkins, da Notre Dame, que não havia visto a reconstrução, disse ao The Guardian que, se ela resistir ao escrutínio, será “notável e historicamente interessante”, mas que cabe aos historiadores determinar quanto dela é de Claude e quanto é de Gödel; acrescentou que a semelhança com a prova de Cohen não significa que Gödel a tivesse elaborado.