四色定理：计算机辅助完成的冗长的证明

在不撞色的前提下，我们能用最少的颜色给所有地图着色吗？1879年，亚瑟·肯普关于地图着色问题可能形式绘制了第一副图，他画出了边境接壤的各种可能形式来证明四种颜色是让相邻地区不撞色的最小可能。托马斯·黑尔斯证明了开普勒球填充猜想的最大填充密度是正确的，证明包含了250页的人类数学分析和3GB的计算机代码和输出结果。