计算机辅助证明
 | 此条目需要扩充。 (2013年2月14日) |
计算机辅助证明是一种部分或全部内容以电脑协助之数学证明。
哲学争议[编辑]
由于大部分的计算机辅助证明计算量庞大，无法以人手验证，很多数学家不接受计算机辅助证明，并表示那只是计算而非证明。他们表示，美丽的数学证明应像首诗，而电脑证明则看似电话簿。
历史[编辑]
第一个著名的计算机辅助证明，是1976年的四色定理证明。
著名的计算机辅助证明[编辑]
参考[编辑]
外部链接[编辑]
- 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). （页面存档备份，存于互联网档案馆）
 | 这是一篇关于数学的小作品。你可以通过编辑或修订扩充其内容。 |