ИИ помог формализовать доказательство Перельмана
Команда математиков сообщила о полной формализации доказательства гипотезы Пуанкаре на языке Lean — при помощи ИИ.
Результат, полученный Григорием Перельманом в 2002–2003 годах, перевели в форму, позволяющую компьютеру проверять каждый логический шаг.
За проектом стоит межвузовская команда из США:
Bennett Chow (University of California San Diego)
Yuan Liao (University of California San Diego)
Ziyang Qin (Cornell University, Math+AI Lab)
Ayush Khaitan (Princeton University, Princeton Language and Intelligence)
Общая тема этой коллаборации — геометрия и автоматизация математических доказательств. Они создают библиотеку, в которой результаты современной математики доступны для машинной проверки и дальнейшего использования.
Математики определяли стратегию и проверяли формулировки, ИИ помогал писать формальные доказательства, а Lean проверял их логическую корректность.
Код открыт; авторы заявляют отсутствие пропущенных доказательств. Автоматическая сборка проекта прошла успешно.
🔗 Код и описание проекта · Результат автоматической проверки
Команда математиков сообщила о полной формализации доказательства гипотезы Пуанкаре на языке Lean — при помощи ИИ.
Результат, полученный Григорием Перельманом в 2002–2003 годах, перевели в форму, позволяющую компьютеру проверять каждый логический шаг.
За проектом стоит межвузовская команда из США:
Bennett Chow (University of California San Diego)
Yuan Liao (University of California San Diego)
Ziyang Qin (Cornell University, Math+AI Lab)
Ayush Khaitan (Princeton University, Princeton Language and Intelligence)
Общая тема этой коллаборации — геометрия и автоматизация математических доказательств. Они создают библиотеку, в которой результаты современной математики доступны для машинной проверки и дальнейшего использования.
Математики определяли стратегию и проверяли формулировки, ИИ помогал писать формальные доказательства, а Lean проверял их логическую корректность.
Код открыт; авторы заявляют отсутствие пропущенных доказательств. Автоматическая сборка проекта прошла успешно.
🔗 Код и описание проекта · Результат автоматической проверки