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

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

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

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

Automathซึ่งพัฒนาโดยNicolaas Govert de Bruijnเริ่มต้นในปี 1967 มักถูกพิจารณาว่าเป็นตัวตรวจสอบการพิสูจน์ตัวแรกและเป็นระบบแรกที่ใช้การจับคู่ Curry–Howardระหว่างโปรแกรมและการพิสูจน์^{[ 2 ]} Automath ถูกใช้โดย LS van Benthem Jutting ในปี 1977 เพื่อกำหนดรูปแบบอย่างเป็นทางการของFoundations of Analysis ของ Landau ซึ่งเป็นการกำหนดรูปแบบอย่างเป็นทางการครั้งแรกของจำนวนจริง^{[ 3 ]}

ในปี พ.ศ. 2516 Robert BoyerและJ Mooreได้ตีพิมพ์Proving Theorems about LISP Functions ซึ่งมีจุดมุ่งหมายเพื่อตรวจสอบ โปรแกรม ไม่ใช่คณิตศาสตร์^{[ 4 ]}ปัจจุบันโปรแกรมพิสูจน์ทฤษฎีบทของพวกเขาเป็นที่รู้จักในชื่อACL2

ในช่วงทศวรรษ 1970 LCF แห่งเอดินบะระได้นำเสนอแนวคิดในการใช้ภาษาการเขียนโปรแกรมเชิงฟังก์ชันเป็นภาษาเมตาสำหรับตัวพิสูจน์ทฤษฎีบท และนำไปสู่ตระกูลตัวช่วยพิสูจน์HOL ^{[ 3 ]}

ในช่วงทศวรรษ 1990 โปรแกรมRocq (ซึ่งในขณะนั้นรู้จักกันในชื่อ Coq) ได้รับความนิยมอย่างมาก และถูกนำไปใช้ในโครงการสร้างแบบจำลองทางคณิตศาสตร์ขนาดใหญ่ หลายโครงการ ตั้งแต่ช่วงปลายทศวรรษ 2010 เป็นต้นมาLeanซึ่งเป็นโปรแกรมช่วยพิสูจน์ที่ได้รับอิทธิพลอย่างมากจาก Rocq ก็กลายเป็นอีกทางเลือกยอดนิยม โดยเฉพาะอย่างยิ่งสำหรับการสร้างแบบจำลองทางคณิตศาสตร์

• ACL2 – ภาษาโปรแกรม ทฤษฎีตรรกะลำดับที่หนึ่ง และตัวพิสูจน์ทฤษฎีบท (ทั้งโหมดโต้ตอบและโหมดอัตโนมัติ) ตามแบบฉบับของ Boyer–Moore
• โปรแกรมพิสูจน์ทฤษฎีบท HOL – ชุดเครื่องมือที่พัฒนามาจากโปรแกรมพิสูจน์ทฤษฎีบท LCFในระบบเหล่านี้ แกนหลักเชิงตรรกะคือไลบรารีของภาษาโปรแกรม ทฤษฎีบทแสดงถึงองค์ประกอบใหม่ของภาษา และสามารถนำเสนอได้ผ่าน "กลยุทธ์" เท่านั้น ซึ่งรับประกันความถูกต้องเชิงตรรกะ การประกอบกลยุทธ์ช่วยให้ผู้ใช้สามารถสร้างบทพิสูจน์ที่สำคัญได้โดยมีการโต้ตอบกับระบบค่อนข้างน้อย สมาชิกในตระกูลนี้ได้แก่:
  • HOL4 – รุ่น "ทายาทหลัก" ที่ยังคงได้รับการพัฒนาอย่างต่อเนื่อง รองรับทั้งMoscow MLและPoly/MLมีใบอนุญาตแบบ BSD
  • HOL Light – โปรเจกต์ "มินิมอลลิสต์" ที่กำลังเติบโตอย่างรวดเร็วพัฒนาด้วยภาษาOCaml
  • ProofPower – เคยเป็นซอฟต์แวร์กรรมสิทธิ์ แล้วกลับมาเป็นโอเพนซอร์สอีกครั้ง โดยอิงจากStandard Machine Learning
• IMPS ระบบพิสูจน์ทางคณิตศาสตร์แบบโต้ตอบ^{[ 11 ]}
• Isabelleเป็นตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบที่สามารถเข้ารหัสระบบอื่นๆ ได้ Isabelle/HOL เป็นอินสแตนซ์ที่ได้รับความนิยมมากที่สุด ซึ่งมีพื้นฐานใกล้เคียงกับตัวพิสูจน์ HOL อินสแตนซ์อื่นๆ ได้แก่ Isabelle/ZF และ Isabelle/FOL ^{[ 12 ]}โค้ดเบสหลักได้รับอนุญาตภายใต้ BSD แต่การแจกจ่าย Isabelle มีเครื่องมือเสริมมากมายที่มีใบอนุญาตที่แตกต่างกัน
• Jape – แอปพลิเคชันที่ใช้ภาษา Java
• Leanเป็นทั้งโปรแกรมพิสูจน์ทฤษฎีบทแบบโต้ตอบและภาษาโปรแกรมเชิงฟังก์ชันที่มีการกำหนดประเภทแบบพึ่งพา มันมีพื้นฐานมาจากแคลคูลัสของการสร้างแบบอุปนัยที่มีเอกภพที่ไม่สะสม ตั้งแต่เวอร์ชัน 4 (เปิดตัวในปี 2023) มันสามารถทำงานบนเซิร์ฟเวอร์ของตัวเองได้ สามารถใช้ในการกำหนดรูปแบบทางคณิตศาสตร์ (และมีไลบรารีขนาดใหญ่ที่สอดคล้องกันสำหรับคณิตศาสตร์เชิงรูปธรรม) แต่ยังสามารถใช้สำหรับการตรวจสอบซอฟต์แวร์และฮาร์ดแวร์ได้อีกด้วย
• เลโก้
• Matita – ระบบแสงสว่างที่ใช้หลักการคำนวณแบบอุปนัย
• MINLOG – เครื่องมือช่วยพิสูจน์ที่ใช้ตรรกะขั้นต่ำลำดับที่หนึ่ง
• Mizar – โปรแกรมช่วยพิสูจน์ที่ใช้ตรรกะลำดับที่หนึ่ง ใน รูปแบบ การอนุมานตามธรรมชาติและทฤษฎีเซต Tarski– Grothendieck
• PhoX – เครื่องมือช่วยพิสูจน์ที่ใช้ตรรกะลำดับสูงซึ่งสามารถขยายได้
• ระบบตรวจสอบต้นแบบ (Prototype Verification System - PVS) – ภาษาและระบบพิสูจน์ที่ใช้ตรรกะลำดับสูง
• Rocq (เดิมชื่อCoq ) – โปรแกรมพิสูจน์ทฤษฎีบทแบบโต้ตอบที่ได้รับความนิยม โดยอิงจากแคลคูลัสของการสร้างแบบอุปนัย
• ระบบพิสูจน์ทฤษฎีบท (TPS) และ ETPS – โปรแกรมพิสูจน์ทฤษฎีบทแบบโต้ตอบซึ่งใช้แคลคูลัสแลมบ์ดาแบบกำหนดประเภทอย่างง่ายเช่นกัน แต่มีพื้นฐานมาจากทฤษฎีตรรกะที่กำหนดขึ้นเองและการใช้งานที่เป็นอิสระ

โปรแกรมช่วยพิสูจน์ที่ใช้กันทั่วไปคือ Proof General ซึ่งพัฒนาโดย Emacsที่มหาวิทยาลัยเอดินบะระปัจจุบัน โปรแกรมพิสูจน์หลายตัวมีตัวแก้ไขของตัวเอง Rocq มี RocqIDE ซึ่งใช้ OCaml/ Gtk เป็นพื้นฐาน Isabelle มี Isabelle/jEdit ซึ่งใช้jEditและโครงสร้างพื้นฐาน Isabelle/ Scalaสำหรับการประมวลผลการพิสูจน์แบบเน้นเอกสาร เมื่อไม่นานมานี้ มีการพัฒนาส่วนขยาย Visual Studio Codeสำหรับ Rocq ^{[ 13 ]} Isabelle โดย Makarius Wenzel ^{[ 14 ]}และสำหรับ Lean 4 โดยนักพัฒนา leanprover ^{[ 15 ]}

Freek Wiedijk ได้จัดอันดับผู้ช่วยพิสูจน์ตามจำนวนทฤษฎีบทที่ได้รับการพิสูจน์อย่างเป็นทางการจากรายการทฤษฎีบทที่รู้จักกันดี 100 รายการ ณ เดือนกันยายน พ.ศ. 2568 มีเพียง 6 ระบบเท่านั้นที่พิสูจน์ทฤษฎีบทได้มากกว่า 70% ได้แก่ Isabelle, HOL Light, Lean, Rocq, Metamath และ Mizar ^{[ 16 ] [ 17 ]}

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

ทฤษฎีบท	ผู้ช่วยพิสูจน์อักษร	ปี
ทฤษฎีสี่สี[ 18 ]	ร็อค	2548
ทฤษฎีบทเฟต-ทอมป์สัน[ 19 ]	ร็อค	2012
กลุ่มพื้นฐานของวงกลม[ 20 ]	ร็อค	2013
ปัญหาแอร์ดอส-เกรแฮม[ 21 ] [ 22 ]	เอียง	2022
การคาดการณ์พหุนาม Freiman-Ruzsa เกี่ยวกับ[ 23 ]${\displaystyle \mathbb {F} _{2}}$	เอียง	2023
BB(5) = 47,176,870 [ 24 ]	ร็อค	2024

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

• Barendregt, Henk ; Geuvers, Herman (2001). "18. ตัวช่วยพิสูจน์โดยใช้ระบบประเภทที่ขึ้นอยู่กับเงื่อนไข" (PDF)ใน Robinson, Alan JA; Voronkov, Andrei (บรรณาธิการ). คู่มือการให้เหตุผลอัตโนมัติเล่ม 2. Elsevier. หน้า 1149–. ISBN 978-0-444-50812-6เก็บถาวรจากไฟล์ต้นฉบับ(PDF)เมื่อวันที่ 27 กรกฎาคม 2550
• Pfenning, Frank . "17. กรอบตรรกะ" (PDF) . คู่มือเล่ม 2 ปี 2001.หน้า  1065–1148 .
• Pfenning, Frank (1996). "การปฏิบัติของกรอบตรรกะ". ใน Kirchner, H. (บรรณาธิการ). ต้นไม้ในพีชคณิตและการเขียนโปรแกรม – CAAP '96 . บันทึกการบรรยายในวิทยาการคอมพิวเตอร์. เล่มที่ 1059. Springer. หน้า  119–134 . doi : 10.1007/3-540-61064-2_33 . ISBN 3-540-61064-2.
• Constable, Robert L. (1998). "X. ประเภทในวิทยาการคอมพิวเตอร์ ปรัชญา และตรรกศาสตร์"ใน Buss, SR (บรรณาธิการ). คู่มือทฤษฎีการพิสูจน์การศึกษาตรรกศาสตร์ เล่มที่ 137. Elsevier. หน้า  683–786 . ISBN 978-0-08-053318-6.
• วีดิจค์, ฟรีค (2005) "สิบเจ็ดผู้พิสูจน์โลก" (PDF ) มหาวิทยาลัย Radboud ไนเมเกน

• พิพิธภัณฑ์ผู้พิสูจน์ทฤษฎีบท
• "บทนำ"ในหลักสูตรการเขียนโปรแกรมโดยใช้ประเภทข้อมูลแบบพึ่งพา ( Certified Programming with Dependent Types)
• บทนำสู่โปรแกรมช่วยพิสูจน์ Coq (พร้อมบทนำทั่วไปเกี่ยวกับการพิสูจน์ทฤษฎีบทแบบโต้ตอบ)
• การพิสูจน์ทฤษฎีบทแบบโต้ตอบสำหรับผู้ใช้ Agda
• รายชื่อเครื่องมือพิสูจน์ทฤษฎีบท

แคตตาล็อก

• คณิตศาสตร์ดิจิทัล แบ่งตามหมวดหมู่: เครื่องมือพิสูจน์กลยุทธ์
• ระบบและกลุ่มการหักเงินอัตโนมัติ
• ระบบการพิสูจน์ทฤษฎีบทและการให้เหตุผลอัตโนมัติ
• ฐานข้อมูลระบบการให้เหตุผลเชิงกลที่มีอยู่
• NuPRL: ระบบอื่นๆ
• "กรอบตรรกะเฉพาะและการนำไปใช้"เก็บถาวรจากต้นฉบับเมื่อวันที่ 10 เมษายน 2565 เรียกดูเมื่อวันที่ 15 กุมภาพันธ์ 2567(โดย แฟรงค์ เฟนนิง)
• DMOZ : วิทยาศาสตร์ : คณิตศาสตร์ : ตรรกศาสตร์และพื้นฐาน : ตรรกศาสตร์เชิงคำนวณ : กรอบตรรกะ