Table of Content
การพิสูจน์ทางคณิตศาสตร์ - ใช้คอมหรือใช้คน
Table of Content
ถ้าใครเป็นคนที่รักในคณิตศาสตร์บริสุทธิ์ หรือเคยได้เข้าค่าย สอวน. คณิตศาสตร์มาก่อน น่าจะคุ้นเคยกับการพิสูจน์ทางคณิตศาสตร์เป็นอย่างดี
การพิสูจน์ทางคณิตศาสตร์โดยส่วนใหญ่นั้นมักจะพิสูจน์โดยนักคณิตศาสตร์ซึ่งเป็นมนุษย์ ร้อยเรียงเป็นข้อเหตุผลลงมา ด้วยความที่คณิตศาสตร์มีหลักเกณฑ์ที่ค่อนข้างชัดเจนอยู่แล้ว หากพิสูจน์ด้วยเหตุและผลที่ตรงไปตรงมา และไม่คิดอะไรผิดพลาด การพิสูจน์นั้นก็จะเป็นที่ยอมรับโดยสมาคมชาวคณิตศาสตร์เองแบบที่ไม่ต้องมีการทดลองซ้ำอะไรอีกเหมือนกับการทดลองทางวิทยาศาสตร์
แต่ถ้าข้อพิสูจน์ทางคณิตศาสตร์นั้นเป็นการพิสูจน์โดยใช้คอมพิวเตอร์เข้าช่วย เราจะยังเชื่อถือการพิสูจน์นั้นได้อยู่หรือไม่
ทฤษฎีบทที่ได้รับความสนใจชิ้นแรก ๆ ที่ได้รับการพิสูจน์ด้วยคอมพิวเตอร์ เป็นทฤษฎีบทที่ชื่อว่า “Four color theorem” ซึ่งย่อเป็นภาษาคนได้ว่า “ถ้าเรามีแผนที่ที่แบ่งเขตแดนต่าง ๆ แล้ว เราสามารถใช้สีเพียงแค่สี่สีเท่านั้นในการระบายเขตแดนต่าง ๆ โดยที่เขตแดนที่ติดกันจะไม่มีสีที่ซ้ำกันเลย”
ข้อคาดการณ์นี้ถูกเสนอขึ้นเป็นครั้งแรกในปี 1852 โดย Francis Guthrie ตอนที่เขากำลังจะระบายสีประเทศอังกฤษ ก่อนที่จะพบว่าเขาใช้เพียงแค่สี่สีก็พอแล้ว ต่อมาก็มีความพยายามของนักคณิตศาสตร์หลายคนที่ต้องการจะพิสูจน์ทฤษฎีบทนี้ แต่ความพยายามทั้งหลายก็ไม่สำเร็จ
ล่วงเลยมาถึงหนึ่งศตวรรษ ในช่วงเวลาที่ระบบคอมพิวเตอร์เพิ่งจะเริ่มบุกเบิก ในปี 1976 นักคณิตศาสตร์สองท่านจากมหาวิทยาลัยอิลลินอยส์นามว่า Kenneth Appel และ Wolfgang Haken ก็ร่วมกันใช้คอมพิวเตอร์ในการพิสูจน์ทฤษฎีบทดังกล่าว ซึ่งพวกเขาลดกรณีของการพิสูจน์ลงเหลือประมาณ 1,834 กรณี และใช้คอมพิวเตอร์ในการพิสูจน์แต่ละกรณีนั้นนานถึงกว่าพันชั่วโมง (หรือกว่า 40 วัน ถ้าปล่อยให้เครื่องทำงานข้ามวันข้ามคืน) การพิสูจน์ดังกล่าวถูกพิมพ์ออกมาลงบนกระดาษที่ยาวกว่า 400 หน้า และได้ให้ Dorothea Blostein ซึ่งเป็นลูกสาวของ Haken ช่วยเช็คความถูกต้อง
การเสนอข้อพิสูจน์ดังกล่าวกลายเป็นเรื่องร้อนแรงในวงการคณิตศาสตร์ เพราะไม่เคยมีครั้งไหนมาก่อนเลยที่ทฤษฎีบททางคณิตศาสตร์จะได้รับการพิสูจน์แบบที่มนุษย์เองก็น่าจะตรวจไม่ไหว นักประวัติศาสตร์คณิตศาสตร์อย่าง David Burton ก็ได้ให้ข้อคิดเห็นว่า “… ข้อพิสูจน์ทางคณิตศาสตร์ที่ให้คอมพิวเตอร์ทำให้นั้นจะทำให้ข้อพิสูจน์นั้นยังถูกเปิดให้คนเข้ามาตรวจและแก้ไขได้อยู่”
แม้ว่าในทางปฏิบัติ ข้อพิสูจน์ทฤษฎีบทดังกล่าวจะได้รับการยอมรับโดยทั่วไปแล้วก็ตาม แต่ก็ยังมีความพยายามในการพัฒนาข้อพิสูจน์อยู่ โดยในปี 1996 ทีมนักคณิตศาสตร์ได้แก่ Neil Robertson, Daniel P. Sanders, Paul Seymour และ Robin Thomas ได้ลดกรณีการพิสูจน์ลงเหลือเพียง 633 กรณี และต่อมาในปี 2005, Benjamin Werner และ Georges Gonthier ก็ได้ใช้ Coq proof assistant ในการพิสูจน์ทฤษฎีบทดังกล่าว เพื่อแก้ไขปัญหาเรื่องความเชื่อใจ (trust) โปรแกรมคอมพิวเตอร์ที่หลากหลายในการแก้ปัญหาทฤษฎีบทแต่ละกรณี
เมื่อเวลาผ่านไป คอมพิวเตอร์มีความเร็วมากขึ้น การแก้ปัญหาที่มีหลายกรณีมาก ๆ แล้วใช้คอมพิวเตอร์ในการแก้จึงได้รับความนิยมมากขึ้น ปัญหาต่าง ๆ นี้เช่น
- การทำให้ลูกบิดกลับมามีหน้าหกหน้าที่เหมือนเดิม ใช้ face move มากสุดเพียงแค่ 20 ครั้ง (ปี 2010)
- คำใบ้ใน Sudoku ที่น้อยที่สุดเท่าที่จะทำให้แก้ได้คือให้แค่ 17 ช่อง (ปี 2012)
- Schur’s theorem ใช้หน่วยความจำถึง 2 petabytes ในการพิสูจน์ (ปี 2017)
ที่มา: