Стремление к строгости в математике имеет долгую и неоднозначную историю — историю, из которой математики могут извлечь уроки сейчас, когда формализуют математику в программе Lean.  

В Древней Греции Евклид показал, что, если согласовать небольшой список предварительных принципов, или аксиом, то с помощью дедуктивного рассуждения можно выявить множество новых математических истин. Эти ранние доказательства выводили по законам логики, но в них нередко прятались скрытые предположения или обманчивая интуиция. В таких случаях небольшие пробелы в доказательстве могли остаться незамеченными; нельзя было с абсолютной уверенностью сказать, что оно верно.

В течение последних нескольких столетий математики стремились устранить эти пробелы. К началу 1900-х годов они определились с аксиомами, которые хотели использовать. Они также ввели различные логические системы и стандарты, стремясь ещё больше «формализовать» свои аргументы. Если каждое умозаключение явно, заключение истинно — независимо от того, насколько длинным и запутанным оно окажется.

Эти усилия по формализации укрепили доверие к математическому доказательству. Но они сделали гораздо больше. Стремление к формализации помогло учёным обнаружить новые связи между различными областями математики. Это научило нас, как сказал Дэвид Брессуд из колледжа Макалестер в Миннесоте, что «часто вы не знаете того, чего не знаете. И нужно быть скромными в этом отношении».

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

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

Сегодня учёные взялись за самый амбициозный проект формализации математики. Они стремятся переписать всю математику на языке программирования, известном как Lean, который затем сможет автоматически проверять их доказательства. Написание доказательства на Lean требует уймы времени и усилий, но к настоящему времени с ее помощью уже проверили более 260 000 теорем. Она способна заложить самый прочный фундамент для математики, какой только можно себе представить.

Как и в прошлые попытки формализации математики, Lean вызвал неоднозначную реакцию. Некоторые математики с нетерпением ждут возможности переложить утомительную работу по проверке доказательств на компьютеры и видят в Lean потенциально революционный новый способ изучения математики. Другие считают, что их время и ресурсы лучше потратить на что-то другое — или, что ещё хуже, что подход, ориентированный на Lean, исказит истинную ценность математики. Этот спор уже идёт на математических факультетах по всему миру: как совместить свободу, нужную для новых открытий, со строгостью, которая делает каждый шаг неоспоримым? 

Поиск пределов

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

В конце XVII века Исаак Ньютон и Готфрид Лейбниц независимо друг от друга изобрели математический анализ — метод, позволяющий понять, как быстро изменяется функция в данной точке. Но в неформальном смысле математический анализ существовал уже несколько столетий. По сути, Архимед занимался чем-то подобным дифференциальному и интегральному исчислению в III веке до нашей эры. Чтобы вычислить площадь круга, он сначала изучал площади фигур с прямыми сторонами, называемых многоугольниками. Используя многоугольники со всё большим количеством сторон, он оценивал предел: площадь круга. Ньютон и Лейбниц использовали аналогичный подход, применяя пределы для понимания изменений.

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

В течение 150 лет это не вызывало никаких проблем. Учёные просто научились определять, когда математический анализ можно эффективно использовать, а когда нет. Но в начале XIX века математики начали сталкиваться с явлениями — например, с бесконечными суммами и странными, извилистыми кривыми, — которые противоречили их интуитивным представлениям о возможном.

Эти открытия совпали с более широким поиском в искусстве и науке. Философы, художники, писатели и исследователи начали проверять границы того, что, как им казалось, они знали. «Интуиция вызывает подозрения», — сказала Альма Штейнгарт, историк из Колумбийского университета. «Существует ощущение, что интуиция может ввести вас в заблуждение». 

Чтобы осмыслить причудливые суммы и кривые из своих работ, Нильс Абель, Огюстен-Луи Коши и Карл Вейерштрасс поняли: надо вернуться к самым основам — к базовым определениям. Что такое функция? Что значит непрерывность функции? Что на самом деле происходит, когда вы складываете бесконечное количество объектов?

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

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

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

Тем не менее некоторые исследователи также с опаской относились к этой новой волне формализации. «Нелегко вновь обрести энтузиазм после того, как он был искусственно охлаждён мокрыми полотенцами ригористов», — писал физик и инженер Оливер Хевисайд в 1899 году.

Историк Йеспер Лютцен заметил, говоря про этот период: «Анализ приобрёл и строгость, и общность, но утратил элегантность и простоту и отдалился от интуиции. Многие математики сожалели об этой тенденции, но от неё было сложно избавиться».

Главное, ригористы (сторонники строгости) и их противники нашли компромисс. Точные определения Коши и Вейерштрасса остались в ходу, но появились и приёмы, позволявшие таким учёным, как Хевисайд, свободнее работать с бесконечностью и бесконечно малыми.

Иными словами, формализация не была их единственной целью. На самом деле, важная часть этой истории — это замысел, стоящий за формализацией. Задача была сравнительно узкой: Вейерштрасс и его коллеги занимались вполне конкретными вопросами о поведении функций и обратились к формализации, чтобы решить эти проблемы. Отсюда естественно выросли анализ, теория множеств и другие формальные системы.

«Научное здание не возводится подобно жилищу, в котором сначала прочно закладывают фундамент, а затем уже приступают к строительству и расширению помещений», — великий математик Давид Гильберт писал в 1905 году. Напротив, учёным следует сначала найти «удобные места для прогулок, и только потом, когда появятся признаки того, что рыхлый фундамент не способен выдержать расширение помещений, следует укреплять и упрочнять его».

«Это не слабость, — продолжил он, — а, наоборот, правильный и здоровый путь развития».

В конце концов, попытки формализации могут иметь совершенно разные последствия, если их цель выходит за рамки простого укрепления непрочного фундамента. 

Суровая Академия

Вполне возможно зайти слишком далеко в стремлении к ясности и строгости.

Рассмотрим одну из самых известных школ в математике, философию, выдвинутую тайным обществом математиков под названием Николя Бурбаки (официальное название: Association des collaborateurs et collaboratrices de Nicolas Bourbaki).

В середине 1930-х годов математика во Франции десятилетиями находилась в упадке. Страна потеряла целое поколение перспективных студентов и исследователей во время Первой мировой войны. Университеты преподавали математику разрозненно, по безнадёжно устаревшим учебникам. И вот несколько молодых математиков объединились, чтобы создать общество Бурбаки. Они начали со скромной цели: привести французскую учебную программу в соответствие с современными стандартами с помощью нового, более целостного учебника. Однако вскоре их амбиции значительно возросли. Сегодня общество Бурбаки (состав которого остаётся секретом) выпустило более 40 томов, охватывающих все мыслимые области математики. 

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

«Это очень формальный стиль, — сказал Лео Корри, историк из Тель-Авивского университета. — Очень строгий».

Философия Бурбаки быстро распространилась, оказав влияние на математику практически повсюду. «Она оказала огромное влияние, — сказал Патрик Массо из Парижского университета Сакле. — Наиболее успешные её части настолько прочно вошли в общепринятые математические знания и стиль, что трудно представить, как они выглядели раньше».

Предмет исследования стал гораздо более чётким, хотя и всё более абстрактным и сложным. «С педагогической точки зрения это не было блестящее решение», — писал Морис Машааль, многолетний редактор журнала Pour la Science и автор книги о Бурбаки. Но акцент группы на абстракции сформировал исследовательскую математику таким образом, который сложно оценить.

Некоторые математики высоко ценят подход Бурбаки. Массо утверждает, что благодаря абстракции и элегантности «вы вынуждены понимать, что на самом деле заставляет вещи работать, а что является просто шумом». С этой точки зрения, формализация принесла ясность.

Однако проект Бурбаки имел и непредвиденные последствия. Их терминология и стиль не всегда подходили для всех видов математики. Например, комбинаторика (наука о подсчете) и теория графов (наука о сетях) обычно очень конкретны и наглядны. Возможно, поэтому неудивительно, что на протяжении десятилетий они не были популярны в большинстве престижных учебных заведений США и некоторых частей Европы. Они смогли процветать только там, где влияние Бурбаки было ограничено, например, в Венгрии.

«Теория графов была трущобами топологии», — сказал Бела Боллобош из Кембриджского университета. «Эта атмосфера изменилась совсем недавно. Совсем недавно». 

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

«Существует ощущение, что это уменьшило культурное разнообразие математики», — сказал Аравинд Асок из Университета Южной Калифорнии. До Бурбаки, например, существовало множество версий алгебраической геометрии. Во Франции методы основывались на анализе, в то время как в Италии господствовал геометрический стиль.

Итальянская школа, отличавшаяся меньшей строгостью и большим количеством ошибок, быстро пришла в упадок по мере распространения влияния Бурбаки. Безусловно, алгебраическая геометрия стала более надёжной. Но, перекрыв другие пути возможного прогресса, Бурбаки создало новую проблему. «Я не хочу математики, в которой доминирует один стиль», — сказал Асок. «У математики есть культурная история, которую следует сохранить». 

Доказательства и обещания 

Несмотря на все усилия Бурбаки, Коши и Вейерштрасса, подлинно формальные доказательства всегда оставались предметом теории, а не практики. Некоторые математики теперь надеются, что компьютеры смогут это изменить.

Начиная с 1960-х годов исследователи разрабатывают компьютерные программы, называемые системами интерактивного доказательства. Используя такую систему, математик записывает каждую строку доказательства (включая каждое определение) на языке, понятном компьютеру, а затем система проверяет логику. Если хотя бы один шаг не вытекает из предыдущего — если не доказана каждая мелочь вплоть до того, что 1 + 1 = 2, — программа не примет доказательство.

Сейчас математики надеются формализовать всю математику с помощью системы интерактивного доказательства под названием Lean. Уже создана библиотека, содержащая более 120 000 определений, и проверено четверть миллиона теорем. Несколько математиков поддерживают эту базу данных, обновляя её и проверяя новые данные. (Некоторые из них занимаются этой работой полный рабочий день.) Они получили более 10 миллионов долларов финансирования, в основном от миллиардера-финансиста Алекса Герко. 

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

Но обычно на написание и проверку определений и доказательств в Lean уходят месяцы. В некоторых случаях формализация доказательства занимает всего несколько недель, в других — более года. Поэтому некоторые математики опасаются, что их время и ресурсы лучше было бы потратить на другие исследования. Они утверждают, что, хотя проверка доказательств важна, ручная проверка показала себя достаточно хорошо. Даже несмотря на то, что «в литературе много, очень много ошибок», — сказал Асок, — «мой опыт показывает, что математика удивительно устойчива». Другими словами, опасность того, что вся конструкция математики рухнет, невелика.

Тем не менее, использование Lean привело к появлению новых математических теорий. В 2019 году Петер Шольце вручную доказал теорему, ключевую для новой теории, которую он тогда разрабатывал. Но доказательство было чрезвычайно сложным, и ему было трудно определить, верно ли оно. Поэтому в конце 2020 года группа математиков во главе с Йоханом Коммеленом и Адамом Топазом приступила к формализации доказательства в Lean. Несколько месяцев спустя они подтвердили его правильность, что укрепило уверенность математиков в новой теории Шольце. В процессе они нашли более изящное доказательство и уточнили некоторые из первоначальных идей Шольце.

«Это заставляет вас правильно мыслить о математике», — сказал Кевин Баззард, математик из Имперского колледжа Лондона и один из главных сторонников Lean. «Это заставляет вас стать художником». Баззард провёл последний год, формализуя в Lean доказательство Великой теоремы Ферма, важного результата, доказательство которого, как известно, очень длинное и сложное. 

Более того, вложиться в Lean сейчас — хорошая ставка на будущее, где искусственный интеллект, несомненно, будет играть более значительную роль в математике. Чем активнее математики будут писать неформальные доказательства с помощью ИИ, тем важнее окажется проверять их в программах вроде Lean. Кроме того, ИИ уже помогает более эффективно писать доказательства в Lean.

Тем не менее широкое внедрение принципов Lean сопряжено с рисками. Может ли Lean, подобно методологии Бурбаки, незаметно изменить характер вопросов, которыми задаются математики? 

«Движущееся, изменчивое существо» 

В Lean практически нет места для концептуального, методологического или идеологического разнообразия.

Во-первых, каждое новое доказательство в Lean может использовать только формальные определения и теоремы, которые уже были проверены и сохранены в его библиотеке. Это означает, что эти определения и доказательства должны идеально сочетаться друг с другом. Это также означает, что обновление или изменение определения создаёт эффект домино: доказательства, написанные на старом определении, могут не работать с новым.

Это может стать проблемой. Математика — это «не фиксированное, конечное и формализованное явление», — говорит Стефани Дик из Университета Саймона Фрейзера. «Это постоянно движущееся, изменчивое существо, и условия его жизни постоянно меняются».

Поэтому прежние попытки оцифровать математику — например, проект  QED Manifesto 1994 года — быстро увязали в спорах о том, какие определения и фреймворки использовать. «В принципе, эта идея всем нравится, но на практике это кошмар», — сказала Дик. «Они расходятся во мнениях о том, на каком языке программирования писать. ... Существуют принципиальные разногласия по поводу того, возможен ли вообще подобный проект».

Чтобы избежать подобных разногласий, специальная группа пользователей Lean отвечает за то, какие определения включать в библиотеку и как их кодировать — примерно так же, как это делает Википедия, по словам Саймона ДеДео из Университета Карнеги-Меллона.

«Это сообщество стремится сделать всё возможное для своих членов», — сказала Эмили Риль, математик из Университета Джонса Хопкинса. Пока что это работает, и процесс в значительной степени демократичен. Но, по её словам, «плохо то, что в итоге принимается только одно решение, хотя во многих случаях нет единственно правильного решения. Одни будут довольны, а другие — недовольны».

Как подход Бурбаки годился для одних областей и не годился для других, так и Lean с его библиотекой определений одним разделам математики подходит лучше, другим — хуже. Например, они хорошо подходят для теории чисел и алгебраической геометрии. А вот для теории графов и теории категорий — не очень.

Это лишь один из способов сделать математику более однообразной. Дик отмечает, что прошлые технологии — даже выбор используемой нотации — незаметно изменили подход математиков к своей работе. Lean может побудить их сосредоточиться на разработке концепций, которые легче формализовать, даже если они этого не осознают. «Я обнаружила множество случаев, когда происходит нечто подобное, — сказала она, — когда «это на деле смещает фокус, интуицию и понимание от области математических задач к поведению этой системы».

Безусловно, в Lean есть много поводов для энтузиазма. Но сама Риль считает, что математикам следует использовать более одного типа систем интерактивного доказательства, а не полагаться исключительно на Lean. Однако она не уверена в практичности такого подхода, учитывая, сколько усилий требует формализация. 

О самокоррекции

На протяжении веков математики стремятся к большей строгости, сосредотачиваясь на проверке каждой строки доказательства. Но так было не всегда. Для Декарта в XVII веке строгость означала способность удерживать идею в голове и интуитивно понимать, почему она верна. В результате, по словам Акшая Венкатеша из Института перспективных исследований, прежние доказательства «обладали своего рода шероховатостью».

«Формально они не были элегантными», — сказал он. Но это «то, что человек может легко понять». Современные доказательства, конечно, элегантнее. Но они также более скользкие, их сложнее усвоить. Интересно, что Баззард использовал похожие формулировки, обсуждая свои надежды на то, как Lean повлияет на написание доказательств. «Я хочу, чтобы это доказательство было красивым», — сказал он. «Я хочу, чтобы оно легко воспринималось».

Эта тенденция отражает идею, которая сейчас воспринимается как само собой разумеющаяся: доказательство должно лежать в основе математики. «Нет сомнений в том, что концепция доказательства является фундаментальной частью математики», — сказал Венкатеш. Но «я думаю, что следует задаться вопросом, должно ли оно быть определяющей чертой математики».

Формализация в Lean продолжит ставить доказательство на первое место. Но это не единственное будущее, которое представляют себе математики. Исследователей подталкивают думать, что «единственный путь вперёд — это формализация научных работ в соответствии с принципами Lean», — сказал Асок. «Я бы сказал, что другой путь — это просто сделать шаг назад и перестать так много писать. Но это противоречит современным принципам».

Невозможно предсказать, как именно формализация в Lean повлияет на математику. История показывает, что математика склонна к самокоррекции, и будущее этой следующей волны формализации мы не можем вообразить.

Автор перевода @arielf

НЛО прилетело и оставило здесь промокод для читателей нашего блога:
-15% на заказ нового VDS — HABRFIRSTVDS.

Положение об акции