Интересное пишут про Lean, про который я тоже недавно рассуждал.

Вроде как нашли некую дырку в доказательстве: что-то связанное с кристальными когомологиями (хз, что это). Пробел обнаружили пока загоняли доказательство теоремы Ферма в Lean, но затем его заполнили при помощи других статей.

Уважаемый коллега делает из этого оптимистичный вывод:

Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.

Я не то чтобы готов спорить на эту тему,: прямо скажем, Lean я не владею. Но скепсис по этому поводу испытываю. Прежде всего, чтобы проверить в Lean некое рассуждение, нужно разжевать доказательство очень и очень подробно, со всеми логическими переходами и всеми возможными ссылками. Так обычно не пишут.

Ну то есть да, для данной конкретной теоремы, при наличии заметного числа волонтёров и\или финансирования, это возможно. Но я сомневаюсь, что такое разжёвывание реально для всей современной математики в добровольном порядке.

А вот гипотетическое принятие принципа «нет сертификата о проверке в Lean -- не опубликуем», выглядит хоть и возможно, но по итогу — ужасно. Реально, будет какой-то научно-бюрократический апокалипсис.

В общем без дополнительной #AI прослойки, которая сумеет «разжевать» текст, написанный современным математическим языком, пусть и под контролем автора, но думаю это вряд-ли станет популярно (и слава богу).

Глобально, я вот боюсь тут двух вещей.

Первая: потока правильных, отleanинынх статей, которые при этом не имеют никакого смысла. Просто доказать что-то новое — это дело не хитрое. Куда сложнее и интереснее придумать и доказать что-то интересное, действительно привносящее какое-то новое понимание.

Вторая: кто сторожит сторожей. Возможно тут всё известно (и я буду рад, если меня просветят в комментариях), но откуда у нас взялась абсолютная уверенность в достоверности компилятора и языка? (раз) И нет ли возможности надуть сам язык, подсовывая ему не вполне достоверную информацию (два)?

В общем «очень интересно, но ничего не понятно». Спасибо, кстати, тем кто обратил моё внимание на этот пост, прочитал с интересом. Думаю, что надо будет в скорости попробовать поиграться с lean. Любопытная штука.