ทฤษฎีบทสี่สีกล่าวว่า แผนที่ใด ๆ ที่วาดบนระนาบสามารถระบายสีได้ด้วยสีไม่เกินสี่สี โดยให้บริเวณที่มีพรมแดนร่วมกันไม่มีสีเดียวกัน บริเวณสองบริเวณที่แตะกันเพียงจุดเดียวสามารถใช้สีเดียวกันได้ ทฤษฎีบทนี้ใช้ได้กับแผนที่ทุกแบบ ไม่ว่าจะซับซ้อนเพียงใด.
บริเวณ 1, 2, 3, 4 แต่ละส่วนมีพรมแดนร่วมกับหลายบริเวณ ส่วนซ้าย (4) และส่วนขวา (4) ไม่ได้มีพรมแดนร่วมกัน จึงใช้สีเดียวกันได้ ตัวอย่างนี้ต้องใช้ 4 สีพอดี.
ฟรานซิส กัทธรีตั้งข้อคาดการณ์นี้ในปี 1852 ระหว่างระบายสีแผนที่มณฑลต่าง ๆ ของอังกฤษ เขาสังเกตว่าสี่สีดูเหมือนจะเพียงพอเสมอ แต่พิสูจน์ไม่ได้ ปัญหานี้ทำให้นักคณิตศาสตร์ติดขัดอยู่นาน 124 ปี มีบทพิสูจน์ผิดพลาดจำนวนมากถูกตีพิมพ์แล้วภายหลังถูกหักล้าง ส่วนห้าสีนั้นเพียงพอเสมอ และสามารถพิสูจน์ได้ด้วยมือโดยใช้สูตรของออยเลอร์สำหรับกราฟเชิงระนาบ.
ทฤษฎีบทสี่สีใช้เวลา 124 ปีจากข้อคาดการณ์ไปสู่บทพิสูจน์ บทพิสูจน์ปี 1976 เป็นทฤษฎีบทสำคัญบทแรกที่ได้รับการตรวจสอบด้วยคอมพิวเตอร์.
บทพิสูจน์ในปี 1976 โดยเคนเน็ธ แอปเพลและโวล์ฟกัง เฮเคน เป็นทฤษฎีบทสำคัญบทแรกที่พิสูจน์ด้วยคอมพิวเตอร์ มันลดแผนที่ที่เป็นไปได้ทั้งหมดให้เหลือการจัดวาง 1,936 แบบ แล้วให้คอมพิวเตอร์ตรวจแต่ละแบบเป็นเวลารวมกว่า 1,200 ชั่วโมงการทำงานของคอมพิวเตอร์ นักคณิตศาสตร์จำนวนมากไม่สบายใจกับบทพิสูจน์ที่ไม่สามารถตรวจสอบด้วยมือได้ทั้งหมด และจนถึงวันนี้ บทพิสูจน์ที่มนุษย์อ่านตรวจได้ง่ายกว่านี้ หากมีอยู่จริง ก็ยังไม่ถูกค้นพบ.
บริเวณด้านนอกห้าส่วน (ซึ่งเป็นจำนวนคี่) บังคับให้วงแหวนต้องใช้ 3 สี เพราะวงจร 5 จุดไม่สามารถลงสีด้วย 2 สีได้ บริเวณตรงกลางติดกับทั้งห้าส่วน จึงสัมผัสสีทั้งสามของวงแหวนและต้องใช้สีที่สี่ สิ่งนี้แสดงว่าในบางกรณีจำเป็นต้องใช้สี่สีจริง ๆ
แผนที่ทุกแผนที่วาดบนระนาบสามารถระบายได้ด้วยสีไม่เกินสี่สี โดยไม่ให้บริเวณที่มีพรมแดนร่วมกันใช้สีเดียวกัน ข้อคาดการณ์นี้ถูกเสนอโดยฟรานซิส กัทธรีในปี 1852 และพิสูจน์โดยแอปเพลและเฮเคนในปี 1976 โดยใช้คอมพิวเตอร์ตรวจสอบการจัดวาง 1,936 แบบ จึงกลายเป็นทฤษฎีบทสำคัญบทแรกที่พิสูจน์ด้วยความช่วยเหลือจากคอมพิวเตอร์ บทพิสูจน์ที่สั้นและเป็นระบบมากขึ้นโดยโรเบิร์ตสัน แซนเดอร์ส ซีมัวร์ และโธมัสในปี 1997 ลดจำนวนกรณีลงและทำให้การตรวจสอบชัดเจนขึ้น แต่ก็ยังอาศัยคอมพิวเตอร์อยู่.