Математики предупреждают: спешная формализация всей математики с помощью AI может нанести непоправимый вред
How to Formalize All of Mathematics
Группа математиков во главе с Jeremy Avigad, Kevin Buzzard и Johan Commelin реагирует на призывы после релиза OpenAI формализовать всю математику. Они признают мощь AI в доказательстве теорем, но предостерегают: поспешная крупномасштабная формализация приведёт к трате ресурсов и долгосрочному ущербу. Пример — попытка Math, Inc. перехватить проект по формализации результатов Maryna Viazovska: AI-код пришлось выбросить. Авторы предлагают позитивное видение качественной формализации.
Если всё сделать хорошо, крупномасштабная скоординированная формализация может чрезвычайно расширить математическое исследование и открытия. Если сделать плохо, это будет в лучшем случае пустой тратой ресурсов; скорее всего, это нанесёт долгосрочный ущерб.