2014 dxdy logo

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

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




Начать новую тему Ответить на тему
 
 Проверка доказательств с помощью Coq
Сообщение14.08.2023, 00:53 


20/09/09
2038
Уфа

(Оффтоп)

Создаю отдельную тему, которая возникла и является оффтопом в этой теме.

Вроде бы существуют автоматизированные системы проверки математических доказательств в научных статьях на ошибки вроде Coq? В. А. Воеводский вроде бы работал над тем же.
Например, если какой-нибудь аспирант прислал в научный журнал математическое доказательство на 200 страниц, а на третьей странице обнаружили ошибку, что аннулирует дальнейшие 197 страниц. Разве применение Coq перед отсылкой статьи в редакцию журнала не позволяет избежать таких проблем?

 Профиль  
                  
 
 Re: Проверка доказательств с помощью Coq
Сообщение14.08.2023, 01:01 


22/10/20
1194
Rasool, найдите на ютубе какой-нибудь курс лекций по Coq и просто посмотрите, как там записываются доказательства. Все вопросы после этого должны отпасть.

 Профиль  
                  
 
 Re: Проверка доказательств с помощью Coq
Сообщение23.08.2023, 22:28 


20/09/09
2038
Уфа
EminentVictorians в сообщении #1605115 писал(а):
Rasool, найдите на ютубе какой-нибудь курс лекций по Coq и просто посмотрите, как там записываются доказательства. Все вопросы после этого должны отпасть.

Спасибо, нашел это.

 Профиль  
                  
 
 Re: Проверка доказательств с помощью Coq
Сообщение24.08.2023, 17:16 
Заслуженный участник


18/09/21
1756
Rasool в сообщении #1605114 писал(а):
Разве применение Coq перед отсылкой статьи в редакцию журнала не позволяет избежать таких проблем?
Просто так туда доказательство не записать.
Надо создать детальное формальное доказательство, где все "дыры" заполнены, что очень турдоёмко (кроме тривиальных случаев).

Вот посмотрите QED manifesto.
Цитата:
The project seems to have dissolved by 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project. In order of importance:

1) Very few people are working on formalization of mathematics. There is no compelling application for fully mechanized mathematics.
2) Formalized mathematics does not yet resemble real, traditional mathematics. This is partly due to the complexity of mathematical notation, and partly to the limitations of existing theorem provers and proof assistants; the paper finds that the major contenders, Mizar, HOL, and Coq, have serious shortcomings in their abilities to express mathematics.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 4 ] 

Модератор: Модераторы



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

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


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

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