การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ เป็นบทพิสูจน์ทฤษฎีทางคณิตศาสตร์ที่มีบางส่วนถูกสร้างขึ้นโดยคอมพิวเตอร์ บทพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยส่วนใหญ่ในปัจจุบัน มักใช้วิธีการพิสูจน์โดยการลองทุกความเป็นไปได้ของทฤษฎีที่พยายามพิสูจน์อยู่ ทฤษฎีบทสี่สีเป็นทฤษฎีใหญ่อันแรกที่ถูกพิสูจน์ด้วยคอมพิวเตอร์
แนวคิดของวิธีการนี้ คือการให้คอมพิวเตอร์รับหน้าที่ทำการคำนวณอันยืดยาว โดยใช้เทคนิคเลขคณิตเชิงช่วงในการควบคุม ไม่ให้มีความผิดพลาดมากเกินไป นั่นคือ เราสามารถมองการคำนวณที่ซับซ้อน เป็นลำดับของการคำนวณพื้นฐาน (เช่น +, -, *, /) ผลที่ได้จากการคำนวณพื้นฐานแต่ละขั้นนี้ เป็นผลโดยประมาณเนื่องจากคอมพิวเตอร์มีความแม่นยำจำกัด อย่างไรก็ตาม เราสามารถสร้างช่วงของคำตอบที่ถูกต้องได้จากผลโดยประมาณนี้ จากนั้นเราสามารถดำเนินการขั้นตอนต่อๆไป โดยการทำการคำนวณระหว่างช่วงของตัวเลขแต่ละตัวที่ได้มา
นอกจากนี้ ในสาขาวิจัยทางด้านปัญญาประดิษฐ์ ยังได้มีความพยายาม ที่จะสร้างบทพิสูจน์ใหม่ที่กระชับและชัดเจนกว่าเดิม โดยการใช้เทคนิคการให้เหตุผลโดยเครื่องจักร เช่น การค้นหาแบบฮิวริสติก ตัวพิสูจน์โดยอัตโนมัติดังกล่าวนี้ ได้ช่วยพิสูจน์ทฤษฏีใหม่ๆ อีกทั้งยังสร้างบทพิสูจน์ใหม่ๆ ให้กับทฤษฏีที่เคยได้รับพิสูจน์มาแล้วอีกด้วย
เป้าหมายเชิงปรัชญา
การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ เป็นประเด็นที่มีการโต้เถียงกันมากในวงการคณิตศาสตร์ นักคณิตศาสตร์บางคนมีความเชื่อว่า บทพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยอันแสนยืดยาวนั้น ไม่ถือเป็นบทพิสูจน์ทางคณิตศาสตร์จริงๆ เนื่องจากบทพิสูจน์แบบนี้ เต็มไปด้วยขั้นตอนการให้เหตุผลทางคณิตศาสตร์ ที่ยาวเกินกว่าที่มนุษย์จะสามารถตรวจสอบได้ และรู้สึกว่านักคณิตศาสตร์ถูกบังคับให้ไว้ใจ ในการเขียนโปรแกรมคอมพิวเตอร์
ในทางกลับกัน เราสามารถถามคำถามโต้กลับได้ว่า หากมนุษย์ไม่ไว้ใจคอมพิวเตอร์ให้ทำการคำนวณอันยืดยาวแล้ว เหตุใดเราจึงไว้ใจในการใช้เหตุผลอันยืดยาวไม่แพ้กัน ของนักคณิตศาสตร์บางคน?
อ้างอิง
- Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STAN-CS-76-570, and Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.
แหล่งข้อมูลอื่น
