Разве применение 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.