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