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