电脑协助证明
| 此条目需要扩充。 (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). （页面存档备份，存于互联网档案馆）
 | 这是一篇关于数学的小作品。你可以通过编辑或修订扩充其内容。 |