В 2020 году мировая наука зафиксировала серию фундаментальных прорывов на стыке математики, физики и компьютерных наук, перевернувших представления исследователей о границах познания. Популяризаторы науки из Quanta Magazine представили подробный обзор этих открытий, включающий в себя решение легендарных многолетних загадок и глобальную цифровизацию самого математического языка. В центре сюжета оказались неожиданные связи между квантовой запутанностью, топологией узлов и возможностями искусственного интеллекта.
🌌 Квантовый допрос и решение проблемы остановки Тьюринга 0:05
В 1935 году Альберт Эйнштейн выразил глубокое беспокойство по поводу одной из ключевых идей квантовой физики — квантовой запутанности, назвав мгновенное взаимодействие частиц на огромных расстояниях «жутким дальнодействием». Всего год спустя, в 1936 году, Алан Тьюринг математически идентифицировал проблему, которую компьютеры никогда не смогут решить, — проблему остановки (halting problem). Она описывает ситуации, когда вычислительная машина, оперирующая входными и выходными данными, навсегда застревает в бесконечном цикле. Сегодня обычные пользователи регулярно видят бытовое проявление этой фундаментальной проблемы в виде «вращающегося колеса смерти» на зависших экранах компьютеров.
Долгое время казалось, что квантовая запутанность и теоретические ограничения вычислительной техники никак не связаны между собой. Однако в 2020 году они объединились в монументальном доказательстве, которое вызвало целую лавину решений открытых задач в физике, математике и теории вычислительных систем.
Соавтор этой революционной работы Генри Юэн (Henry Yuen) пояснил ключевые особенности исследуемой им области:
- Сфера науки: Исследование относится к теории сложности вычислений (Computational Complexity Theory), являющейся ответвлением теоретической компьютерной науки.
- Объект изучения: Вычислительная мощность модели так называемых интерактивных доказательств.
- Суть модели: Интерактивное доказательство представляет собой метод логического опроса, моделирующий вычисления как непрерывный обмен сообщениями между доказывающей (prover) и проверяющей (verifier) сторонами.
🕵️ Аналогия с полицейским допросом
Для объяснения сути открытия Генри Юэн привел наглядную аналогию с офицером полиции, который допрашивает двух подозреваемых. Следователь физически не может выйти из участка и лично проверить абсолютно каждую деталь в историях задержанных. Однако, задавая правильные, перекрестные вопросы и сталкивая показания субъектов лбами, он способен поймать их на лжи или, напротив, убедиться в том, что озвученные факты сходятся.
В классическом сценарии полицейский помещает подозреваемых в разные комнаты, чтобы исключить сговор. Но в квантовой модели субъекты обладают уникальной особенностью: они способны использовать общую квантовую запутанность, чтобы координировать свои ответы «жутким квантово-механическим способом». Основная задача следователя в таких условиях — все равно докопаться до истины.
Главный результат научной работы Юэна и его коллег заключается в том, что даже при наличии у допрашиваемых квантовой связи следователь может выстроить допрос таким образом, чтобы гарантированно установить истинность абсолютно любого математического утверждения в рамках колоссально сложного диапазона вопросов. Теоретически это доказывает, что гипотетический сверхмощный квантовый компьютер способен верифицировать ответы даже для принципиально нерешаемых задач, включая проблему остановки Тьюринга. По мнению Юэна, это открытие связывает воедино поразительные элементы из ранее казавшихся разрозненными областей науки и дает исследователям вдохновляющее ощущение открытия целого нового мира.
🪢 Как студентка за выходные распутала узел Конвея 2:54
Знаменитая задача выдающегося математика Джона Хортона Конвея (John Horton Conway) о свойствах его именного узла не поддавалась ученым на протяжении полувека. Вопрос исследователей заключался в том, является ли узел Конвея так называемым «срезом» (slice) более многомерного узла в четырехмерном пространстве — это топологическое свойство называют гладкой срезанностью. Для тысяч аналогичных математических узлов ответ был успешно найден, но именно структура Конвея упорно сопротивлялась любым попыткам анализа.
Лиза Пиччирилло (Lisa Piccirillo) впервые услышала об этой проблеме, будучи аспиранткой. По ее признанию, ей показалось совершенно нелепым, что современная топология с ее огромным арсеналом развитых инструментов не способна определить статус какого-то узла, имеющего всего 11 пересечений. Уже на следующий день, в воскресенье, она решила ради забавы протестировать собственный подход к этой задаче и затем на протяжении недели немного работала над ней по вечерам, чтобы понять, в чем заключается скрытая сложность.
📈 Неожиданное признание в Annals of Mathematics
Спустя неделю Пиччирилло пришла на плановую встречу со старшим топологом своего факультета Кэмероном Гордоном (Cameron Gordon) совершенно по другому учебному вопросу и вскользь упомянула о своих результатах. Профессор удивился и попросил ее показать выкладки. По мере того как Лиза переносила доказательство на доску, а Гордон задавал детальные уточняющие вопросы, ученый пришел в сильнейший восторг, осознав масштаб события.
В итоге доказательство Пиччирилло было официально опубликовано в престижнейшем научном журнале Annals of Mathematics. Саму исследовательницу столь бурный ажиотаж вокруг ее работы несколько удивил. По ее словам, когда математики доказывают какие-то положения, они обычно стремятся вывести максимально широкие общие утверждения, применимые ко всем объектам определенного класса. Она же доказала свойство лишь для одного конкретного узла, до которого ей, строго говоря, «нет дела». При этом Пиччирилло подчеркнула, что искренне увлечена изучением структуры трехмерных и четырехмерных пространств, а их детальное исследование в любом случае неизбежно заставляет ученых сталкиваться с теорией узлов.
💻 Оцифровка математики и искусственный интеллект Lean 4:50
Современная математика порой напоминает хаотичную мозаику: важнейшие и актуальные области исследований до сих пор не зафиксированы в едином строгом цифровом формате. Полная запись всех существующих теорем потребовала бы использования тысяч других сопутствующих определений, которые на сегодняшний день еще даже не сформулированы программно. Если представить создание своеобразной Александрийской библиотеки, содержащей в себе всю историю и сумму накопленных математических знаний в каталогизированном виде, это позволило бы запрограммировать искусственный интеллект для верификации сложнейших доказательств, а в будущем — для самостоятельного открытия новых законов.
Профессор Кевин Баззард (Kevin Buzzard) из Имперского колледжа Лондона активно занимается реализацией этого процесса цифровизации, обучая математическим концепциям специализированное программное обеспечение под названием Lean. Эта система непрерывно черпает знания из постоянно растущей библиотеки верифицированных доказательств и теорем.
Примерно три года назад Баззард разглядел в этом софте колоссальный потенциал и с тех пор прикладывает огромные усилия для его популяризации в академической среде. В рамках экспериментов его команда ввела в Lean концепции из очень сложной современной математики, и программа успешно с ними справилась. Это, по мнению Баззарда, доказывает, что софт потенциально способен освоить абсолютно любую математическую задачу.
🛠️ Преодоление человеческой неточности
Текущие масштабы и динамика развития системы Lean характеризуются следующими показателями:
- Объем базы данных: Математическая библиотека проекта уже насчитывает более 450 тысяч строк кода.
- Скорость расширения: База растет непрерывно — каждый день в систему через пулл-реквесты (pull requests) добавляется около 10 новых математических положений.
- Влияние на дисциплину: По образному выражению Кевина Баззарда, этот колоссальный массив данных буквально «медленно съедает математику», переводя ее на строгий машинный язык.
Однако на пути тотальной оцифровки стоит серьезный барьер: компьютеры разговаривают на специфическом, быстро меняющемся кодовом языке, который человеку необходимо долго осваивать. Проблема, как отмечает Баззард, заключается в том, что ведущие университеты по всему миру продолжают учить студентов сложным математическим идеям, но никто не обучает их языку программирования, понятному современным машинам.
Кроме того, Баззард выразил критическое мнение о текущем состоянии высшего образования. По его словам, реальная математика устроена совсем не так, как ее принято презентовать студентам. Профессора уверяют бакалавров, что математика — это абсолютно строгая теория, безупречно строящаяся на базовых аксиомах, но на практике реальная работа ученых-человек далека от этого идеала. Компьютеры чрезвычайно придирчивы, так как им жизненно необходимо точно знать, что происходит на каждом этапе вычислений, в то время как люди склонны к легкой небрежности и размытости в формулировках, которые софт категорически не принимает.
Процесс обучения машины приносит пользу и самому человеку, поскольку перед тем как объяснить что-то компьютеру, исследователь обязан понять предмет безупречно. По опыту Баззарда, когда ученый пытается перенести изначально сумбурное и грязное человеческое доказательство в Lean, в процессе отсечения неточностей на выходе всегда получается гораздо более изящный, выверенный и чистый аргумент. Глобальная цель проекта заключается в том, чтобы полностью перевести в Lean учебную программу бакалавриата по математике. Баззард прогнозирует, что через пару лет можно будет с полной уверенностью заявить, что искусственный интеллект стал в некотором смысле столь же умен в математике, как и дипломированный выпускник вуза.
