Ну всё, я это сказал. «Один запрет за проблемами тысячелетия». Половина из вас уже тянется к минусу и слову на букву «к». И правильно тянется, потому что почти каждый, кто пишет такое, несёт чушь. Решили задачу тысячелетия или пробили столетнюю гипотезу, которую не смогли сотни умнейших математиков планеты до вас. Ну точно кранки!
Поэтому договоримся сразу. Первым делом не пафос, а признание:
Мы не решили ни одной проблемы тысячелетия. Гипотеза близнецов в нашем проекте — это
sorry, незакрытая дыра в доказательстве. Все «трудные» результаты либо висят на одной‑единственной аксиоме, которую мы честно принимаем извне, либо открыты.
Всё ещё здесь? Отлично. Тогда, может, вам будет интересно то, что осталось, когда пропал весь пафос. А осталось две вещи. Первая — одна невозможность, которая странным образом узнаётся за формой совершенно разных трудных задач. Вторая, и нам она была даже интереснее, — программа на Lean 4, которая ловит за руку каждый раз, когда мы пытаемся про эту невозможность соврать.
Про вторую и есть весь пост. Потому что идея это дёшево. Идею «за всем стоит одно» может выкрикнуть кто угодно. Дорого не дать себе в неё поверить. Итак — поехали!
Соблазн, который губит всех
Возьмите самый древний приём в математике бесконечный спуск Ферма. Натуральные числа нельзя уменьшать вечно: любая строго убывающая цепочка натуральных упрётся в дно. Банальность, которую знает первокурсник. Его использовали уже бесчисленное количество раз.
А теперь посмотрите на неё под нужным углом. Назовём бесконечную строго убывающую цепь «вечным двигателем», потому что она вечно черпает «работу» и никогда не останавливается. На натуральных числах его нет. И вдруг начинаешь видеть его повсюду:
конечное множество простых близнецов? — если раскрутить, получается бесконечный спуск, которого не бывает;
ноль дзета‑функции Римана не на критической прямой? — снова замаскированный вечный двигатель;
сингулярный каскад в Навье‑Стоксе — двигатель;
обрыв последовательности Коллатца, который никогда не падает на дно, — буквально вечное движение на ℕ.
И вот тут наступает опасный момент, когда сидишь в два часа ночи, смотришь на очередную задачу, и мозг услужливо шепчет: «ну ведь и здесь то же самое, правда?». Это самая сладкая ложь на свете — ложь, в которую хочется верить. Ещё чуть‑чуть, ещё одна натяжка, и «одна теория объясняет всё». Именно так рождаются кранки: не от глупости, а от того, что некому сказать «стоп, вот здесь ты перемудрил и обманул сам себя».
Мы решили, что «стоп» нам будет говорить компилятор. И работая с большими системами, в первую очередь, не нужно верить самому себе. Как же прекрасно, что есть такой замечательный язык Lean 4!
Детектор лжи на Lean 4
Весь проект держится на трёх цветах, и это не украшение:
🟢 — доказано машинно под стандартными аксиомами (
propext,Classical.choice,Quot.sound). Настоящее.🟡 — доказано условно на одну‑единственную нестандартную аксиому
step00FirstCause— «событие первопричины», которое я принимаю снаружи и честно в этом признаюсь.🔴 — открытый вход. Не «почти доказано», а честное «здесь дыра, вот её имя».
А сверху сидит скрипт VerifyAll.lean, который перечисляет все ~20 000 деклараций проекта и проверяет два жёстких инварианта. Его вывод буквально такой:
Declarations checked: 20055 Tainted by sorryAx: 1 ← ровно один sorry: twin_prime_conjecture Tainted by NON-STANDARD axioms: 49 ← все 49 тянутся к ОДНОЙ аксиоме ✔ INVARIANTS OK
Смысл простой: мы физически не можем протащить вторую аксиому или спрятать второй sorry — сборка развалится, инвариант не сойдётся. Если захотелось «дожать» задачу нечестным допущением, машина немедленно ставит на место. Честность здесь — не обещание в README, а свойство, которое проверяется на каждом коммите.
Знаете, что оказалось самым полезным? Не то, что машина подтверждала наши успехи. А то, что она регулярно отказывалась подтверждать то, во что мы уже успели поверить.
Что осталось после того, как машина всё отфильтровала
Когда убираешь всё, во что просто хотелось верить, остаётся не так уж мало настоящего, доказанного безусловно, зелёного:
Разделяющая линия. Двигатель запрещён на любом вполне‑фундированном носителе — но реализован на континууме ℝ: цепочка (1/2)ⁿ спускается вечно и никогда не касается нуля. Один и тот же запрет проводит точную границу между «дискретным, выводимым» и «континуумом».
Дискретный Гаусс‑Бонне. У графа спуска считается комбинаторная кривизна κ = 1 − outdeg, и её сумма по замкнутой области равна эйлеровой характеристике |V| − |E| = χ. Кривизна равна топологии — машинно.
Канон завершаемости. Тот же запрет доходит до классики: гидра Кирби‑Пэриса гарантированно умирает; «ω‑червь» завершается под трансфинитным ординальным рангом ω·a + b — значение при этом может взрываться сколь угодно, а ординал всё равно падает (это, кстати, и есть механизм теоремы Гудстейна); дерево Маркова x²+y²+z²=3xyz сводится к корню.
И совсем сбоку выпала честная жемчужина: простые Софи Жермен p ≡ 3 (mod 4) делят соответствующие числа Мерсенна — классика Эйлера‑Лагранжа, теперь проверенная машиной.
Самое честное, что умеет машина, — говорить «нельзя»
Вот интересный момент. Недавно нам пришла красивая мысль: раз континуум реализует вечный двигатель, давайте посадим наблюдателя на огромный центр‑близнец, инвертируем всех близнецов в отрезок (0,1) — и используем бесконечное дробление континуума, чтобы получить бесконечность близнецов «даром». Красиво же?
Красиво — и неверно. И мы это доказали против себя: вечный двигатель на ℝ спускается сквозь зазоры континуума (свидетель (1/2)ⁿ — целое число ровно один раз, при n = 0), а не сквозь ℕ‑скелет, где сидят близнецы. Инверсия в (0,1) — это переодевание гипотезы близнецов в топологические одежды, ровно с тем же содержанием и ни граммом больше. Континуум даёт двигатель даром именно потому, что не несёт ни одной целой точки.
То же и с физикой. Да, у проекта есть космологическое прочтение — стрела времени как необратимость спуска, гравитация как кривизна, чёрные дыры как колодцы. Но это явно объявлено переводом, а не физикой: в Lean нет ни метрики, ни гильбертова пространства. Мы специально проверяли границы — вывести космологическую постоянную Эйнштейна или квантовую механику из этой структуры нельзя, это категориальная ошибка, и она честно записана как «нельзя». Философия живёт строго поверх математики, с чертой между ними до последней строки.
А что же тогда «жёлтое»?
Единственная аксиома несёт ровно три границы — узел близнецов, закон Римана, гейт Навье‑Стокса. И покупает их трудные половины условно: если принять первопричину извне, то близнецов бесконечно, RH верна, у Навье‑Стокса нет сингулярного каскада. Подчёркиваю — это принятие, а не вывод. Вывести саму первопричину изнутри системы означало бы запустить тот самый запрещённый двигатель (и это теорема!.. она ниже). А остальные фронты — Янг‑Миллс, Ходж, P/NP — обходятся вообще без этой аксиомы. И это плюс: аксиома минимальна ровно потому, что нужна всего троим.
Вы действительно видите фрактал, самоподобие подтверждено машинно и закреплено теоремой. И да, он вывернут наизнанку. Доказательство началось именно с близнецов. Главная точка входа всего сущего — первопричина, которую невозможно обосновать.
Лучший результат в мире это 246. Что это? 246 это расстояние, внутри которого точно есть хотя бы два простых числа. Величайший математик нашего времени Теренс Тао доказал, что современная математика не может улучшить этот результат без новых идей. Как думаете, в чем же причина? Мы считаем, что это сравнимо с постройкой вечного двигателя. А потому главная, полностью зеленая, теорема в коде Lean звучит так:
ТЕОРЕМА: знать, что близнецы бесконечны, нельзя; но если незнание первопричины принять за истину — они бесконечны, и это строго. Узнать первопричину изнутри стоило бы вечного двигателя, которого нет, — поэтому она непознаваема; а конечный наблюдатель и близнеца‑то различает лишь целым чистым классом. Обе стены — одна природа; несущая грань замыкает круг: сама эта несовместимость плюс принятая причинная граница ⟹ близнецы бесконечны.
«Плюс принятая причинная граница» — это и есть намеренно принятая аксиома. Машина говорит, что изнутри к ней никак не подступиться. Это очень важно не путать. Можете зайти и убедиться сами.
В заключении
Если честно — была интересна не «теория всего», а эксперимент над самим собой: почему некоторые математически задачи так сложно решить? Да и вообще все началось с разбора Коллатца, а не с близнецов. И там тоже вылезло кое‑что интересное. Отсюда весь аппарат — цвета, верификатор, единственная аксиома, теоремы вида «а вот здесь нажать нельзя».
Мы независимые исследователи. Приоритет уже закреплён DOI на Zenodo, arXiv — в процессе (и да, ищем эндорсера в math.LO / cs.LO. Так что, если среди вас есть публикующиеся авторы, будем очень признательны). Но больше всего нужно другое: разбор. Где редукции честны, а где мы всё‑таки перемудрили и не заметили. Проект двуязычный (RU + EN), с прозой на каждый результат, так что копать можно с любого места.
Архив с DOI: zenodo.org/…/10.5281/zenodo.21198730
И самое искреннее: если вы найдёте место, где мы себе соврали, — это будет самый ценный комментарий под этим постом. Машина ловит на аксиомах. А на натяжках в редукциях можете поймать только вы.
