微软公司与四色定理

用计算机证明数学定理是从证明四色定理开始的，在证明的过程中，算法和形式体系结合将彻底地改变数学传统，Dr.Gonthier相信，总有一天数学证明的成立不成立，将不再依赖数学同事的集体和议，而有一点儿像可重复、可复制的物理实验那样被验证，而微软公司相信通过证明四色定理，可以发展许多数学和编码工具，找到排除软件BUG的方法和技术。