计算机辅助证明

此条目需要扩充。 (2013年2月14日)
请协助改善这篇条目，更进一步的信息可能会在讨论页或扩充请求中找到。请在扩充条目后将此模板移除。

计算机辅助证明是一种部分或全部内容以电脑协助之数学证明。

哲学争议

由于大部分的计算机辅助证明计算量庞大，无法以人手验证，很多数学家不接受计算机辅助证明，并表示那只是计算而非证明。他们表示，美丽的数学证明应像首诗，而电脑证明则看似电话簿。

历史

第一个著名的计算机辅助证明，是1976年的四色定理证明。

著名的计算机辅助证明

四色定理 - 1976
四子棋 - 1988
Order 10有限射影平面的不存在性 - 1989
开普勒猜想
17点的幸福结局问题

参考

自动化定理证明

外部链接

Edmund Furse; Why did AM run out of steam?
Keith Devlin; Last doubts removed about the proof of the Four Color Theorem, MAA Online, January 2005
Number proofs done by computer might err （页面存档备份，存于互联网档案馆）
A Special Issue on Formal Proof. Notices of the American Mathematical Society. December 2008 [2010-09-21]. （原始内容存档于2019-03-14）.
M. Nakao, M. Plum, Y. Watanabe (2019); Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (Springer Series in Computational Mathematics). （页面存档备份，存于互联网档案馆）