Небольшое сообщество математиков использует программу Lean для создания новой цифровой базы. Они надеются, что она обеспечит будущее их научной области.
Ежедневно десятки математиков-единомышленников встречаются в чате Zulip, чтобы работать, как они считают, над созданием будущего их научной области.
Все они – поклонники программы Lean. Это инструмент интерактивного доказательства теорем, который, в принципе, способен помогать математикам писать доказательства. Однако для этого математики должны вручную ввести математические правила в базу программы, приведя собранные за тысячи лет знания к виду, понятному компьютеру.
Для многих участников проекта его преимущества практически не требуют объяснений.
«На фундаментальном уровне очевидно, что после оцифровки чего-либо его можно использовать новыми способами», — сказал Кевин Баззард из Имперского колледжа Лондона. «И мы собираемся оцифровать математику, в результате чего она станет лучше».
Оцифровка математики – мечта давняя. Ожидаемые преимущества этого простираются от банальных – проверка домашней работы учащихся при помощи компьютеров – до исключительных: использование искусственного интеллекта для совершения новых математических открытий и поиска новых решений старых задач. Математики считают, что автоматические доказыватели теорем также смогут рецензировать статьи, поступающие в журналы, находить ошибки, которые иногда пропускают люди-рецензенты, а также заниматься утомительной технической работой по заполнению доказательства всеми необходимыми деталями.
Но сначала математикам, собирающиеся в чате, нужно оснастить Lean знаниями в рамках школьной математики, и пока эта задача выполнена только наполовину. В ближайшее время Lean вряд ли сможет решать открытые задачи, но работающие над базой люди почти уверены, что всего через несколько лет программа хотя бы научиться понимать вопросы уровня экзаменов в старших классах.
Да и кто знает? Участвующие в проекте математики не всегда точно представляют себе, для чего может пригодиться цифровая математика.
«Мы не знаем точно, куда движемся», — сказал Себастиен Гёзель из Реннского университета.
Вы планируете, Lean работает
Летом группа опытных пользователей Lean проводила онлайн-семинар “Lean для любопытных математиков“. На первом занятии Скотт Моррисон из Сиднейского университета показал, как можно записать доказательство при помощи программы.
Начал он с записи утверждения, которое хотел доказать, в понятных Lean терминах. На человеческом языке оно означало «существует бесконечное число простых чисел». Это утверждение можно доказать несколькими способами, однако Моррисон хотел использовать немного изменённый вариант первого из обнаруженных доказательств за авторством Евклида от 300 года до н.э. В доказательстве все известные простые числа перемножаются, а потом после добавления 1 получается новое простое число (либо само произведение, либо один из его делителей будет простым). Выбор Моррисона был связан одним из базовых правил использования Lean: пользователь должен сам придумать основную идею доказательства.
«За первое предположение отвечаете вы», — сказал Моррисон в интервью.
Введя утверждение и выбрав стратегию, Моррисон за несколько минут обрисовал структуру доказательства. Он определил последовательность промежуточных шагов, каждый из которых было относительно легко доказать. И хотя Lean не может предложить общую стратегию доказательства, она может помочь исполнять мелкие конкретные шаги. Разбивая доказательство на доступные подзадачи, Моррисон чем-то напоминал шефа, дающего обычным поварам команды порезать лук или вскипятить воду. «Именно в этот момент надеешься, что Lean возьмёт управление на себя и начнёт тебе помогать», — сказал Моррисон.
Lean выполняет промежуточные задачи при помощи автоматизированных процессов под названием «тактики». Это что-то вроде коротких алгоритмов, предназначенных для выполнения очень конкретных задач.
Работая с доказательством, Моррисон запустил тактику под названием «библиотечный поиск». Она прочесала базу математических данных программы и вернула несколько теорем, которые, по её мнению, могли бы заполнить пробелы в конкретном разделе доказательства. Разные тактики выполняют разные математические задачи. Одна из них, linarith, может взять набор неравенств для, допустим, двух вещественных чисел, и подтвердить истинность нового неравенства, куда входит третье число: если a равно 2, а b больше a, тогда 3a + 4b больше 12. Другая выполняет большую часть работы с базовыми алгебраическими правилами типа ассоциативности.
«Два года назад в Lean ассоциативность приходилось применять вручную, — сказала Амелия Ливингстон, изучающая математику студентка Имперского колледжа Лондона, обучающаяся работе с Lean у Баззарда. – А потом кто-то написал тактику, которая делает это за вас. Я каждый раз радуюсь, когда её использую».
В целом на завершение доказательства Евклида у Моррисона ушло 20 минут. Кое-где он дописывал детали сам; иногда за него это делали тактики. После каждого шага Lean проверяла непротиворечивость доказательства согласно встроенным логическим правилам, записанным на формальном языке под названием теория зависимых типов.
«Это похоже на приложение для судоку. Если вы делаете неправильный ход, оно издаёт сигнал», — сказал Баззард. В итоге Lean подтвердила работоспособность доказательства Моррисона.
Это было очень увлекательное упражнение – как обычно бывает, когда технологии делают что-то вместо вас. Однако доказательство Евклида существует уже более 2000 лет. Интересующие сегодняшних математиков вопросы настолько сложны, что Lean пока даже не может понять вопросы, не говоря уже о том, чтобы помогать отвечать на них.
«Вероятно, пройдут десятилетия, до тех пор, пока этот инструмент будет помогать с исследованиями», — сказала Хезэр Макбет из Фордэмского университета, один из пользователей Lean.
Так что, перед тем, как математики смогут работать с Lean над действительно интересными им вопросами, им придётся добавить в программу больше математических правил. А это, на самом деле, задача довольно простая.
Анатомия программы для построения доказательств: программа Lean помогает математикам доказывать теоремы, проверяя работу и автоматизируя некоторые этапы доказательств.
1) Математик описывает базовую структуру доказательства, и записывает последовательность шагов в Lean.
2) В библиотеке математических программ mathlib есть набор тактик, выполняющих шаги этого доказательства. Математики продолжают вносить в mathlib новые данные. Доказанные теоремы добавляются в mathlib.
3) Алгоритм Kernel проверяет корректность доказательства по простым правилам.
*Осьминожка почему-то стала обозначением радостных эмоций в сообществе Lean.
«Чтобы Lean смогла что-то понимать, люди должны перевести учебники математики в вид, понятный программе», — сказал Моррисон.
К сожалению, простота задачи не означает, что её просто выполнить – учитывая, что значительная часть математики в учебниках не описана.
Разбросанные знания
Если вы не изучали высшую математику, эта область может показаться вам точной и хорошо описанной. Алгебра, дифференциальное счисление, математический анализ – всё следует из всего, и на все вопросы есть ответы, перечисленные в конце учебника.
Однако математика в школьной программе, программе колледжа и даже по большей части в университете – это исчезающее малая часть всех знаний. Большая их часть организована не так хорошо.
Существуют огромные и важные области математики, не описанные полностью. Они хранятся в головах небольшого числа людей, обучавшихся своей подобласти математики у людей, научившихся ей у тех, кто её изобрёл – то есть, они существуют на правах фольклора.
Есть и другие области, базовый материал которых записан, но он настолько сложный и длинный, что никто ещё не смог проверить его правильность. Вместо этого математики просто в него верят.
«Мы полагаемся на репутацию автора. Мы знаем, что он гений и дотошный парень, поэтому доказательство, скорее всего, верное», — сказал Патрик Мэссо из университета Париж-Сакле.
Это одна из причин привлекательности программ, помогающих доказывать теоремы. Перевод математики на понятный компьютеру язык заставляет математиков каталогизировать, наконец, свои знания и точно определить все объекты.
Ассия Мабуби из французского государственного института исследований в информатике и автоматике вспоминает первый раз, когда она осознала потенциал такой упорядоченной цифровой библиотеки: «Меня захватила возможность теоретического охвата всей математической литературы при помощи языка чистой логики, хранения всей математической библиотеки в компьютере, проверки и поиска данных в ней при помощи программ».
Lean – не первая программа, обладающая таким потенциалом. Первая из них, Automath, появилась ещё в 1960-х, а Coq, одна из самых популярных сегодня, вышла в 1989. Пользователи Coq формализовали большой объём математики на языке программы, однако эта работа велась децентрализовано и не была как следует организована. Математики работали только над интересовавшими их проектами, и определяли только те объекты, которые были нужны им для собственной работы, часто описывая их уникальными способами. В итоге библиотеки для Coq выглядят захламлёнными, будто план города, росшего естественным путём.
«Coq сегодня – это старичок, покрытый шрамами, — сказала Мабуби, активно работавшая с этой программой. – Его долгое время поддерживало много народу, и благодаря его долгой истории на сегодня его недостатки хорошо известны».
В 2013 году Леонардо де Мура, исследователь из Microsoft, запустил проект Lean. Его название [lean (англ.) – худой, экономный] отражает желание де Мура создать эффективную и не замусоренную программу. Он предполагал, что программа будет инструментом для проверки точности кода других программ, а не математики. Однако оказалось, что проверка правильности программы во многом схожа с проверкой доказательства.
«Мы создали Lean, потому что интересуемся разработкой программ, и между созданием математики и созданием кода есть аналогия», — сказал де Мура.
Хезэр Макбет из Фордэмского университета, один из пользователей Lean
На момент выхода Lean существовало достаточно много других вспомогательных программ, включая Coq, наиболее похожий на Lean. Логическая база обеих программ построена на теории зависимых типов. Однако Lean предлагает шанс начать всё заново.
Она быстро привлекла математиков. Они пользовались ею с таким энтузиазмом, что начали отнимать у де Муры всё свободное время своими вопросами о разработке из области математики. «Он немного задолбался руководить математиками и сказал – а почему бы вам, ребята, не сделать отдельный репозиторий?» – сказал Моррисон.
Математики создали эту библиотеку в 2017-м. Они назвали её mathlib и рьяно взялись за её наполнение мировыми математическими знаниями, создавая что-то вроде аналога Александрийской библиотеки в XXI веке. Математики создавали и закачивали фрагменты оцифрованной математики, постепенно создавая каталог для Lean. И поскольку mathlib была новой, они могли учиться на ограничениях прошлых систем вроде Coq, и тщательно следить за организацией материала.
«Идёт целенаправленная попытка создания монолитной математической библиотеки, все фрагменты которой будут работать друг с другом», — сказала Макбет.
Александрийская mathlib
На главной странице проекта mathlib есть графики, в реальном времени отражающие прогресс проекта. У проекта есть список лидеров, вкладывающих в него больше всех, отсортированный по количеству строк кода [на первом месте, кстати, российский математик Юрий Кудряшов / прим. перев.]. Также подсчитывается общее количество оцифрованных математических объектов: на начало октября там содержится 18 756 определений и 39 157 теорем.
Все эти ингредиенты математики могут смешивать для того, чтобы создавать математику внутри Lean. Пока что их ассортимент сильно ограничен, несмотря на вроде бы впечатляющие цифры. Там почти ничего нет из разделов комплексного анализа или дифференциальных уравнений – а это два базовых элемента многих областей высшей математики. Кроме того, программа знает ещё недостаточно для того, чтобы даже описать какую-либо из задач тысячелетия – математических проблем, определенных Математическим институтом Клэя в 2000 году как «важные классические задачи, решение которых не найдено вот уже в течение многих лет».
mathlib медленно, но верно наполняется. Работа идёт в духе совместного труда. В чате Zulip математики выбирают определения, требующие формализации, вызываются записывать их и обеспечивают оперативные отзывы о работе других.
«Любой математик-исследователь может изучить mathlib и составить список из 40 вещей, которых там нет, — сказала Макбет. – Поэтому он решает заполнить какой-либо из этих недочётов. И мгновенное удовольствие гарантируется – кто-нибудь прочтёт ваш труд и оставит комментарий о нём в течение 24 часов».
Многие дополнения получаются небольшими – как обнаружила Софи Морель из Лионской высшей нормальной школы во время онлайн-семинара «Lean для любопытных математиков». Организаторы конференции выдавали участникам относительно простые математические утверждения, которые нужно было доказывать в Lean в качестве практики. Работая с одним из них, Морель поняла, что её доказательство требует леммы – небольшого промежуточного результата – которой не оказалось в mathlib.
«Это была небольшая деталь из линейной алгебры, которой там, по каким-то причинам, ещё не было. Люди, наполняющие mathlib, пытаются объять всё, но нельзя же предусмотреть все варианты», — сказала Морель, вписавшая в базу нужную лемму на три строчки самостоятельно.
Другие вклады более весомы. Последний год Гёзель работал над определением гладкого многообразия для mathlib. Гладкие многообразия – это множества (такие, как прямые, окружности или поверхности шара), играющие фундаментальную роль в изучении геометрии и топологии. Они также часто играют важную роль в задачах из таких областей, как теория чисел и математический анализ. Большую часть математических исследований без них вести невозможно.
Однако гладкие многообразия могут скрываться под разными личинами – всё зависит от контекста. Они могут иметь конечное или бесконечное количество измерений, иметь границы или не иметь их, определяться над различными числовыми системами – на множестве вещественных, комплексных или p-адических чисел. Определить гладкое многообразие – всё равно, что определить любовь: вы её узнаете, когда встретите, но из любого строгого определения наверняка выпадут какие-то самые очевидные примеры этого явления.
«Определяя базовые вещи, вам не нужно делать какой-то выбор, — сказал Гёзель. – Но более сложные объекты можно формализовать 10-20 разными способами».
Гёзелю необходимо сохранять баланс конкретики и обобщений. «У меня было правило – я хотел иметь возможность определить 15 разных применений многообразий, — сказал он. – При этом я не хотел, чтобы определение было слишком общим, иначе с ним невозможно было бы работать».
Разработанное им определение умещается в 1600 строк кода – это довольно много для определения из mathlib, но, возможно, и не так уж много по сравнению со всеми математическими возможностями, открываемыми им программе Lean.
«Теперь, получив нужный язык, мы можем начать доказывать теоремы», — сказал он.
Поиски правильного определения объекта правильной степени общности – основное занятие математиков, наполняющих mathlib. Создатели библиотеки надеются определять объекты так, чтобы это было полезно сегодня, и одновременно достаточно гибко, чтобы эти объекты можно было использовать непредсказуемым сейчас образом.
«Подчёркивается необходимость того, чтобы всё было полезным для использования и в отдалённом будущем», — сказала Макбет.
Перфектоиды рождаются из практики
Но Lean не просто полезный инструмент – он даёт математикам шанс по-новому заняться своей работой. Макбет до сих пор вспоминает, как она впервые попробовала воспользоваться программой, помогающей писать доказательства. Это был 2019 год, а программой была Coq (хотя сейчас она перешла на Lean). Она не могла остановиться.
«В один из безумных выходных я 12 часов подряд работала с этой программой, — сказала она. – Это была реальная зависимость».
Другие математики сходным образом описывают свой опыт. Они говорят, что работа с Lean похожа на компьютерную игру – вплоть до тех же выбросов гормонов награды, из-за которых сложно отложить в сторону игровой контроллер. «Можно по 14 часов в день заниматься этим, не чувствуя усталости и находясь в приподнятом состоянии весь день, — сказал Ливингстон. – Постоянно получаешь положительную обратную связь».
Себастиен Гёзель
И всё же сообщество Lean понимает, что для многих математиков в их программе просто недостаточно уровней.
«Если оценить количественно процент формализованной математики, я бы сказал, что пока готово меньше одной тысячной процента», — сказал Кристиан Сегеди, программист из Google, работающий над ИИ-системами, которые, как он мечтает, смогут самостоятельно читать и формализовывать учебники математики.
Но математики увеличивают этот процент. Если сегодня в mathlib содержится большая часть материала, изучаемого второкурсниками университетов, то участники проекта надеются добавить оставшуюся программу за несколько лет – и это будет значительное достижение.
«За все 50 лет существования этих систем ещё никто не предлагал: давайте сядем, и организуем последовательную базу знаний математики, описывающую институтский материал, — сказал Баззард. – Мы создаём вещь, которая сможет понимать вопросы институтского экзамена – такого раньше не было».
Пройдут, вероятно, ещё десятилетия, перед тем, как наполнение mathlib будет соответствовать исследовательской библиотеке, однако пользователи Lean демонстрируют хотя бы теоретическую возможность создания такого каталога – и достижение этой цели зависит просто от занесения в базу всей математики в виде программного кода.
С этой целью в прошлом году Баззард, Массо и Йохан Коммелин из Фрайбургского университета в Германии реализовали проект, доказывающий состоятельность этой мечты. Они временно отложили постепенное наполнение базы институтским материалом и перешли к передовым областям. Их целью было определить одну из величайших инноваций математики XXI века – такой объект, как «перфектоидное пространство», разработанный за последние десять лет Петером Шольце из Боннского университета. В 2018 году он получил за свою работу филдсовскую премию – величайшую награду в математике.
Баззард, Массо и Коммелин хотели продемонстрировать, что, хотя бы в принципе, Lean может работать с математикой, которая реально интересна математикам. «Они взяли нечто очень сложное и новое, и показали, что с этими объектами можно работать при помощи программы, помогающей писать доказательства», — сказала Мабуби.
Кевин Баззард
Чтобы определить перфектоидное пространство, трём математикам потребовалось скомбинировать более 3000 определений математических объектов и 30 000 связей между ними. Определения протянулись через множество областей математики, от алгебры до топологии и геометрии. Их объединение в одном определении стало яркой демонстрацией роста сложности математики со временем – и то, почему так важно правильно заложить основы mathlib.
«Многие области передовой математики требуют от вас знаний всех видов математики, которые преподают студентам», — сказала Макбет.
Троице удалось определить перфектоидное пространство, однако пока что математики мало что могут с ним сделать. В Lean требуется внести ещё много математических определений, пока программа сможет хотя бы сформулировать те сложные вопросы, в которых возникают эти перфектоидные пространства.
«Довольно глупо, что Lean знает, что такое перфектоидное пространство, но не знает комплексного анализа», — сказал Массо.
Баззард соглашается с ним, называя формализацию перфектоидного пространства «уловкой» – трюком, который новые технологии иногда показывают для демонстрации своей полезности. И на этот раз трюк сработал.
«Не нужно думать, что благодаря нашей работе все математики на Земле начали использовать программы, помогающие писать доказательства, — сказал Массо, — но я думаю, что многие из них заметили такую возможность и начали задавать вопросы».
Пройдёт ещё много времени до тех пор, пока Lean сможет стать реальной частью математических исследований. Однако это не значит, что сегодня программа является картинкой из научной фантастики. Математики, занимающиеся её разработкой, сравнивают свою работу с прокладкой первых железнодорожных путей – необходимым началом важного предприятия, даже если они сами так и не смогут прокатиться по этой дороге.
«Это будет такая крутая вещь, что она стоит сегодняшних трудов, — сказала Макбет. – Я вкладываю в неё своё время сегодня с тем, чтобы кто-нибудь в будущем смог получить такой потрясающий опыт от работы с ней».
