不用计算机证明数学定理,计算机证明数学定理的方式论
数学证明不是对就是错，数学没有灰色地带。数学界许多人不接受借助计算机证明定理这种方式，戏称那是暴力法。
开普勒猜想的证明花了400年时间，甚至在那项证明公之于世的6年后，仍然有许多数学家在专心致志地思索这个证明问题。
1611年，开普勒提出排列球体最有效率的方式是以金字塔形式堆栈，如同世界各地杂货摊老板堆放西红柿、苹果和柳橙那样，但证明这个看起来显而易见的观点却出乎意料地困难。直到1998年，密西根大学数学教授黑尔斯(Thomas C.Hales)才借助计算机成功证明了开普勒猜想。数学界许多人不接受这种证明定理的方式，戏称那是暴力法。
普林斯顿高等研究院的麦克弗森(Robert MacPherson)，也是著名期刊《数学年刊》(Annals of Mathematics)的编辑，希望刊登这个证明。依照所有科学文章的发表惯例，他请专家严谨地审查这篇论文。12位数学家仔细研读数百贞计算机计算出来的结果，细察和质疑每一个细节。5年后，他们认输了。虽然他们没有发现谬误、缺失或程序错误，但还是觉得不安，因为不可能检查每一行计算编码，重新进行每一步计算机运算，因此，他们无法绝对肯定这个证明的正确性。数学家们又气又累，说他们没法保证这个计算机辅助证明绝对正确。