Post #564

Истерия вокруг «ИИ» создаёт ощущение, что компьютерные достижения в математике — это что-то новое Но история куда длиннее… Одним из первых громких случаев «компьютерного доказательства» стало решение проблемы о четырёх красках в 1976 году Звучит она так: любую карту можно раскрасить четырьмя цветами так, чтобы соседние области не совпадали Доказательство оказалось настолько громоздким, что без компьютера справиться было невозможно — программа перебрала 1936 конфигураций, но математики всё равно относились к неручной работе с подозрением В конце XX века разрешилась гипотеза Кеплера о плотнейшей упаковке шаров О ней, кстати, уже писали ранее тут и тут Она оставалась недоказанной почти 400 лет В 1998 году Томас Хейлс заявил о доказательстве, включавшем тысячи страниц текста и гигабайты расчётов Эксперты ошибок не нашли, но и проверить результат вручную им не удалось Так в 2003 году родился проект FlySpeck, завершившийся в 2014 Ещё один пример — теорема Фейта-Томпсона Это теорема о разрешимости конечных групп нечётного порядка Оригинальное доказательство было опубликовано в 1963 году Его формализация в системе Coq в 2012 году под руководством Жоржа Гонтье стала вехой в истории компьютерной проверки доказательств и заняла почти пятнадцать лет ️️ И, конечно, классификация конечных простых групп Грандиозный проект длиной в полвека и объёмом более десяти тысяч страниц Здесь компьютеры играли заметную роль в доказательствах, связанных со спорадическими группами Один из идеологов проекта, в шутку называл классификацию «тридцатилетней войной» Эти примеры показывают: компьютеры давно участвуют в математике, но скорее как верификаторы, перебирающие варианты, проверяющие случаи и формально подтверждающие логические выводы Первые системы середины XX века были символическими, логическими и уже «пытались рассуждать и доказывать» Logic Theorist, родившаяся в 1956 году, была первой программой, которую создатели прямо назвали «искусственным интеллектом» Она смогла доказать 38 из 52 теорем из Principia Mathematica Программу представили на Дартмутской конференции 1956 года, которая считается моментом рождения Ml как научной дисциплины Через год появилась GPS Программа General Problem Solver демонстрировала универсальный подход к решению задач — от логических головоломок и алгебраических преобразований до просчёта шахматных позиций Проблема была лишь в том, что комбинаторный взрыв делал сложные задачи непосильными компьютеру Тем не менее это был не он За этими программами стояла важная идея формализации математики, которая возникла задолго до компьютеров Формализация утверждала, что любая теорема — это цепочка строго определённых логических шагов