Математики, используя компьютерную программу Lean, подтвердили точность сложной теоремы на переднем крае исследовательской математики. Комментарий Сохранить статью Прочитать позже
Введение
Помощники по компьютерному доказательству уже много лет являются интригующей темой в математике, обещая автоматизировать основные аспекты работы математиков, но на практике оказывая незначительное влияние на эту область.
Однако новый результат, полученный в начале июня, ощущается как первый успех новичка в высшей лиге: наконец-то помощник по доказательству внес реальный вклад в передовые математические исследования, проверив правильность сложного современного доказательства.
«Это показывает, что современную математику можно формализовать с помощью средства доказательства теорем», — сказал Бхавик Мехта, аспирант Кембриджского университета, участвовавший в работе.
Доказательство, о котором идёт речь, принадлежит Петеру Шольце из Боннского университета, одному из самых уважаемых математиков в мире. Это лишь часть более масштабного проекта под названием «концентрированная математика», над которым он и Дастин Клаузен из Копенгагенского университета работают уже несколько лет.
Их цель — создать новые основы топологии, заменив традиционное понятие топологического пространства, примеры которого включают сферу и пончик, более универсальными объектами, которые авторы называют конденсированными множествами. В этой новой перспективе топологические пространства рассматриваются как собранные из бесконечного количества склеенных вместе точек пыли.
Этот проект включает в себя особенно важное и сложное доказательство, которое Шольце разработал самостоятельно в течение напряженной недели в июле 2019 года. Оно устанавливает, что область математики, называемая вещественным функциональным анализом, по-прежнему работает, если заменить топологические пространства конденсированными множествами.
Шольце начал доказательство в понедельник. Он работал исключительно в уме, почти ничего не записывая, не говоря уже о компьютере. К полудню четверга он почти разобрался, за исключением одного фрагмента, который никак не мог решить. Он также чувствовал напряжение от чрезмерной концентрации, необходимой для удержания столь сложного аргумента в активной памяти. Поэтому в тот вечер он отдохнул с друзьями в баре. Он заплатил за него следующим утром, в пятницу.
«У меня было ужасное похмелье», — сказал Шольце.
Но он также понимал, что на выходных у него не будет времени поработать, поэтому пятница была лучшим шансом закончить доказательство. Мысль о том, что он потеряет связь со всем, что накопил за последнюю неделю, а в понедельник придётся начинать всё заново, была ему не по душе.
«Я не думал, что у меня хватит умственных способностей снова воссоздать это в голове», — сказал Шольце.
Итак, он с трудом довёл дело до конца и закончил доказательство. Но потом он не был уверен в правильности своего решения. Причина была не только в туманных обстоятельствах, при которых он преодолел последнее препятствие. Доказательство было настолько сложным, что Шольце понимал, что он, возможно, что-то упустил.
«Это очень запутанная система со множеством подвижных частей. Сложно понять, какие части и на сколько смещаются при изменении одного из этих параметров», — сказал Шольце.
Шольце нашел время записать доказательство только в ноябре 2019 года. Год спустя он связался с Кевином Баззардом, математиком из Имперского колледжа Лондона и видным сторонником программы Lean для помощи в доказательстве. Шольце хотел узнать, можно ли перевести его доказательство в Lean, превратив его в строки кода, как в программе, чтобы программа могла проверить его истинность.
Баззард поделился исследованием Шольце с несколькими другими членами сообщества Lean, включая Йохана Коммелина, постдокторанта из Фрайбургского университета. У Коммелина был идеальный опыт для этой работы — он использовал Lean несколько лет и был знаком с краткой математикой — и он был убеждён, что проверка доказательства Шольце во многом укрепит положение помощника-доказательника в математическом сообществе.
«Возможность сотрудничать с Питером в таком проекте и упоминание его имени в нем стало бы огромным стимулом для Lean», — сказал Коммелин.
Но он также считал, что на это может уйти год или больше, и это заставило его задуматься. Коммелин опасался, что он потратит всё это время на проверку доказательства, а в итоге остальной математический мир просто пожмёт плечами.
«Я подумал, что если я потрачу два года, работая над этим, выйду из своей пещеры и скажу: „Всё отлично“, то весь остальной мир скажет: „Ух ты, мы это уже знали, Питер доказал“», — сказал Коммелин. Не имело значения, что сам Шольце не был до конца уверен.
Поэтому Коммелин спросил Шольце, готов ли он сделать публичное заявление, подтверждающее важность работы. Шольце согласился и 5 декабря 2020 года опубликовал пост в блоге Баззарда.
Они назвали его «Эксперимент с жидким тензором», отсылая к математическим объектам, участвующим в доказательстве, называемым жидкими вещественными векторными пространствами, и к прогрессивной рок-группе «Liquid Tension Experiment», которую они с Коммелином любят. В вводной части объёмом 4400 слов Шольце объяснил некоторые технические аспекты полученного результата, а затем добавил примечание, простым языком подтверждающее, по его мнению, важность проверки его с помощью компьютера.
«Думаю, это, пожалуй, моя самая важная теорема на сегодняшний день. (Пока что она не имеет реальных применений, но я уверен, что это изменится)», — написал Шольце. «Лучше убедиться, что она верна…»
Получив необходимые гарантии, Коммелин приступил к работе. Объяснив Лину математическое утверждение, доказательство которого он в конечном итоге хотел проверить с помощью программы, он привлёк к проекту других математиков. Они определили несколько лемм — промежуточных шагов доказательства, — которые показались наиболее доступными. Сначала они формализовали их, закодировав на основе библиотеки математических знаний, к которым Лин обращается для определения истинности данного утверждения.
В октябре прошлого года издание Quanta писало, что коллективные усилия по написанию математических формул на языке Lean напоминают «строительство амбара». Этот проект не стал исключением. Коммелин выделил отдельные части доказательства и опубликовал их на Zulip, форуме, который служит центром сообщества Lean. Когда математики находили часть доказательства, соответствующую их компетенции, они добровольно формализовали её.
Мета был одним из примерно дюжины математиков, внесших свой вклад в эту работу. В мае он увидел сообщение от Коммелина с просьбой помочь формализовать доказательство утверждения, называемого леммой Гордана, которое было связано с работами Меты в области комбинаторной геометрии. Он потратил неделю на то, чтобы закодировать доказательство в терминах, согласующихся с более обширным доказательством, которое разрабатывали математики. По его словам, это символизирует принцип работы Lean.
«Это большое сотрудничество множества людей, которые делают то, что у них хорошо получается, чтобы создать единый монолит», — сказал он.
По мере продвижения работы Шольце постоянно присутствовал на «Зулипе», отвечая на вопросы и разъясняя пункты доказательства — словно архитектор, дающий указания строителям на стройплощадке. «Он всегда был рядом», — сказал Коммелин.
В конце мая группа завершила формализацию той части доказательства, в которой Шольце был наиболее не уверен. Коммелин нажал последнюю клавишу в 1:10 утра 29 мая. Лин скомпилировал доказательство, и оно заработало как функционирующая программа, подтвердив 100%-ную корректность работы Шольце. Теперь Шольце и другие математики могут применять эти методы из вещественного функционального анализа к уплотнённым множествам, зная, что они определённо будут работать в этой новой ситуации.
И хотя Шольце по-прежнему предпочитает придумывать доказательства в уме, способности Лина произвели на него впечатление. Теперь он может предвидеть, что подобные программы будут играть важную роль в исследовательской математике.
«Этот эксперимент радикально изменил моё представление о возможностях [помощников по доказательной работе], — сказал Шольце. — Теперь я считаю, что в принципе разумно формализовать всё, что угодно, в Lean. Никаких серьёзных препятствий этому нет».
Источник: www.quantamagazine.org
