Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?