ผลต่างระหว่างรุ่นของ "ทฤษฎีบทสี่สี"
เนื้อหาที่ลบ เนื้อหาที่เพิ่ม
บรรทัด 89:
== บทพิสูจน์ที่สำเร็จ: สี่สีก็เพียงพอ ==
หลังจากความพยายามที่ล้มเหลวนับครั้งไม่ถ้วนของนักคณิตศาสตร์จำนวนมาก ในที่สุดทฤษฎีบทนี้ก็ได้รับการพิสูจน์โดย[[เคนเน็ท แอพเพล]] (Kenneth Appel) และ[[โวล์ฟแกง เฮเคน]] (Wolfgang Haken) โดยได้ประกาศต่อสาธารณะใน[[วันที่ 22 กรกฎาคม]] [[พ.ศ. 2519]] (ค.ศ.1976)และตีพิมพ์ในปี[[พ.ศ.2520]]
บทพิสูจน์นี้ไม่ได้ง่ายนัก เนื่องจากต้องใช้เวลาในการคำนวณด้วยคอมพิวเตอร์(ในยุค[[พ.ศ.2520]]นับพันชั่วโมง เพื่อตรวจสอบกรณีเฉพาะถึง 100,000 กรณี วิธีการนี้ไม่เป็นที่ยอมรับสำหรับนักคณิตศาสตร์บางคน เนื่องจากบทพิสูจน์ไม่สามารถตรวจสอบได้ แต่ก็มีคำถามว่า แล้วบทพิสูจน์ที่ยาวนับพันหน้านั้นสามารถตรวจสอบได้หรือ?
สิ่งสำคัญที่บทพิสูจน์นี้ไม่ได้ให้ก็คือ ความเข้าใจลึกซึ้งว่าทำไมข้อความคาดการณ์นี้จึงเป็นจริง ทฤษฎีอาจจะจริง แต่มันไม่สามารถนำมาอธิบายได้ นี่เป็นอีกผลหนึ่ง(ซึ่งมีน้ำหนักมาก)ของคำวิจารณ์ว่าบทพิสูจน์ขาดสง่างาม
ในปี [[พ.ศ.2547]] [[เบนจามิน เวอร์เนอร์]] (Benjamin Werner) และ [[จอร์จส์ กอนทิเออร์]] (Georges Gonthier) พิสูจน์ทฤษฎีบทนี้ด้วยใช้โปรแกรมพิสูจน์ทฤษฎีบทชื่อ [[Coq]] ซึ่งช่วยลดความจำเป็นที่จะต้องเชื่อในความถูกต้องของโปรแกรมหลาย ๆ โปรแกรม ที่ใช้ในการสอบกรณีแต่ละกรณี — เหลือเพียงแค่ต้องเชื่อใน Coq เท่านั้น
==หัวข้อที่เกี่ยวข้อง==
| |||