В интернете появился репозиторий, опровергающий гипотезу Коллатца на Lean — без единой заглушки, то есть формально проверенный. Оказалось, что это не прорыв в математике, а эксплуатация ошибки в самом проверяющем ядре.

Леонардо де Моура, автор Lean, написал разбор случившегося. Киран Гопинатан свёл находку к короткому доказательству False — то есть в системе можно было доказать что угодно. Ошибка сидела в обработке вложенного индуктивного типа с фиктивными параметрами: параметры терялись во вспомогательном типе и не проверялись. Исправление выпустили примерно через час после минимального воспроизведения.

Отдельно автор объясняет, почему это нельзя закрыть запретами. Внешняя часть языка такой случай ловила, но это не спасает: подсунуть можно и заранее собранный файл, и напрямую построенный терм доказательства. Ядро обязано отвергать плохие объявления само.

Отдельный урок про независимую проверку: сторонний проверяющий на Rust это место проверял, но содержал собственную ошибку и пропускал специально сконструированное выражение. Две реализации помогают, только если обе свежие.

@prog_stuff