Claude помогла найти сотни неизвестных теорем в тетрадях Гёделя
Изображение: OpenAI
Модель Claude помогла найти в математических тетрадях Курта Гёделя сотни ранее неизвестных теорем. Над записями с 2017 года работала команда Хельсинкского университета.
В сентябре модель за пару дней подготовила 650-страничный разбор 1009 страниц записей, рассказал изданию The Guardian руководитель проекта. Прежде команда продвигалась примерно на страницу в неделю. Для анализа руководитель проекта передал Claude расшифровки тетрадей и научную литературу. Полученный разбор требовал постраничной проверки.
Всего Claude выделила 663 утверждения, для которых Гёдель записал доказательство или наметил путь к нему. По словам руководителя проекта, проверка доказательств в программе Coq дала такие результаты:
- Около 400 утверждений прошли проверку без изменений.
- Примерно 200 удалось подтвердить после уточнения формулировок или добавления условий.
- Около 50 оказались ложными. Сам Гёдель иногда отмечал ошибки на полях своих записей.
Отдельно Claude восстановила доказательство независимости аксиомы выбора, которое, по словам руководителя проекта, прошло проверку в Coq. В исходных записях Гёделя было ошибочное определение, хотя правильный вариант он использовал двумя годами ранее.
Профессор логики Университета Нотр-Дам, который не видел реконструкции, считает, что историкам ещё предстоит отделить вклад Claude от вклада Гёделя. Сходство записей с известным доказательством не означает, что у Гёделя оно было готово, подчеркнул учёный.
