переходят на coq!". И вот я думаю, а за каким лядом может быть нужен математику coq?! Я могу вообразить только в каких-нибудь разделах общей алгебры и все. Да и то не понятно зачем тратить на него время... Я очень сильно заблуждаюсь? :)
Если я все правильно помню, то Воеводский нашел ошибку в каком-то своем старом рукописном доказательстве, решил, что так больше нельзя, и занялся развитием машиннопроверяемых доказательств
Ну в смысле, а классификацию конечных простых групп как проверить
А вентили в котельных так и продолжать руками крутить?
хм, я думал, только математики им и пользуются
Обсуждают сегодня