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

形式证明：机器的光荣和人的梦想

• 1954年，Davis成功地让电脑证明了定理：偶数加偶数仍然等于偶数。
• 1959年，王浩让电脑证明了罗素和怀特海的名著《数学原理》中的所有谓词逻辑定理。
• 1968年，de Bruijn用电脑给出了Landau为其女儿所写的一本关于实数的入门小册子中的全部数学定理的证明。
• 1976年，Lenat让电脑自发的开始探索数学世界，他的电脑从基本公理开始，自己发现了自然数、加法、乘法、素数这些词的意思，甚至还发现了算术基本定理。
• 1984年，吴文俊发表《几何定理机器证明的基本原理》，用电脑证明了一系列平面几何中的著名定理。
• 1996年，McCune设法让电脑“自动”证明了布尔代数理论中的Robbins猜想。这里“自动”的意思是，把这个猜想输入电脑，回车之后，电脑花了八天时间给出了这个猜想的证明而没有借助人类的任何帮助。
• 2005年，Gonthier建立了四色定理的全部电脑化证明。这一证明和1976年那个证明虽然都用到了电脑，但是其意义则根本不同。1976年的证明本质上仍然是传统证明，电脑只是起到了辅助计算的作用，而Gonthier的证明则是纯粹的形式证明，其每一步逻辑推导都是由电脑完成的。

阅读全文

今天你想投票了吗？

在投票这件事情上，我们面对的不仅是简单的数字游戏，而是人类社会最本质的问题之一：如何才有可能把社会中每个成员的意见，综合成为一个社会的整体意见？有趣的是，对这个问题最好的回答之一是以数学形式得到的。经济学巨擎，1972年诺贝尔经济学奖得主K. Arrow在他的成名作Social Choice and Individual Values中 给出了著名的Arrow定理，在这里考虑的是比投票更为普遍的情况，即如果一个集体中每个成员都对给定的一系列选项（或者候选人）有一组偏好顺序，那么一个“社会选择机制”能够在多好的程度上得到一个综合的排序。换句话说，需要找到一个函数，把所有人的排序映射为一个综合的排序，关于这个函数我们有下面这些自然的标准：

• 非独裁性：这个函数的输出意见不能总是等于同一个人的输入意见，也就是说，不存在一个人的意见总是凌驾于所有人的意见之上。
• 帕雷托最优：如果在每个人的排序中A都优于B，在输出结果中A也应当优于B。
• 无关因素独立性：如果人们对C的看法改变了，不应当影响到结果中A和B的相对排序。

Arrow定理是说，只要有三个或更多的候选者，就不可能存在一个函数，或者说社会选择机制，满足这些标准。

阅读全文