電腦協助證明

電腦協助證明是一種部份或全部內容以電腦協助之數學證明。

哲學爭議
由於大部份的電腦協助證明計算量龐大，無法以人手驗證，很多數學家不接受電腦協助證明，並表示那只是計算而非證明。他們表示，美麗的數學證明應像首詩，而電腦證明則看似電話簿。

歷史
第一個著名的電腦協助證明，是1976年的四色定理證明。

著名的電腦協助證明
*四色定理 - 1976
*四子棋 - 1988
*Order 10有限射影平面的不存在性 - 1989
*克卜勒猜想
*17點的幸福結局問題

參考

• 自動化定理證明

外部連結

• Edmund Furse; [https://web.archive.org/web/20060528011654/http://www.comp.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html Why did AM run out of steam?]
• Keith Devlin; [https://web.archive.org/web/20100906030843/http://www.maa.org/devlin/devlin_01_05.html Last doubts removed about the proof of the Four Color Theorem], MAA Online, January 2005
• [http://www.post-gazette.com/pg/07012/753384-28.stm Number proofs done by computer might err]

*

• M. Nakao, M. Plum, Y. Watanabe (2019); [https://www.springer.com/gp/book/9789811376689 Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations (Springer Series in Computational Mathematics).]