Пример расчётного доказательства в Lean

Математики давно используют компьютеры в своей работе как инструменты для сложных вычислений и выполнения рутинных операций перебора. Например, в 1976 году методом компьютерного перебора была доказана теорема о четырёх красках. Это была первая крупная теорема, доказанная с помощью компьютера.

Теперь вспомогательный софт для доказательства теорем (proof assistant software) не просто для проверяет доказательства, но помогает выйти на принципиально новый уровень великого объединения разных математических разделов. Концепция «конденсированной математики» обещает принести новые идеи и связи между областями, начиная от геометрии и заканчивая теорией чисел. Это в своём роде «великое объединение» математики

Впрочем, обо всём по порядку.

Одним из самых талантливых современных математиков называют молодого немецкого теоретика чисел Петера Шольце. Он смело связывает математику с другими творческими занятиями, увлекается прогрессивным роком, выдвигает необычные теории и уже имеет опыт внедрения революционных концепций.

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

Конденсированная математика

Амбициозный план Петер Шольце разработал совместно с коллегой Дастином Клаузеном из Копенгагенского университета и изложил в серии лекций по аналитической геометрии (pdf) в в 2019 году в Боннском университете (Германия), где они работают.

По мнению коллег, если замысел Шольце будет реализован, то через 50 лет преподавание математики аспирантам может сильно отличаться от сегодняшнего. «Мне кажется, есть много областей математики, на которые повлияют его идеи», — говорит Эмили Риль, математик из Университета Джона Хопкинса в Балтиморе.

До сих пор большая часть «аналитической геометрии» Шольце опиралась на техническое доказательство, настолько сложное, что даже сами авторы не были уверены в его корректности. Но 5 июня 2021 года Шольце объявил в блоге о завершении работы по компьютерному доказательству!

Великое объединение

Решающим моментом конденсированной математики является переопределение понятия топологии, одного из краеугольных камней современной математики. Многие объекты, которые изучают математики, имеют топологию — эта структура определяет, какие части объекта расположены близко друг к другу, а какие нет. Топология даёт понятие формы, но более гибкое, чем в привычной геометрии: в топологии допустимо любое преобразование, которое не разрывает объект.

Топология играет важную роль не только в геометрии, но и в функциональном анализе, изучении функций. Функции обычно «живут» в пространствах с бесконечным числом измерений (например, волновые функции, которые являются основой квантовой механики). Это также важно для систем чисел, называемых p-адическими числами, которые имеют экзотическую, «фрактальную» топологию.

Примерно в 2018 году Шольце и Клаузен начали понимать, что традиционный подход к понятию топологии приводит к несовместимости этих трёх математических вселенных — геометрии, функционального анализа и p-адических чисел, но можно попробовать устранить эти пробелы.

Многие результаты в каждой из математических областей имеют аналоги в других областях, хотя на первый взгляд это совершенно разные понятия.

Но если определить топологию «правильным» образом, то аналогии между теориями окажутся примерами одной и той же «конденсированной математики», пишет Nature. Это своего рода «великое объединение» трёх областей.

Шольце и Клаузен уже нашли «конденсированные» доказательства ряда глубоких геометрических фактов и теперь могут доказать теоремы, которые ранее были неизвестны. Правда, они ещё не обнародовали эти данные.

Теорема

Суть поставленной задачи Шольце подробно изложил в декабре 2020 года. Он поставил задачу доказать очень теорему о множестве вещественных чисел, которое имеет топологию прямой линии. «Это как бы основополагающая теорема, которая позволяет вещественным числам войти в эту новую структуру», — объясняет Коммелин.

Работа по доказательству получила название Liquid Tensor Experiment, по имени любимой рок-группы математиков.

Вспомогательный софт для доказательства теорем

Вспомогательный софт для доказательства теорем (proof assistant software) используется уже десятилетиями. Если вкратце, то пользователь вводит в систему утверждения, которые дают машине определения математических понятий — объектов — на основе более простых объектов, о которых машина уже знает. Это утверждение может просто ссылаться на известные объекты. Затем программа ответит, является ли данный факт «очевидно» истинным или ложным, основываясь на своих текущих знаниях.

Если ответ не очевиден, пользователь должен ввести больше деталей. Таким образом, вспомогательный софт заставляет пользователя излагать логику своих аргументов в строгой форме, в том числе заполнять все проблемы — простые шаги, которые математики сознательно или бессознательно пропускали.

Из самых известных систем такого типа — Isabelle, Lean, Mizar и Coq, см. более полный список.

В данном случае математики решили использовать программу Lean — и кодирование всех необходимых понятий и объектов заняло полгода. Естественно, Шольце работал не в одиночку. Ему помогала группа добровольцев под руководством Йохана Коммелина, математика из Фрайбургского университета в Германии.

Числовая прямая, показано положение на ней чисел $$, $$ и $$

По словам одного из помощников Йохана Коммелина, Lean-версия доказательства Шольце включат десятки тысяч строк кода — она примерно в 100 раз больше, чем оригинальная версия: «Если вы просто посмотрите на код Lean, вам будет очень трудно понять доказательство, особенно в его нынешнем виде». Но исследователи говорят, что потраченные усилия, заставить доказательство сработало в программе, помогли им лучше понять саму теорему и доказательство.

Вообще, кодирование теоремы в программе для автоматического доказательства помогает понять, что построение теоремы и её доказательство — по сути одно и то же.

По мнению некоторых исследователей, компьютерные программы для автоматического доказательства теорем в ближайшее время будут более широко использоваться в университетах. Возможно, компьютеры смогут указать на какие-то последствия или выводы известных теорем, которые математики не заметили. Хотя сам Шольце говорит, что ему лично не нужны такие программы в «творческой работе математика».

Так или иначе, но данный случай доказывает, что программы для доказательства теорем действительно способны помочь в особо тяжёлых случаях. Похоже, компьютер способен одновременно оперировать с большим количеством объектов, чем оперативная память человека. После того, как в течение полугода, в программу вводили объекты, она всё-таки смогла выстроить логическую цепь и подтвердить доказательство.

Выдача Lean по доказательству теоремы Шольце и Клаузена

«У таких программ есть свои поклонники, но это первый случай, когда они сыграли важную роль во фронтире математической науки, — говорит Кевин Баззард, математик из Имперского колледжа Лондона, который участвовал в совместном проекте по проверке результатов Шольце и Клаузена. — До сих пор в воздухе висел главный вопрос: справятся ли они со сложной математикой? Мы показали, что справятся».

Специалисты говорят, что полгода кодирования в Lean — даже небольшой срок для такой монументальной задачи. Софт для доказательства теорем доказал, что за разумный промежуток времени может формально проверить сложнейшее оригинальное исследование.

---

VPS серверы от Маклауд быстрые и безопасные.

Зарегистрируйтесь по ссылке выше или кликнув на баннер и получите 10% скидку на первый месяц аренды сервера любой конфигурации!