Математический прорыв десятилетия: от квантовой запутанности до цифровизации доказательств 0:05
За последние годы математика и компьютерные науки пережили ряд фундаментальных сдвигов, объединивших, казалось бы, несовместимые дисциплины. В центре внимания оказались прорывы в теории вычислительной сложности, решение десятилетних топологических загадок и амбициозный проект по переводу всей математики на «язык» машин. Об этих достижениях рассказывает журнал Quanta Magazine, подводя итоги наиболее значимых научных свершений недавнего времени.
🔐 Квантовая запутанность против проблемы остановки 0:05
В 1930-х годах Альберт Эйнштейн был обеспокоен феноменом квантовой запутанности, когда частицы мгновенно взаимодействуют на огромных расстояниях. Примерно в то же время Алан Тьюринг сформулировал «проблему остановки» — фундаментальное ограничение компьютеров, которые не всегда могут определить, завершится ли процесс или зациклится бесконечно. Долгое время эти области считались далекими друг от друга, однако недавнее исследование объединило их, запустив цепную реакцию решений в науке.
Генри Юэн, один из пяти соавторов прорывного доказательства, объясняет, что работа затрагивает теорию вычислительной сложности и так называемые интерактивные доказательства. Этот метод моделирует вычисления как обмен сообщениями между «доказывающим» и «верификатором» (проверяющим).
- Аналогия с полицией: Представьте офицера, допрашивающего двух подозреваемых в разных комнатах.
- Квантовый аспект: Подозреваемые могут использовать квантовую запутанность для координации ответов.
Результат исследования показал, что даже если подозреваемые обмениваются квантовой информацией, проверяющий может структурировать вопросы так, чтобы вычислить истинность любого математического утверждения. По мнению Юэна, это означает, что в теории супермощный квантовый компьютер способен верифицировать ответы на задачи, которые считались неразрешимыми, включая проблему Тьюринга.
🪢 Разгадка «узла Конвея» 3:00
На протяжении полувека математики не могли решить проблему «узла Конвея» — вопроса о том, является ли этот узел «срезом» узла в пространстве более высокой размерности. Хотя этот вопрос был решен для тысяч подобных объектов, узел Конвея оставался неприступным.
Лиза Пичарилло, будучи аспиранткой, решила эту задачу практически случайно, работая над ней в свободное время. Она признается, что для нее было странно, почему такая задача оставалась нерешенной, имея современные инструменты.
После того как Пичарилло представила свои расчеты старшему топологу Кэмерону Гордону, проверка подтвердила верность ее доказательства. Работа была опубликована в Annals of Mathematics. Сама автор отмечает: хотя она не является узким специалистом по теории узлов, изучение трехмерных и четырехмерных пространств неизбежно привело ее к этому результату.
🤖 Цифровизация математики: проект Lean 5:00
Математика часто представляет собой хаотичную мозаику, где многие области не описаны формально до конца. Кевин Базард из Имперского колледжа Лондона стремится изменить это, создавая своего рода «Библиотеку Александрии» современной математики с помощью программного обеспечения Lean.
- Принцип работы: Базард «обучает» компьютер математическим теоремам.
- Масштаб: Библиотека Lean уже насчитывает 450 000 строк кода и постоянно растет благодаря вкладу сообщества.
По словам Базарда, компьютеры требуют абсолютной точности, в отличие от людей, которые могут позволить себе быть слегка неточными. Процесс перевода доказательств в машинный код часто приводит к более элегантным и «гладким» формулировкам самой математики. Цель проекта — оцифровать весь курс бакалавриата, чтобы через несколько лет компьютер смог «мыслить» на уровне студента университета.
