#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.

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

Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------

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

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

думаю, что весьма скоро компьютеры будут доказывать новые теоремы. Что породит множество интересных коллизий. Сейчас на работу берут математиков, которые смогли придумать что-то новое и интересное. А если они это делают, существенно опираясь на AI ? Как решать кто круче и кому давать гранты? Стоит ли бежать учить Lean? Или заниматься максимально далёкой от формализации математикой?

Представьте, что есть писатель, и примерно 98% текста генерится не человеком, а AI (и выходит не хуже, чем у писателей-людей. А то и лучше — промпты там лучше подобрал). Стоит ли такому человеку давать литературные премии? Такое уже есть ?(есть ли рассказы, написанные AI, которые очень хороши?)

Коллизии ограничиваются только вашей фантазией.

насколько я понимаю, китайский чатgpt - https://www.deepseek.com/ по всяким метрикам не хуже обычного. И работает в том числе из России и Китая. Вдруг кому надо.

Впрочем, как и обычный чатGPT он не смог мне найти уравнение параболы, касательной к двум данным прямым в данных точках.

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

UPD: победил параболу. deepseek стало искать наклонную параболу, но в какой-то момент решает квадратное уравнении, выбирает "for simplicity" один корень и получается двойная прямая в итоге. И признается, что не получилось. Если явно сказать, "выбери другой знак в шаге 8", то всё получается, и даже меня хвалит за подсказки.