粑粑糁，搜一下机器证明学派（automated proof checking）？ 我们国内吴文俊70年代 就在做这个了。
老图前几天贴的那个数学哲学的链接里简略提了几句：

https://handwiki.org/wiki/Philosophy:Philosophy_of_mathematics#Mathematicism

【 在 Barbarossa 的大作中提到: 】
: 我们讨论哲学时，大家通常能如数家珍一般提起历史上那些所谓伟大的哲学家。很多人攀龙附凤，借机谈论这些如雷贯耳的名字来提高自己的身价，仿佛一只野鸡突然变成了金凤凰，使自己变得高高在上。特别是，当他拾人牙慧地堆砌一些他自己也云里雾里半通不通的名词，让一些不明所以的听众，尤其是女听众被唬得一愣一愣时，优越感爆棚，似乎自己变成了世界上最伟大的哲学家了。
: 不幸的消息传来了。一门流派的哲学，只不过是某个个体创造出一个学说，比如康德哲学，庄子哲学，或者其他哲学。这些哲学无论如何听起来多么高大上，归根到底都能够装进一个人的脑袋，超越不了单个个体的心智范围。
: 曾几何时，一个哲学流派诞生出来，世界为之震动。但是你们会发现最近几十年没有任何新的流派诞生出来，对哲学感兴趣的人越来越少，原因是，哲学被信息化了，就像各行各业都要计算机化一样，哲学这个行业也被信息化，无法用来装逼，也装不起来。为啥？从人工智能角度看，哲学也是收集数据，处理数据，得出结论。但一个哲学家他的大脑无法和计算机内存比，算力没法和电脑比，精巧的算法更是没有。因此旧时代的哲学家在人工智能时代，无法无所不知，无所不晓，无所不能。哲学家被无助化，弱化，低能化，最终会被扫入历史的垃圾堆。
--
FROM 125.33.200.*

你还是搜了再说吧。。。
希望你不会后悔刚说过的话。

【 在 Barbarossa 的大作中提到: 】
: 他无名小辈，不足挂齿。请问他发表了什么文章？
--
FROM 125.33.200.*