Микола Канян

Область, где языковые модели являются бесспорной инновацией в формализации доказательств, это самый первый шаг: запись теорем на формальном языке (т.е. до поиска контрпримеров, до написания и проверки собственно доказательств). Им можно скармливать красиво набранные в LaTeX статьи и получать на выходе машиночитаемые определения. Ничего удивительно здесь нет, потому что языковые модели и были изобретены для перевода с одного языка на другой. Они решают не саму проблему доказательства, а пользовательского интерфейса к уже существующим инструментам. Тем не менее, я не думаю, что все это как-то изменит математику как область знания, потому что математика никому не интересна. Шум о «замене математиков языковыми моделями» будет продолжаться лишь до тех пор, пока он работает как реклама для изделий Nvidia. Роль математика состоит вовсе не в доказательстве теорем, а в понимании. Существует бесконечное число теорем, и почти все они неинтересны. Пока «искусственный интеллект» (в любой форме, необязательно «языковых моделей») не станет способен к религиозному опыту и к его представлению в виде цеховых мистерий, он не заменит людей-математиков.