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