Сенсация: гипотеза Коллатца опровергнута. Рамана Кумар доказал её отрицание, Lean проверил доказательство, а Nanoda перепроверил. Но доказательство неверно: оно опиралось на баг в ядре Lean, и Nanoda ошибку тоже пропустил. Автор не злорадствует: soundness-баги находили в Isabelle и других системах, завтра может всплыть новый.
Гипотеза простая: чётное N делим на 2, нечётное заменяем на 3N+1. Коллатц считал, что процесс всегда дойдёт до 1. Перебор не нашёл ни одного контрпримера. Недавно выяснилось, что языковые модели неплохо находят контрпримеры к гипотезам, так что опровержение прогремело бы.
Полвека назад Робин Милнер придумал язык ML, чтобы через абстрактный тип защитить ядро proof assistant: правила вывода становятся API для создания теорем. Значит, proof objects не нужны. Но их всё равно хранят как «сертификат» для независимой проверки. Только ни один независимый проверщик не ловил ошибку, прошедшую через ядро. Nanoda в случае Collatz тоже купился. Таскать proof objects за собой — как возить запасную машину на прицепе: основная ломается, запасная не работает, а сломалась основная именно из-за тяжести прицепа.
Показательно: баг в Lean, по слухам, вызван вложенными индуктивными типами в ядре; в Rocq soundness ломал pattern matching с рекурсивными функциями в ядре. В теории множеств и простой теории типов аксиом нужно мало, а остальное получают честным трудом: индуктивные определения, рекурсивные структуры и функции, pattern matching. Рассел говорил: постулировать желаемое — преимущества воровства перед честным трудом. Полсон в 1980-х работал с Martin-Löf type theory и вручную строил комбинаторы для рекурсивных функций. Позже его цитировали как «Полсон расширил MLTT рекурсией» — никто не мог представить, что рекурсию можно вывести, а не постулировать.
Честный труд действительно похож на долбёжку камней. Рекурсивные типы получаются из монотонных операторов на множествах: наименьшая неподвижная точка даёт индукцию, наибольшая — коиндукцию. В Isabelle рекурсивные типы данных обрабатываются через bounded natural functors. Рекурсивные функции строятся через фундированное отношение и фундированную индукцию. Isabelle/HOL умеет общие рекурсивные определения с pattern matching и проверкой завершения — и всё это лежит снаружи ядра.
Ирония: proof objects якобы гарантируют корректность, а на деле наоборот. Если soundness важнее всего — берите HOL Light или HOL4. В Isabelle багов было больше, чем в них, но немного и точно меньше, чем у некоторых других систем.