ผลต่างระหว่างรุ่นของ "ทฤษฎีบทสี่สี"

เนื้อหาที่ลบ เนื้อหาที่เพิ่ม
Danupon (คุย | ส่วนร่วม)
Danupon (คุย | ส่วนร่วม)
→‎ประวัติ: - ใส่ ค.ศ. เพื่อสะดวกในการลำดับเวลาเทียบกับเหตุการณ์สากล
บรรทัด 10:
 
==ประวัติ==
ข้อความคาดการณ์อันนี้ถูกกล่าวถึงครั้งแรกในปี [[พ.ศ.2395]] (1852) เมื่อ [[ฟรานซิส กูทรี]] (Francis Guthrie) ได้สังเกตเห็นว่าสามารถใช้เพียงสี่สีก็เพียงพอในการระบาย ขณะที่กำลังระบายแผนที่ของเขตหนึ่งใน[[แคว้นอังกฤษ|อังกฤษ]] ในขณะนั้นกูทรีเป็นลูกศิษย์ของ [[ออกัสตัส เดอ มอร์แกน]] (Augustus De Morgan) ที่ [[วิทยาลัยยูนิเวอร์ซิตี้ลอนดอน]] (University College London) (กูทรีจบการศึกษาในปี [[พ.ศ.2393]](1850) และต่อมาได้เป็นศาสตราจารย์สาขาคณิตศาสตร์ใน[[ประเทศแอฟริกาใต้]]) โดยตามคำบอกเล่าของเดอร์มอร์แกน:
 
:''วันนี้ลูกศิษย์ของผมคนหนึ่ง'' [[กูทรี]] ''ขอให้ผมช่วยให้เหตุผลของความจริงอันหนึ่ง-ทั้งที่ผมก็ยังไม่รู้จนถึงบัดนี้เลยว่ามันเป็นความจริง เขาบอกว่า ไม่ว่าเราจะแบ่งรูปออกเป็นส่วนๆในลักษณะใดก็ตาม แล้วระบายสีแต่ละส่วนโดยให้ส่วนที่มีขอบร่วมกันเป็นคนละสีกัน แล้วมันเพียงพอที่จะใช้สีเพียงสี่สี กรณีต่อไปนี้คือกรณีที่ต้องการสี่สีพอดี เรายังไม่สามารถหากรณีที่ต้องการห้าสีหรือมากกว่านั้นได้ ...''
บรรทัด 16:
หลักฐานอ้างอิงที่มีการตีพิมพ์เป็นอันแรกถูกพบในงานของ [[อาร์เทอร์ เคย์เลย์]] (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) ต้นแบบขึ้น
บรรทัด 24:
ในช่วงปี [[พ.ศ.2503-2522]] (1960s และ 70s) นักคณิตศาสตร์ชาว[[ประเทศเยอรมนี|เยอรมัน]] [[ไฮน์ริค ฮีช]] (Heinrich Heesch) ได้พัฒนาวิธีการในการใช้[[คอมพิวเตอร์]]ช่วยหาบทพิสูจน์
 
ใน[[พ.ศ.2512]](1969) นักคณิตศาสตร์[[แคว้นอังกฤษ|ชาวอังกฤษ]] [[จี สเปนเซอร์-บราวน์]] (G. Spencer-Brown) อ้างว่าทฤษฎีบทนี้สามารถพิสูจน์ได้ด้วย[[กฏของรูปแบบ|ระบบคณิตศาสตร์ที่เขาได้พัฒนาขึ้นมา]] อย่างไรก็ตาม เขาไม่เคยสามารถที่จะสร้างบทพิสูจน์นี้ขึ้นมาจริง ๆ ได้
 
จนกระทั่งปี [[พ.ศ.25162519]](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(''n''<sup>2</sup>) เมื่อ ''n'' คือจำนวนจุดยอด นอกจากนี้ยังมีอัลกอริทึมทรงประสิทธิภาพที่สามารถตรวจสอบได้ว่าแผนที่ใช้สี 1 หรือ 2 สีระบายได้หรือไม่ สำหรับกรณี 3 สีนั้นเป็นปัญหา[[เอ็นพีสมบูรณ์]] และดังนั้นจึงเป็นไปได้สูงว่าจะไม่มีวิธีการเร็ว ๆ การตรวจสอบว่ากราฟโดยทั่วไป (ไม่จำเป็นต้องเป็นกราฟเชิงระนาบ) สามารถระบายด้วยสี่สีได้หรือไม่ ก็เป็นปัญหา[[เอ็นพีสมบูรณ์]]เช่นกัน