Математика · Вернуться на главную
В первой лекции курса «Цветные метабиблиотеки. Разум пространства» (лаборатория им. П. Л. Чебышева СПбГУ, 02.09.2016, YouTube) Р. В. Михайлов описывает «хищную спектралку»: взять лист E² цветной метабиблиотеки и дать ему «съедать себя как можно быстрее, ограничиваясь только цветом». Для 3-кручения гомотопических групп πₙ(S²) лекция предсказывает, что в π₄₈ его нет, а во всех πₙ при 49 ≤ n ≤ 149 оно есть. В нашем пересчёте метабиблиотека — это набор допустимых слов из букв λᵢ и μᵢ лямбда-алгебры по модулю 3 из статьи Иванова, Михайлова и Ву, а цвет слова — число букв μ в нём.
Лист E² с цветами мы посчитали до π₁₅₀. Цвет оказался числом бокштейнов (Q-весом) в нестабильном Ext; это проверено поклеточно прямым счётом лямбда-алгебры до π₇₅ и выборочно до π₈₅. Хищное правило с цветом +1 совпадает с таблицей Тоды при всех n ≤ 48, включая π₄₄ = 0, и воспроизводит предсказания лекции. После π₄₈ оно расходится с таблицей Тоды 2003 года в девятнадцати группах, от π₄₉ до π₈₀, и везде оставляет больше классов.
Для пяти первых расхождений — π₄₉, π₅₀, π₅₁, π₅₉ и π₆₀ — результат не держится на
доверии к нашей программе. Счёт пишет сертификаты; их проверяет проверялка,
написанная заново и не использующая код, которым считался E²; а Lean 4 — третья
независимая реализация той же алгебры — доказывает число выживших классов как
теорему вычислением (native_decide, то есть с доверием к компилятору Lean).
Чего это не покрывает: значения Тоды цитируются, а не проверяются, а само
правило — наше прочтение лекции.
Всё остальное — сравнение по каждой группе, классы E², дифференциалы, метод и данные — на сайте пересчёта: Цветная метабиблиотека: пересчёт.