本科同学木瑶的窗子最近写了两篇文章，分别关于机器证明和投票，是这两个话题写的最好的介绍性文章了，分享给大家看一看：
形式证明：机器的光荣和人的梦想

1954年，Davis成功地让电脑证明了定理：偶数加偶数仍然等于偶数。
1959年，王浩让电脑证明了罗素和怀特海的名著《数学原理》中的所有谓词逻辑定理。
1968年，de Bruijn用电脑给出了Landau为其女...