การ พิสูจน์โดย ใช้ คอมพิวเตอร์ช่วยคือการพิสูจน์ทางคณิตศาสตร์ที่อย่างน้อยบางส่วนถูกสร้างขึ้นโดยคอมพิวเตอร์

การพิสูจน์โดยใช้คอมพิวเตอร์ส่วนใหญ่ในปัจจุบันเป็นการนำการพิสูจน์ทฤษฎีทางคณิตศาสตร์ แบบ ละเอียดมาใช้ แนวคิดคือการใช้โปรแกรมคอมพิวเตอร์ในการคำนวณที่ยาวนาน และให้การพิสูจน์ว่าผลลัพธ์ของการคำนวณเหล่านั้นบ่งชี้ถึงทฤษฎีที่กำหนด ในปี 1976 ทฤษฎีสี่สีเป็นทฤษฎีสำคัญแรกที่ได้รับการตรวจสอบโดยใช้โปรแกรม คอมพิวเตอร์

ในด้าน การวิจัย ปัญญาประดิษฐ์ มีความพยายาม ที่จะสร้างบทพิสูจน์ใหม่ที่ชัดเจนและกระชับยิ่งขึ้นสำหรับทฤษฎีบททางคณิตศาสตร์ โดยใช้ เทคนิค การให้เหตุผลอัตโนมัติเช่นการค้นหาแบบฮิวริสติกเครื่องมือพิสูจน์ทฤษฎีบทอัตโนมัติ เหล่านี้ ได้พิสูจน์ผลลัพธ์ใหม่ ๆ จำนวนมากและค้นพบบทพิสูจน์ใหม่สำหรับทฤษฎีบทที่รู้จักกันอยู่แล้ว นอกจากนี้ผู้ช่วยพิสูจน์ แบบโต้ตอบ ยังช่วยให้นักคณิตศาสตร์สามารถพัฒนาบทพิสูจน์ที่มนุษย์อ่านได้ ซึ่งได้รับการตรวจสอบความถูกต้องอย่างเป็นทางการแล้ว เนื่องจากบทพิสูจน์เหล่านี้โดยทั่วไปสามารถตรวจสอบได้โดยมนุษย์ (แม้ว่าจะทำได้ยาก เช่นเดียวกับการพิสูจน์ข้อสันนิษฐานของร็อบบินส์ ) จึงไม่มีนัยยะที่ก่อให้เกิดข้อถกเถียงเหมือนกับการพิสูจน์โดยใช้คอมพิวเตอร์ช่วยแบบครบถ้วน

วิธีหนึ่งในการใช้คอมพิวเตอร์ในการพิสูจน์ทางคณิตศาสตร์คือการใช้สิ่งที่เรียกว่าการคำนวณเชิงตัวเลขที่ผ่านการ ตรวจสอบ แล้ว หรือการคำนวณเชิงตัวเลขที่เข้มงวด ซึ่งหมายถึงการคำนวณเชิงตัวเลขแต่มีความแม่นยำทางคณิตศาสตร์ โดยใช้เลขคณิตแบบเซตและหลักการรวมเพื่อให้แน่ใจว่าผลลัพธ์แบบเซตของโปรแกรมเชิงตัวเลขนั้นครอบคลุมคำตอบของปัญหาทางคณิตศาสตร์ดั้งเดิม ทำได้โดยการควบคุม การครอบคลุม และการกระจายข้อผิดพลาดจากการปัดเศษและการตัดทอนโดยใช้เลขคณิตแบบช่วงเป็นต้นกล่าวคือ ลดการคำนวณลงเหลือลำดับของการดำเนินการพื้นฐาน เช่นในคอมพิวเตอร์ ผลลัพธ์ของการดำเนินการพื้นฐานแต่ละครั้งจะถูกปัดเศษตามความแม่นยำของคอมพิวเตอร์ อย่างไรก็ตาม เราสามารถสร้างช่วงที่กำหนดโดยขอบเขตบนและล่างของผลลัพธ์ของการดำเนินการพื้นฐานได้ จากนั้นจึงดำเนินการแทนที่ตัวเลขด้วยช่วงและทำการดำเนินการพื้นฐานระหว่างช่วงของตัวเลขที่สามารถแทนได้เหล่านั้น ${\displaystyle (+,-,\times ,/)}$

การพิสูจน์โดยใช้คอมพิวเตอร์ช่วยเป็นประเด็นถกเถียงในวงการคณิตศาสตร์ โดยโทมัส ทิมอคซ์โกเป็นคนแรกที่แสดงข้อโต้แย้ง ผู้ที่ยึดถือตามข้อโต้แย้งของทิมอคซ์โกเชื่อว่าการพิสูจน์โดยใช้คอมพิวเตอร์ช่วยที่ยาวนานนั้น ในแง่หนึ่งไม่ใช่การพิสูจน์ทางคณิตศาสตร์ ที่ 'แท้จริง' เพราะมีขั้นตอนเชิงตรรกะมากมายจน มนุษย์ไม่สามารถตรวจสอบได้ จริง และนักคณิตศาสตร์ถูกขอให้แทนที่ การอนุมานเชิงตรรกะจากสัจพจน์ ที่สมมติขึ้น ด้วยความเชื่อมั่นในกระบวนการคำนวณเชิงประจักษ์ ซึ่งอาจได้รับผลกระทบจากข้อผิดพลาดในโปรแกรมคอมพิวเตอร์ รวมถึงข้อบกพร่องในสภาพแวดล้อมการทำงานและฮาร์ดแวร์^{[ 1 ]}

นักคณิตศาสตร์คนอื่นๆ เชื่อว่า การพิสูจน์โดยใช้คอมพิวเตอร์ที่ใช้เวลานาน ควรถูกมองว่าเป็นการคำนวณมากกว่าการพิสูจน์กล่าวคือ ควรพิสูจน์ความถูกต้องของอัลกอริทึมการพิสูจน์เสียก่อน เพื่อให้การใช้งานนั้นถือได้ว่าเป็นเพียง "การตรวจสอบ" เท่านั้น ข้อโต้แย้งที่ว่าการพิสูจน์โดยใช้คอมพิวเตอร์อาจมีข้อผิดพลาดในโปรแกรมต้นฉบับ คอมไพเลอร์ และฮาร์ดแวร์ สามารถแก้ไขได้โดยการให้การพิสูจน์ความถูกต้องอย่างเป็นทางการสำหรับโปรแกรมคอมพิวเตอร์ (ซึ่งเป็นแนวทางที่ประสบความสำเร็จในการนำไปใช้กับทฤษฎีบทสี่สีในปี 2548) รวมถึงการจำลองผลลัพธ์โดยใช้ภาษาโปรแกรม คอมไพเลอร์ และฮาร์ดแวร์คอมพิวเตอร์ที่แตกต่างกัน

อีกวิธีหนึ่งที่เป็นไปได้ในการตรวจสอบความถูกต้องของบทพิสูจน์ที่สร้างโดยคอมพิวเตอร์คือ การสร้างขั้นตอนการให้เหตุผลใน รูปแบบ ที่เครื่องอ่านได้จากนั้นใช้ โปรแกรม ตรวจสอบบทพิสูจน์เพื่อแสดงความถูกต้อง เนื่องจากการตรวจสอบความถูกต้องของบทพิสูจน์ที่กำหนดนั้นง่ายกว่าการค้นหาบทพิสูจน์มาก โปรแกรมตรวจสอบจึงง่ายกว่าโปรแกรมช่วยเหลือเดิม และทำให้มั่นใจในความถูกต้องได้ง่ายขึ้น อย่างไรก็ตาม วิธีการใช้โปรแกรมคอมพิวเตอร์เพื่อพิสูจน์ความถูกต้องของผลลัพธ์จากโปรแกรมอื่นนี้ไม่เป็นที่ถูกใจผู้ที่สงสัยในบทพิสูจน์ที่สร้างโดยคอมพิวเตอร์ ซึ่งมองว่าเป็นการเพิ่มความซับซ้อนอีกชั้นหนึ่งโดยไม่ตอบสนองความต้องการความเข้าใจของมนุษย์

อีกข้อโต้แย้งหนึ่งต่อการพิสูจน์โดยใช้คอมพิวเตอร์ช่วยคือ การพิสูจน์เหล่านั้นขาดความสง่างามทางคณิตศาสตร์กล่าวคือ ไม่ได้ให้ข้อมูลเชิงลึกหรือแนวคิดใหม่ ๆ ที่มีประโยชน์ อันที่จริง นี่เป็นข้อโต้แย้งที่สามารถนำมาใช้กับวิธีการพิสูจน์แบบละเอียดทุกวิธีได้เช่นกัน

ประเด็นทางปรัชญาเพิ่มเติมที่เกิดขึ้นจากการพิสูจน์ด้วยคอมพิวเตอร์คือ การพิสูจน์ดังกล่าวทำให้คณิตศาสตร์กลายเป็นวิทยาศาสตร์กึ่งเชิงประจักษ์ หรือไม่ ซึ่งวิธีการทางวิทยาศาสตร์จะมีความสำคัญมากกว่าการใช้เหตุผลบริสุทธิ์ในด้านแนวคิดทางคณิตศาสตร์เชิงนามธรรม ประเด็นนี้เกี่ยวข้องโดยตรงกับข้อโต้แย้งภายในคณิตศาสตร์ว่า คณิตศาสตร์นั้นตั้งอยู่บนพื้นฐานของความคิด หรือเป็นเพียงการฝึกฝนการจัดการสัญลักษณ์อย่างเป็นทางการ นอกจากนี้ยังก่อให้เกิดคำถามว่า หากตาม ทัศนะ ของเพลโตแล้ววัตถุทางคณิตศาสตร์ที่เป็นไปได้ทั้งหมด "มีอยู่แล้ว" ในบางแง่มุม คณิตศาสตร์ที่ใช้คอมพิวเตอร์ช่วยนั้นเป็น วิทยาศาสตร์ เชิงสังเกตการณ์ เช่นเดียวกับดาราศาสตร์ หรือเป็นวิทยาศาสตร์เชิงทดลองเช่นเดียวกับฟิสิกส์หรือเคมี ข้อโต้แย้งภายในคณิตศาสตร์นี้เกิดขึ้นพร้อมๆ กับคำถามที่เกิดขึ้นในวงการฟิสิกส์ว่า ฟิสิกส์เชิงทฤษฎีในศตวรรษที่ 21 กำลังกลายเป็นคณิตศาสตร์มากเกินไปหรือไม่ และละทิ้งรากฐานเชิงทดลองไปหรือไม่

สาขาคณิตศาสตร์เชิงทดลอง ที่กำลังเกิดขึ้นใหม่นี้ กำลังเผชิญหน้ากับการถกเถียงนี้โดยตรง โดยมุ่งเน้นที่การทดลองเชิงตัวเลขเป็นเครื่องมือหลักในการสำรวจทางคณิตศาสตร์

การรวมอยู่ในรายชื่อนี้ไม่ได้หมายความว่ามีหลักฐานพิสูจน์ที่ตรวจสอบโดยคอมพิวเตอร์อย่างเป็นทางการ แต่หมายความว่าโปรแกรมคอมพิวเตอร์มีส่วนเกี่ยวข้องในบางทาง โปรดดูรายละเอียดเพิ่มเติมในบทความหลัก

• Lenat, DB (1976). AM: แนวทางปัญญาประดิษฐ์เพื่อการค้นพบในคณิตศาสตร์ในรูปแบบการค้นหาแบบฮิวริสติก (PDF) (ปริญญาเอก). ห้องปฏิบัติการ AI, มหาวิทยาลัยสแตนฟอร์ด. STAN-CS-76-570, รายงานโครงการเขียนโปรแกรมแบบฮิวริสติก HPP-76-8.
• Meyer, KR; Schmidt, DS, บรรณาธิการ (2012). การพิสูจน์โดยใช้คอมพิวเตอร์ช่วยในการวิเคราะห์ . ชุดหนังสือ IMA ในสาขาคณิตศาสตร์และการประยุกต์ใช้. เล่มที่ 28. Springer. ISBN 978-1-4613-9092-3.
• Nakao, M.; Plum, M.; Watanabe, Y. (2019). วิธีการตรวจสอบเชิงตัวเลขและการพิสูจน์โดยใช้คอมพิวเตอร์ช่วยสำหรับสมการเชิงอนุพันธ์ย่อย . ชุดหนังสือคณิตศาสตร์เชิงคำนวณของ Springer. Springer. ISBN 9789811376696.

• Lanford, Oscar E. (1982). "การพิสูจน์สมมติฐานของ Feigenbaum โดยใช้คอมพิวเตอร์ช่วย" (PDF) . Bull. Amer. Math. Soc . 6 (3): 427– 434. CiteSeerX  10.1.1.434.8389 . doi : 10.1090/S0273-0979-1982-15008-X .
• เฟอร์ส, เอ็ดมุนด์ (1990). ทำไม AM ถึงหมดแรง? (รายงานทางเทคนิค). ภาควิชาวิทยาการคอมพิวเตอร์ มหาวิทยาลัยแกลมอร์แกน. CS-90-4. เก็บถาวรจากต้นฉบับเมื่อ 17 กรกฎาคม 2012. สืบค้นเมื่อ6 กันยายน 2016 .{{cite tech report}}: CS1 maint: bot: สถานะ URL เดิมไม่ทราบ ( ลิงก์ )
• เบกลีย์, เอส. (16 เมษายน 2561). "การพิสูจน์ตัวเลขที่ทำโดยคอมพิวเตอร์อาจผิดพลาดได้" . พิตต์สเบิร์ก โพสต์-กาเซ็ตต์ . เก็บถาวรจากต้นฉบับเมื่อ 16 เมษายน 2561.
• "ฉบับพิเศษว่าด้วยการพิสูจน์เชิงรูปธรรม"วารสารNotices of the American Mathematical Societyธันวาคม 2008