Математика не для всех

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

Часть 3 из 3

Классификация остаётся достижением создавших её математиков. Проект использовал Lean, Mathlib и около 1,2 млн строк из Qiuzhen-CFSG. В публикации формализации доступны итоговая теорема, инструкции проверки и промежуточные результаты. Работа над исправлениями продолжается со специалистами, включая Лайонса и Соломона. Заявленная формализация позволяет проверять условия и зависимости огромного доказательства как единое целое и использовать его части в дальнейшей математике.

Наши каналы
MAX · Telegram · Дзен

#ТеорияГрупп #Симметрия #Формализация #Доказательства

CFSG используют в алгебре, теории чисел, комбинаторике и математической физике. Monster действует как группа симметрий квантовой теории Френкеля, Леповского и Мёрмана, связанной через monstrous moonshine с модулярными функциями, обладающими особыми законами преобразования. В 2007 году Виттен предположил, что эта теория могла бы описывать гравитацию в двух пространственных и одном временном измерении. В этом предложении математика Monster связана с распределением квантовых состояний чёрных дыр по энергиям. Родственная umbral moonshine связывает другие конечные группы с особым классом функций, мок-модулярными формами, и мотивирует исследования связей с теорией струн. Эти физические предположения не являются результатами формализации CFSG.

Часть 2 из 3

Команда сообщает о 34 существенных отступлениях от опубликованных аргументов. Подозрительные места исследовали отдельно, поскольку ошибиться мог и агент. В квазитонких томах Ашбахера и Смита нашлось ложное равенство. Для матричной группы SL₂(5) над полем из пяти элементов одна величина равнялась 1 вместо требуемых 2. Замена равенства неравенством вернула случаи, ранее исключённые в последующих рассуждениях. Команда расширила более ранний аргумент и перераспределила случаи, сохранив конечный вывод. Находки обсуждали со специалистами и собирали в список исправлений.

Самое серьёзное препятствие касалось теоремы о несбалансированных группах, UGT. Предположим, есть конечная простая группа вне списка CFSG, и выберем такую группу наименьшего порядка. Меньшие простые группы, возникающие в её собственных подгруппах, уже классифицированы. При этой предпосылке UGT позволяет распознать всю группу, когда в централизаторе инволюции возникает определённая структура нечётного порядка.

В аргументе Уолтера 1986 года предполагалось, что определённая операция сохраняет некоторое семейство простых групп. Контрпример использует группы PSL₂(q) и PGL₂(q), построенные из матриц 2 × 2 над полем с q элементами. Группа PSL₂(49) входит в семейство. Нетождественная симметрия поля из 49 элементов, которая сохраняет арифметику и при двукратном применении возвращает каждый элемент на место, задаёт полевую инволюцию группы. Это автоморфизм, то есть взаимно однозначное преобразование группы в себя, сохраняющее умножение, а не элемент самой группы. Неподвижные при нём элементы образуют централизатор PGL₂(7). На следующем шаге из централизатора выделяют простую подгруппу PSL₂(7). Она исключена из семейства, поскольку 7 = 2³ − 1 является простым числом Мерсенна. Значит, операция вывела нас за пределы семейства. Контрпример опровергает утверждение о замкнутости, но не UGT и не заключение соответствующего предложения Уолтера.

Смена доказательства UGT могла потребовать большого объёма новой формализации. После консультаций с Лайонсом и Соломоном AxiomProver построил альтернативный аргумент на основе теории Соломона 1976 года. В сопровождающей статье об UGT команда представляет новую теорему 2.3. При специальных гипотезах этого этапа CFSG сравнения подгрупп через связывающие их инволюции сохраняют соответствующую простую группу. Вместе с редукциями Гилмана и Соломона и теоремами распознавания Фута и Харриса это даёт нужную форму UGT для простых групп. Позднее математики Axiom нашли в рамках первого поколения более короткий путь без теоремы 2.3. Длинный путь оставили как формализованный аргумент, дающий дополнительный результат.

Для завершения CFSG нужно доказать существование и простоту групп списка при допустимых параметрах, а также попадание в список любой конечной простой группы. Все части должны соединиться без необоснованных предпосылок. Люди проверяют, что определения и итоговая формулировка действительно выражают классификацию; Lean проверяет формальные выводы. Замена аргумента UGT показывает, почему доказательство той же теоремы не обязано буквально повторять исторический путь.

Программа Горенстейна 1972 года разбила работу на 16 этапов. Объявление о завершении в 1983 году оказалось преждевременным. Квазитонкий случай Ашбахер и Смит закрыли в 2004 году на 1221 странице; ещё один пробел, связанный с M₂₂, устранили в 2008 году. Второе поколение доказательства систематизирует материал, но ещё не завершено. Axiom выбрала первое поколение, хотя карту зависимостей строила с опорой на тома второго.

Проект опирался на прежние формализации и карту из 108 этапов и примерно 380 задач. Агенты распределяли леммы и делегировали недостающие предпосылки; математики разбирали препятствия, инженеры поддерживали систему. Lean может принять вывод из дополнительной гипотезы, которая ещё не доказана, оставив исходную задачу открытой. Так было с одним вариантом теоремы о сигнальных функторах, объясняющей согласование локальных подгрупп. Из-за недоказанных предпосылок пришлось удалить десятки тысяч строк и пересмотреть план.

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

Для Monster команда сообщает о формализации построения через алгебру Грисса размерности 196 884, доказательства простоты и распознавания по структурным признакам. Эти три задачи требуют отдельных аргументов.

Классификация конечных простых групп и проверка её доказательства (часть 1 из 3)

Как проверить доказательство, распределённое по сотням статей? Axiom Math объявила о первой полной формализации классификации конечных простых групп, CFSG, в Lean. По данным команды, за 24 дня десятки ИИ-агентов вместе с математиками и инженерами подготовили около 43,1 млн строк кода. Историческое доказательство занимает примерно 15 тысяч страниц в более чем 500 статьях около ста математиков. Lean проверяет выводы из точно записанных определений и гипотез.

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

Конечные группы разлагаются на неразложимые факторы, простые группы, в смысле теоремы Жордана и Гёльдера. CFSG перечисляет все возможные простые факторы.

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

Тем не менее CFSG даёт полный список простых групп. В него входят циклические группы простого порядка, то есть с простым числом элементов, знакопеременные группы чётных перестановок пяти и более символов, простые группы лиева типа над конечными полями с допустимыми параметрами, составляющие 16 бесконечных семейств, и 26 отдельных спорадических групп.

Крупнейшая спорадическая группа Monster имеет примерно 8 × 10⁵³ элементов. Главная трудность CFSG состоит в доказательстве полноты списка. Построить даже такую группу для этого недостаточно.

В 1954 году Брауэр предложил распознавать простые группы через инволюции и их централизаторы. Инволюция является нетождественной симметрией, двукратное применение которой возвращает исходное состояние. В её централизатор входят элементы, для которых умножение на неё слева и справа даёт один результат. В 1963 году Фейт и Томпсон доказали, что любая конечная простая группа с некоммутативным умножением имеет чётный порядок. По теореме Коши она содержит инволюцию. Поэтому стратегия применима ко всему этому классу. Их 255-страничное доказательство заняло целый выпуск журнала.

Тихо Браге и числа, изменившие астрономию

Как наблюдения без телескопа помогли открыть математические законы движения планет? В истории Тихо Браге ответ начинается с инструментов, измерений и возможности годами работать в собственной обсерватории.

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

Браге открыл сверхновую в созвездии Кассиопеи. Его наблюдения новой звезды и комет показали, что эти объекты находятся дальше Луны. Это различие было принципиальным. Если небесная область за Луной неизменна, появление там новой звезды противоречит такой картине. Чтобы поставить её под сомнение, требовалось не просто заметить необычный объект, но и установить, что он принадлежит именно этой области.

За научной работой стояла зависимость от покровителя. После смерти Фредерика II его наследник сократил финансирование Ураниборга. Обсерваторию пришлось закрыть, а Браге впоследствии перебрался в Прагу. Там его ассистентом стал молодой Иоганн Кеплер, которому предстояло извлечь из накопленных измерений законы движения планет.

Биографию Браге часто запоминают по другому эпизоду. В 1566 году он поссорился с троюродным братом Мандерупом Парсбергом. По одной версии, они выясняли, кто лучше знает математику, по другой, спорили о правильности формулы. Через три дня состоялась дуэль на шпагах, на которой Браге потерял кончик носа. После этого он носил протез. Причина ссоры остаётся предметом разных версий.

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

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

Научное наследие Браге имеет гораздо более определённое содержание. Его точные измерения стали основой, из которой Кеплер вывел законы движения планет. Позднее Ньютон дал им физическое объяснение. Здесь различаются три вклада, последовательно связанные друг с другом. Браге обеспечил наблюдательные данные, Кеплер нашёл математические закономерности, Ньютон объяснил движение. Эта линия развития науки ведёт к расчётам спутниковых орбит, космических миссий и навигации, но собственным достижением Браге были прежде всего измерения, которым должна была соответствовать теория.

Наши каналы
MAX · Telegram · Дзен

#ИсторияМатематики #Астрономия #Кеплер #НаучныеИзмерения