四色定理：机器首次碾压数学家

The Four Colour Theorem: The first time machines mogged mathematicians

1976年，困扰数学界百年的四色定理终于被 Kenneth Appel 和 Wolfgang Haken 破解，但过程却引发轩然大波：他们动用了计算机进行1200小时的运算和100亿次决策。这一突破标志着人类首次依赖机器完成数学证明，却遭到 Herbert Wilf 等权威数学家的强烈质疑，甚至被斥为“亵渎”。老一辈数学家难以接受无法人工验证的证明，而年轻一代则对冗长的手算充满怀疑。这场争论不仅关乎证明本身，更触及了数学的本质与人类理性的边界。