Zmn-0994-4 师教民 : 简评《基于 Coq 的第三代微积分 机器证明系统》′

【编者按。下面是师教民先生的第四篇评论文章。现在发布如下，供网友们共享。请大家关注并积极评论。另外本《专栏》重申，这里纯属学术讨论，所有发布的各种意 见仅代表作者本人，不代表本《专栏》编辑部的意见。《专栏》中有些文章发扬了啄木鸟精神，对一些错误的观点和言论进行了说理的批评。但请大家注意，也有些有严重错误的文章在这里发布，就是为了引起和得到广大网友们的评论。不要以为在这里发布的文章都是正确无误的。】

【编者注。读者可点击頁面最上面的〖博文〗这个选項，来查找本′《专栏》的其它文章。】