2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 18:25 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 19:01 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Не Воеводин, а Воеводский, наверное.

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

 Профиль  
                  
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 19:54 
Заслуженный участник
Аватара пользователя


20/08/14
6871
Xaositect в сообщении #1072721 писал(а):
Не Воеводин, а Воеводский, наверное.

Мои извинения Владимиру Александровичу!
Xaositect в сообщении #1072721 писал(а):
способ мышления нужен не совсем тот, что у работающего математика

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

 Профиль  
                  
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 20:21 
Заслуженный участник
Аватара пользователя


23/07/05
17684
Москва
Xaositect в сообщении #1072276 писал(а):
А почему там куда ни ткнёшь, везде пишет Not Found?

 Профиль  
                  
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 20:35 
Заслуженный участник


31/12/05
1180
http://ssr.msr-inria.inria.fr/

 Профиль  
                  
 
 Re: Самое длинное доказательство
Сообщение12.11.2015, 21:09 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Someone в сообщении #1072739 писал(а):
А почему там куда ни ткнёшь, везде пишет Not Found?
Извиняюсь, не проверил ссылку. Год назад все работало :)

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 21 ]  На страницу Пред.  1, 2

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group