Annals of Formalized Mathematics – это уникальный специализированный журнал, который представляет собой площадку для публикации исследований в области формализации математических теорий, доказательств и алгоритмов с использованием современных компьютерных систем. Выпуск под номером один стал важным событием для международного сообщества математиков и специалистов по формальным методам, так как он собрал в себе ряд фундаментальных работ, расширяющих границы возможного в области формализации сложных математических объектов. Обзор этого выпуска открывает новые перспективы понимания и развития формальных методов в математике и информатике. Одной из ключевых тем первого тома является формализация производных категорий с помощью системы Lean 4 и библиотеки mathlib. Производные категории являются важным понятием в современной алгебраической геометрии и теории категорий в целом.
Работа Жоэля Риау демонстрирует, как класс локализации категории неограниченных коцепных комплексов по отношению к классу квазизоморфизмов можно формализовать и снабдить триангулированной структурой. Это достижение открывает путь к более глубокому и структурированному подходу к сложным категориям в математике, позволяя использовать возможности Lean 4 для строгости и автоматизации доказательств. Следующая статья посвящена формализации знаменитой теории дзета-функций Римана и более общих L-функций Дирихле, которые занимают центральное место в теории чисел. Доклад Дэвида Лоэффлера и Майкла Столла повествует о проекте, где формализуются основные свойства этих функций в mathlib, включая доказательство теоремы Дирихле о распределении простых чисел в арифметических прогрессиях, а также формулировку гипотезы Римана в формальной системе. Данная работа не только служит площадкой для проверки сложнейших математических рассуждений, но и открывает путь к дальнейшей проверке других гипотез и теорем, связанных с анализом и теорией чисел.
Важным и практическим аспектом формализации в математике является проверка эффективных алгоритмов, особенно тех, которые используют детерминированные методы замены случайных, так называемые дерминированные алгоритмы с использованием псевдослучайности. В статье Эмина Карайеля рассматривается, как сложные алгоритмы, зависящие от конструкций псевдослучайных объектов — таких как семейства хешей и расширительные графы, — могут быть формализованы и проверены в системе Isabelle. Созданная библиотека не только абстрагирует глубокие алгебраические и аналитические результаты, но и облегчает верификацию алгоритмов последних лет, включая пространство-оптимальные решения на основе сочетания множества приемов дерминизации. Уникальность данного подхода состоит в объединении теоретических знаний с практическими потребностями компьютерной науки, что позволяет создавать надежные и проверенные математические модели и алгоритмы. Важнейшим достижением тома стала полная формализация регулярного случая Великой теоремы Ферма, которая долгое время была символом математической загадки.
Алекс Бест, Кристофер Беркбек, Риккардо Браска и их коллеги подготовили грандиозное доказательство в Lean 4, включая формализацию леммы Куммера. Особенностью их подхода является отказ от современных методов через теорию классов полей, и использование набора теорем Гильберта 90-94, что делает доказательство более доступным для формализации. Такие работы важны не только с академической точки зрения, но и для практического превращения глубоких математических теорий в проверяемые компьютерными системами результаты. Ещё одним вкладом выпуска является формализация локальной компактности кольца аделей числового поля, выполненная Сальваторе Меркури. Адельное кольцо играет ключевую роль в современной теории чисел и алгебраической геометрии.
Показ локальной компактности этого объекта с помощью Lean 4 сопровождается введением новых типов, таких как дополнение числового поля в бесконечном месте и отдельные типы конечных и бесконечных аделей. Этот опыт демонстрирует возможности формальных систем в работе с топологическими свойствами алгебраических структур и служит базой для новых исследований. В целом первый том Annals of Formalized Mathematics отражает современные тенденции и вызовы в области формализации математики. Он показывает, как благодаря высоким вычислительным возможностям и совершенствованию формальных языков можно не просто проверять старые доказательства, но и создавать новые, которые были бы трудно воспроизводимы без помощи автоматизированных систем. Уникальность этого издания заключается в высоком уровне интеграции теоретических знаний и средств программирования, что способствует развитию строгой и надёжной математической базы для будущих исследований.
