Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng
Я только что загрузил на arXiv нашу препринтную статью «Проект „Equational Theories“: продвижение масштабных совместных математических исследований». Это финальный отчёт по проекту «Equational Theories», который был представлен в этом блоге и также показан в этом последующем блоге.
Цель проекта
Цель проекта — выяснить, можно ли совместными усилиями провести крупномасштабное систематическое исследование математического пространства, а именно — графа импликаций между 4684 уравнительными законами магм.
Магма — это множество, снабжённое бинарной операцией (или, эквивалентно, таблицей умножения). Уравнительный закон — это уравнение, включающее эту операцию и несколько неопределённых переменных.
Примеры уравнительных законов:
* тривиальный закон;
* закон о синглтоне;
* коммутативный закон;
* закон центрального группоида;
* ассоциативный закон.
Эти законы можно изучить с помощью нашего инструмента «Equation Explorer».
Например, закон о синглтоне подразумевает все остальные, но коммутативный закон не подразумевает ассоциативный (поскольку существуют магмы, которые являются коммутативными, но не ассоциативными), и наоборот.
В общей сложности необходимо было рассмотреть множество импликаций такого типа. Большинство из них относительно просты и могут быть решены за несколько минут экспертом по алгебре уровня колледжа, но до этого проекта практически невозможно было сделать это таким образом, чтобы это можно было практически проверить.
Тем не менее мы смогли решить все импликации неформально за два месяца, а затем полностью формализовать их в Lean за последующие пять месяцев.
Этапы работы
Прогресс шёл разными волнами. Сначала огромные массивы импликаций могли быть решены с помощью очень простых методов, таких как перебор всех малых конечных магм, чтобы опровергнуть импликации; затем были задействованы автоматизированные средства доказательства теорем, такие как Vampire или Mace9, для обработки значительной части оставшихся.
Несколько уравнений имели существующую литературу, которая позволяла определить многие импликации, связанные с ними. Это оставило ядро, состоящее из чуть менее тысячи импликаций, которые не поддавались никаким «дешёвым» методам и занимали основную часть усилий проекта.
Как оказалось, все оставшиеся импликации были отрицательными; сложность заключалась в построении явных магм, которые подчинялись одному закону, но не другому. Для этого мы обнаружили ряд общих конструкций магм, которые были эффективны в этой задаче.
Линейные модели, в которых носитель был (коммутативным или некоммутативным) кольцом, а операция магмы имела вид для некоторых коэффициентов, оказались эффективными для разрешения многих случаев.
Мы обнаружили новый инвариант уравнительного закона, который мы называем «скручивающей полугруппой» этого закона, который также позволил нам построить дополнительные примеры магм, которые подчинялись одному закону, но не другому, начиная с базовой магмы, которая подчинялась обоим законам, беря декартово произведение этой магмы и затем «скручивая» операцию магмы с помощью определённых перестановок, предназначенных для сохранения, но не для .
Мы разработали теорию «расширений абелевых магм», аналогичную понятию абелева расширения группы, которая позволила нам гибко строить новые магмы из старых управляемым образом с помощью определённой «группы когомологий магмы», которые были поддающимися вычислению, и снова давали способы построения магм, которые подчинялись одному закону, но не другому.
Жадные методы, в которых одна бесконечная таблица умножения заполняется жадным образом (несколько похоже на наивное решение головоломки судоку), подчиняясь некоторым правилам, предназначенным для предотвращения столкновений и поддержания закона, а также некоторым начальным записям, предназначенным для обеспечения контрпримера к отдельному закону. Несмотря на кажущуюся сложность этого метода, его можно автоматизировать таким образом, чтобы опровергнуть многие оставшиеся импликации.
Были разработаны более умные способы использования автоматизированных средств доказательства теорем, такие как стратегическое добавление дополнительных аксиом в магму, чтобы сузить пространство поиска.
Однако даже после применения всех этих общих методов оставалось около дюжины особенно сложных импликаций, которые сопротивлялись даже этим более мощным методам. Потребовалось несколько специальных конструкций, чтобы понять поведение магм, подчиняющихся таким уравнениям, как E854, E906, E1323, E1516 и E1729, причём последнее потребовало месяцев усилий, чтобы наконец решить и затем формализовать.
Кроме одной (и её двойственной):
* Гипотеза 1. Подразумевает ли закон (E677) закон (E255) для конечных магм?
На этом этапе мы не смогли решить эту проблему даже после месяцев усилий.