Нейросеть Claude помогла финским исследователям обнаружить 663 математических утверждения в рабочих тетрадях Курта Гёделя, включая завершенные теоремы и черновики доказательств. Об этом рассказал руководитель проекта из Хельсинкского университета Ян фон Плато в интервью The Guardian.
Ученые анализируют 16 тетрадей логика, созданных в начале 1940-х годов и содержащих 1009 страниц, написанных в основном устаревшей немецкой стенографией Габельсбергера. До применения ИИ расшифровка продвигалась со скоростью одна страница в неделю. Фон Плато передал Claude уже расшифрованные тексты, свои книги о Гёделе и научную литературу, после чего модель за несколько дней подготовила 650-страничный анализ и помогла объединить разрозненные идеи.
Из 663 выявленных утверждений около 400 прошли формальную проверку в системе Coq без изменений, примерно 200 потребовали уточнений, а около 50 оказались ошибочными. В тетрадях нашлись идеи, предвосхитившие результаты 1970–1980-х годов, и 14 направлений логики, которые почти не развивались. Особое внимание привлекли записи об аксиоме выбора: Гёдель утверждал, что пришел к результату, за который Пол Коэн получил Филдсовскую медаль в 1966 году, раньше, но не смог восстановить доказательство. Claude помог восстановить почти завершенное рассуждение, исправив одно ошибочное определение, и доказательство прошло проверку в Coq. Однако профессор логики Университета Нотр-Дам Джоэл Дэвид Хэмкинс отметил, что сходство с доказательством Коэна не означает полного завершения работы Гёделя.