ทฤษฎีบทสี่สี
ประวัติ

ข้อความคาดการณ์อันนี้ถูกกล่าวถึงครั้งแรกในปี พ.ศ. 2395 (ค.ศ. 1852) เมื่อ ฟรานซิส กูทรี (Francis Guthrie) ได้สังเกตเห็นว่าสามารถใช้เพียงสี่สีก็เพียงพอในการระบาย ขณะที่กำลังระบายแผนที่ของเขตหนึ่งในอังกฤษ ในขณะนั้นกูทรีเป็นลูกศิษย์ของ ออกัสตัส เดอ มอร์แกน (Augustus De Morgan) ที่ ยูนิเวอร์ซิตีคอลเลจลอนดอน (University College London) (กูทรีจบการศึกษาในปี พ.ศ. 2393 (ค.ศ. 1850) และต่อมาได้เป็นศาสตราจารย์สาขาคณิตศาสตร์ในประเทศแอฟริกาใต้) โดยตามคำบอกเล่าของเดอร์มอร์แกน:
หลักฐานอ้างอิงที่มีการตีพิมพ์เป็นอันแรกถูกพบในงานของ อาร์เทอร์ เคย์เลย์ (Arthur Cayley) On the colourings of maps., Proc. Royal Geography Society 1, 259-261, 1879.
นับตั้งแต่ข้อความคาดการณ์นี้ถูกประกาศขึ้นมา ก็มีผู้คนจำนวนมากต้องประสบความล้มเหลวในการพิสูจน์มัน บทพิสูจน์หนึ่งของทฤษฎีบทนี้คืองานของ อัลเฟรด เคมป์ (Alfred Kempe) ในปี พ.ศ. 2422 (ค.ศ. 1879) ซึ่งเป็นชิ้นที่ผู้คนยอมรับกันทั่วไป บทพิสูจน์อีกอันหนึ่งคือของ ปีเตอร์ เทท (Peter Tait) ในปี พ.ศ. 2423(1880) จวบจนกระทั่งปี พ.ศ. 2433 (ค.ศ. 1890) เพอร์ซี เฮวูด (Percy Heawood) จึงได้แสดงว่าบทพิสูจน์ของเคมป์มีข้อผิดพลาด และใน พ.ศ. 2434 (ค.ศ. 1891) จูเลียส ปีเตอร์เซน (Julius Petersen) จึงได้แสดงว่าบทพิสูจน์ของเททผิดพลาด น่าแปลกใจว่าไม่มีผู้ใดเห็นข้อผิดพลาดเหล่านี้ในบทพิสูจน์แต่ละอันถึง 11 ปี
ใน พ.ศ. 2433 (ค.ศ. 1890) นอกจากเฮวูดจะชี้ให้เห็นถึงข้อผิดพลาดของบทพิสูจน์ของเคมป์แล้ว เขายังได้พิสูจน์ว่ากราฟเชิงระนาบทุกอันสามารถระบายได้ด้วยสี 5 สี - ดู ทฤษฎีบทห้าสี
ผลงานที่สำคัญได้ถูกสร้างขึ้นโดยนักคณิตศาสตร์ชาวโครเอเชียชื่อ ดานีโล บลานูซา (Danilo Blanuš) ในช่วงปี พ.ศ. 2483-2492 (1940s) โดยการสร้างสนาร์ค (snark) ต้นแบบขึ้น
ในช่วงปี พ.ศ. 2503-2522 (1960s และ 70s) นักคณิตศาสตร์ชาวเยอรมัน ไฮน์ริค ฮีช (Heinrich Heesch) ได้พัฒนาวิธีการในการใช้คอมพิวเตอร์ช่วยหาบทพิสูจน์
ในพ.ศ. 2512 (ค.ศ. 1969) นักคณิตศาสตร์ชาวอังกฤษ จี สเปนเซอร์-บราวน์ (G. Spencer-Brown) อ้างว่าทฤษฎีบทนี้สามารถพิสูจน์ได้ด้วยระบบคณิตศาสตร์ที่เขาได้พัฒนาขึ้นมา อย่างไรก็ตาม เขาไม่เคยสามารถที่จะสร้างบทพิสูจน์นี้ขึ้นมาจริงๆ ได้
จนกระทั่งปี พ.ศ. 2519 (ค.ศ. 1976) นั่นเอง จึงได้มีผู้พิสูจน์ข้อคาดการณ์สี่สีนี้ได้สำเร็จ โดย เคนเน็ท แอพเพล (Kenneth Appel) และ โวล์ฟแกง เฮเคน (Wolfgang Haken) แห่งมหาวิทยาลัยอิลลินอยส์ เออร์บานา-แชมเปญ โดยได้รับคำปรึกษาทางด้านขั้นตอนวิธีจาก เจ คอช (J. Koch)
บทพิสูจน์เริ่มต้นด้วยการลดรูปแบบของแผนที่ทั้งหมดให้เหลือเพียง 1,936 รูปแบบ (และภายหลังสามารถลดลงเหลือ 1,476 รูปแบบ) จากนั้นจึงนำไปตรวจสอบทีละอันด้วยคอมพิวเตอร์ และมีการตรวจสอบซ้ำสองแยกต่างหากโดยโปรแกรมและเครื่องคอมพิวเตอร์ที่ต่างกัน อย่างไรก็ตามบทพิสูจน์นี้มีความยาวถึง 500 หน้า และเต็มไปด้วยตัวอย่างค้านของตัวอย่างค้าน (counter-counter-example) ที่เขียนด้วยมือ โดยส่วนใหญ่เป็นการทดสอบการระบายสีกราฟ ของลูกชายวัยสิบกว่าๆ ของเฮเคน โปรแกรมคอมพิวเตอร์นี้ใช้เวลาทำงานหลายร้อยชั่วโมง
ในปี พ.ศ. 2539 (ค.ศ. 1996) นีล โรเบิร์ตสัน (Neil Robertson) , แดเนียล แซนเดอร์ส (Daniel Sanders) , พอล ซีมัวร์ (Paul Seymour) และ โรบิน โทมัส (Robin Thomas) สร้างบทพิสูจน์ที่คล้ายๆ กัน แต่มีกรณีที่ต้องทดสอบเพียง 633 กรณี บทพิสูจน์อันใหม่นี้ก็ยังจำเป็นต้องใช้คอมพิวเตอร์ช่วย และเป็นการยากที่จะตรวจสอบด้วยคน
ในปี พ.ศ. 2547 (ค.ศ. 2004) เบนจามิน เวอร์เนอร์ (Benjamin Werner) และ จอร์จส์ กอนทิเออร์ (Georges Gonthier) พิสูจน์ทฤษฎีบทนี้ด้วยใช้โปรแกรมพิสูจน์ทฤษฎีบทชื่อ Coq ซึ่งช่วยลดความจำเป็นที่จะต้องเชื่อในความถูกต้องของโปรแกรมหลายๆ โปรแกรม ที่ใช้ในการสอบกรณีแต่ละกรณี — เหลือเพียงแค่ต้องเชื่อใน Coq เท่านั้น
ตั้งแต่ได้มีการพิสูจน์ทฤษฎีบทนี้สำเร็จ ขั้นตอนวิธีที่มีประสิทธิภาพมากมายก็ได้ถูกสร้างขึ้นสำหรับระบายสีแผนที่ด้วนสี่สี โดยทำงานในเวลาเพียง O(n2) เมื่อ n คือจำนวนจุดยอด นอกจากนี้ยังมีขั้นตอนวิธีทรงประสิทธิภาพที่สามารถตรวจสอบได้ว่าแผนที่ใช้สี 1 หรือ 2 สีระบายได้หรือไม่ สำหรับกรณี 3 สีนั้นเป็นปัญหาเอ็นพีสมบูรณ์ และดังนั้นจึงเป็นไปได้สูงว่าจะไม่มีวิธีการเร็วๆ การตรวจสอบว่ากราฟโดยทั่วไป (ไม่จำเป็นต้องเป็นกราฟเชิงระนาบ) สามารถระบายด้วยสี่สีได้หรือไม่ ก็เป็นปัญหาเอ็นพีสมบูรณ์เช่นกัน