Самое длинное доказательство

[Anton_Peplov]

Вот про Coq, кстати. Помнится, Воеводин говорил в интервью, что занялся основаниями математики именно с целью научить компьютеры проверять доказательства. Из чего можно сделать вывод, что существующие системы компьютерной проверки доказательств несовершенны. Кто-нибудь может объяснить в двух словах, что может и что не может проверить тот же Coq и другие пруверы? Желательно на пальцах, я с лямбда-исчислениями и тому подобными вещами не знакомый. Если на пальцах нельзя, то прошу список литературы, который надо освоить, чтобы это понять.

[Xaositect]

Не Воеводин, а Воеводский, наверное.

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

[Anton_Peplov]

Xaositect в сообщении #1072721 писал(а):

Не Воеводин, а Воеводский, наверное.

Мои извинения Владимиру Александровичу!

Xaositect в сообщении #1072721 писал(а):

способ мышления нужен не совсем тот, что у работающего математика

Ну и программисту нужен не совсем тот. И инженеру-телескопостроителю - тоже не совсем тот, что астроному. То есть получается, что перевод доказательств на язык автоматических пруверов - это просто отдельная область деятельности по обслуживанию науки. А насколько практика проверки доказательств в Coq распространена, интересно? Это единичные случаи или..? И сколько, интересно, человеко-часов нужно, чтобы перевести на Coq доказательство теоремы о модулярности?

[Someone]

Xaositect в сообщении #1072276 писал(а):

Фейта-Томпсона. http://ssr2.msr-inria.inria.fr/~jenkins/current/progress.html

А почему там куда ни ткнёшь, везде пишет Not Found?

[tolstopuz]

http://ssr.msr-inria.inria.fr/

[Xaositect]

Someone в сообщении #1072739 писал(а):

А почему там куда ни ткнёшь, везде пишет Not Found?

Извиняюсь, не проверил ссылку. Год назад все работало :)

Anton_Peplov в сообщении #1072732 писал(а):

То есть получается, что перевод доказательств на язык автоматических пруверов - это просто отдельная область деятельности по обслуживанию науки.

Это, наверное, правильный взгляд на эту область, по крайней мере в наше время. Но вот Воеводскому хочется самому проверять перед публикацией, а не после.