Комментарии 7
Вопрос закрыт.
X doubt. Lean хорош, но пока нет гарантий, что где-то там не затесалось какого-нибудь бага, превращающего некорректное утверждение в истинное. плюс выглядит что из тех 49 миллионов многие леммы как будто лишние и полное доказательство должно уменьшаться в куда меньший объём.
Где гарантия, что аналогичного бага нет в мозгах людей, способных понять математику?
У lean очень маленькое и относительное простое ядро, которое верифицировано в том числе человеками, в этом большая уверенность в его корректности, насколько я понимаю.
Не совсем. Как минимум теперь там есть ещё альтернативное ядро проверок на Rust - человек это-то как раз и отсматривал. Сам компилятор Lean 4 нынче написан на Lean, однако это не помешало найти баг в верификации - гипотеза Коллаца несколько часов провисела доказанной потому что в Lean некорректно обрабатывались зав.типы (lean#14576). Имея 14, 49, или сколько угодно миллионов кода пруфов шанс найти псевдокорректный код все ещё остаётся просто исходя из статистики. Если не компилятор, то какие-нибудь тактики начнут подводить. На gh там почти семь сотен issue с тегом bug и шанс затронуть хотя бы что-то при таких размерах кодовой базы сильно ненулевой. Поэтому, пока человек не отсмотрит пруфы - слепо доверять этому не стоит. Ну и опять же - если посмотреть на граф зависимостей, то выглядит, что некоторые пруфы там совершенно лишние и часть кода просто делает дичь а ля 2+2=4 и можно сократить реальный пруф до куда более приемлимых размеров.
Сейчас меня тут наверное закидают гнилыми помидорами, но когда я читаю подобные новости, у меня всегда возникает вопрос, а что значит "доказали" ??? И вообще что такое "доказательство" ??? По традиции идущей ещё о Евклида, доказательство это рассуждение, позволяющее убедить собеседника в том, что доказываемое утверждение логически следует из принимаемых на веру аксиом. Скажите, кого и в чём может убедить рассуждение, требующее 15 тысяч страниц в 500 статьях, которого целиком не понимает ни один человек в мире ! Тут на Хабре уже было несколько интересных, хотя и спорных публикаций о природе конечного и бесконечного. Вот например https://habr.com/ru/articles/1041350/ . В частности про Есенина-Вольпина, который сомневался не только в бесконечном, но и в существовании просто достаточно больших чисел. Может пора пересмотреть и взгляд на природу математического доказательства ???
Здесь главным образом неочевиден статус доказываемого утверждения. Единого рассуждения растянутого на 15 тысяч страниц нет. Есть набор огромного количества утверждений, которые имеют смысл сами по себе, скажем, описание групп лиевого типа, но которые при этом суммируются в относительно компактный вывод, теорему о классификации простых конечных групп. Если же мы попытаемся зайти с другого конца: вот есть такая-то и такая-то алгебраическая конструкция, докажите, что ... - то иного способа доказать эту теорему в текущей формулировке, иначе кроме как через воспроизведение огромного корпуса частных результатов, мы не знаем.
Можно поставить вопрос иначе. А существует ли другая естественная классификация конечных простых групп, доказательство которой от силы займет семестровый спецкурс? Например, вместо групп лиевого типа будут группы, порожденные какими-нибудь гипотетическими расслоенными надбулевыми многогранниками, которые не только содержат все группы лиевого типа, но и спорадические группы, которые появляются как соответствующие конечному семейству целых чисел, по какой-то своей сложной причине, непокрываемых группами лиевого типа. Специальные конструкции придумать несложно, но они, понятно, неинтересны.
Классификационные теоремы - вещь непростая. Все конечные группы можно разделить на группы с четным и нечетным числом элементов. Доказательство элементарно и к группам отношение имеет постольку поскольку. А вот теорема о том, что любая некоммутативная простая группа должна иметь четное число элементов - уже совсем другое дело.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Агенты Axiom Math доказали полноту классификации конечных простых групп всего лишь в 41,3 млн. строчках кода Lean