有人对定理证明器感兴趣吗?

写了个简单的介绍定理证明器的文章,有一些cs和数学背景应该可以看懂。定理证明器其实回答了一个问题:“怎么才算证明了一个数学命题?”我们在中学学习证明的时候,一般是通过感觉一个证明是合理的,没有遗漏东西就算是证明了,但是这样可能会存在错误。而通过把证明写成代码,再由计算机验证,我们可以真正确保一个证明是正确的。

我觉得哲学生有兴趣的话也可以看看代数方面的知识,最近在看category theory,感觉这个理论非常接近大脑思考问题时候的过程,通过一些基础的原语可以定义出很多有意思的东西。