️️️️ИИ решил математическую задачу, с которой человечество не могло справиться десятилетиями️️️️

В новостях всё чаще появляются подобные заголовки. Звучит впечатляюще, но стоят ли за этим полноценные научные результаты? Или всё ради хайпа? Давайте разбираться — разговор будет основательный и с пруфами!

Глава 1: Не ИИ, а алгоритмы

Повестка вокруг ИИ создаёт ощущение, что компьютерные достижения в математике — это что-то новое. Но история куда длиннее…

Одним из первых громких случаев «компьютерного доказательства» стало решение проблемы о четырёх красках в 1976 году.

Звучит она так: любую карту можно раскрасить четырьмя цветами так, чтобы соседние области не совпадали. Доказательство оказалось настолько громоздким, что без компьютера справиться было невозможно — программа перебрала 1936 конфигураций, но математики всё равно относились к неручной работе с подозрением.

В конце XX века разрешилась гипотеза Кеплера о плотнейшей упаковке шаров. О ней мы, кстати, уже писали ранее тут и тут.

Она оставалась недоказанной почти 400 лет. В 1998 году Томас Хейлс заявил о доказательстве, включавшем тысячи страниц текста и гигабайты расчётов. Эксперты ошибок не нашли, но и проверить результат вручную им не удалось. Так в 2003 году родился проект FlySpeck, завершившийся в 2014-м.

Ещё один пример — теорема Фейта-Томпсона.

Это теорема о разрешимости конечных групп нечётного порядка. Оригинальное доказательство было опубликовано в 1963 году. Его формализация в системе Coq в 2012 году под руководством Жоржа Гонтье стала вехой в истории компьютерной проверки доказательств и заняла почти пятнадцать лет.

️️ И, конечно, классификация конечных простых групп.

Грандиозный проект длиной в полвека и объёмом более десяти тысяч страниц. Здесь компьютеры играли заметную роль в доказательствах, связанных со спорадическими группами. Один из идеологов проекта, в шутку называл классификацию «тридцатилетней войной».

Эти примеры показывают: компьютеры давно участвуют в математике, но скорее как верификаторы, перебирающие варианты, проверяющие случаи и формально подтверждающие логические выводы.

Однако и искусственный интеллект в математике появился вовсе не вчера!

Глава 2: Не алгоритмы, а ИИ

Первые ИИ-системы середины XX века были символическими, логическими и уже тогда пытались рассуждать и доказывать.

️️ Logic Theorist, родившаяся в 1956 году, была первой программой, которую создатели прямо назвали «искусственным интеллектом».

Она смогла доказать 38 из 52 теорем из Principia Mathematica. Программу представили на Дартмутской конференции 1956 года, которая считается моментом рождения ИИ как научной дисциплины.

️️ Через год появилась GPS.

Программа General Problem Solver демонстрировала универсальный подход к решению задач — от логических головоломок и алгебраических преобразований до просчёта шахматных позиций. Проблема была лишь в том, что комбинаторный взрыв делал сложные задачи непосильными компьютеру. Тем не менее это был настоящий ИИ.

За этими программами стояла важная идея формализации математики, которая возникла задолго до компьютеров. Формализация утверждала, что любая теорема — это цепочка строго определённых логических шагов.

А это значит, что математики могли поручить машине вычисления и, главное, рассуждения, пусть и на ограниченных мощностях. Как думаете, что-то изменилось сейчас, в 21 веке?

Будем рады почитать ваши мысли в комментах. И тыкайте на 🙊, если хотите знать, что за история с заголовками, и почему она нас так волнует. Расскажем завтра!

#история