電腦協助證明

此條目需要擴充。 (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). （页面存档备份，存于互联网档案馆）

这是一篇关于数学的小作品。您可以通过编辑或修订扩充其内容。 查 论 编