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