เคนเนธ แอปเพล: ผู้เปิดศึกคอมพิวเตอร์กับการพิสูจน์ทางคณิตศาสตร์

Kenneth Appel (1932–2013)

นักคณิตศาสตร์ชาวอเมริกันผู้ร่วมพิสูจน์ทฤษฎีบทสี่สี (Four Color Theorem) กับวูล์ฟกัง ฮาเคิน (Wolfgang Haken) ในปี 1976 ซึ่งเป็นการพิสูจน์ทฤษฎีบทสำคัญครั้งแรกในประวัติศาสตร์ที่ต้องอาศัยคอมพิวเตอร์ช่วยตรวจสอบกรณีย่อยนับพันกรณี และจุดชนวนการถกเถียงครั้งใหญ่ในวงการคณิตศาสตร์ว่า “การพิสูจน์ด้วยคอมพิวเตอร์” นับเป็นการพิสูจน์ที่แท้จริงหรือไม่

ชีวิตช่วงต้นในบรูคลิน

เคนเนธ แอปเพล เกิดเมื่อวันที่ 8 ตุลาคม ค.ศ. 1932 ที่เมืองบรูคลิน นครนิวยอร์ก เป็นบุตรของเออร์วิน แอปเพลและลิลเลียน เซนเดอร์ ครอบครัวย้ายไปอยู่ที่ควีนส์หลังปี 1935 เขาสำเร็จการศึกษาระดับปริญญาตรีสาขาคณิตศาสตร์จากวิทยาลัยควีนส์ในปี 1953 จากนั้นรับราชการทหารในกองทัพสหรัฐฯ เป็นเวลาสองปี รวมถึงประจำการอยู่ที่เยอรมนีช่วงหนึ่ง ก่อนจะเข้าศึกษาต่อที่มหาวิทยาลัยมิชิแกน และได้รับปริญญาโทในปี 1956 และปริญญาเอกในปี 1959 โดยมีโรเจอร์ ลินดอน (Roger Lyndon) เป็นอาจารย์ที่ปรึกษา

เส้นทางสู่มหาวิทยาลัยอิลลินอยส์

หลังสำเร็จการศึกษา แอปเพลทำงานอยู่ที่ Institute for Defense Analyses ในพรินซ์ตันเป็นเวลาสองปี โดยทำงานด้านวิทยาการเข้ารหัส (cryptography) ก่อนจะย้ายไปรับตำแหน่งผู้ช่วยศาสตราจารย์ที่มหาวิทยาลัยอิลลินอยส์ เออร์แบนา-แชมเปญในปี 1961 ซึ่งเขาทำงานวิจัยด้านทฤษฎีกรุป (group theory) และทฤษฎีการคำนวณได้ (computability theory) และที่นี่เองที่เขาได้พบกับวูล์ฟกัง ฮาเคิน เพื่อนร่วมงานซึ่งจะกลายเป็นผู้ร่วมพิสูจน์ทฤษฎีบทที่สร้างชื่อให้เขาไปตลอดกาล

ทฤษฎีบทสี่สีที่ท้าทายมากว่าศตวรรษ

ทฤษฎีบทสี่สีเป็นปัญหาที่ตั้งคำถามมาตั้งแต่ปี 1852 ว่า แผนที่ระนาบใด ๆ ที่แบ่งเป็นภูมิภาคต่าง ๆ สามารถระบายสีได้ด้วยสีเพียงสี่สี โดยที่ภูมิภาคที่มีขอบเขตติดกันจะต้องมีสีต่างกันเสมอ ใช่หรือไม่ ปัญหานี้ดูเรียบง่ายในการตั้งคำถาม แต่กลับยากอย่างยิ่งในการพิสูจน์ และท้าทายนักคณิตศาสตร์ชั้นนำมานานกว่าหนึ่งศตวรรษโดยไม่มีใครพิสูจน์ได้สำเร็จ

แอปเพลและฮาเคินร่วมมือกันพัฒนาวิธีการที่สืบทอดมาจากแนวทางของอัลเฟรด เคมป์ (Alfred Kempe) ในศตวรรษที่ 19 โดยลดรูปปัญหาให้เหลือเพียงการตรวจสอบโครงแบบ (configuration) จำนวนจำกัดที่ “ลดทอนไม่ได้” (unavoidable) ซึ่งหากพิสูจน์ได้ว่าแต่ละโครงแบบเหล่านี้ระบายสีได้ด้วยสี่สีเสมอ ก็เท่ากับพิสูจน์ทฤษฎีบทสี่สีได้โดยสมบูรณ์

การพิสูจน์ด้วยคอมพิวเตอร์ครั้งแรกของประวัติศาสตร์

ปัญหาคือจำนวนโครงแบบที่ต้องตรวจสอบมีมากถึงราว 1,936 กรณี ซึ่งเกินกว่าที่มนุษย์จะตรวจสอบด้วยมือได้ในเวลาอันสมควร แอปเพลและฮาเคินจึงใช้คอมพิวเตอร์ของมหาวิทยาลัยอิลลินอยส์ช่วยตรวจสอบกรณีย่อยเหล่านี้ทั้งหมด โดยใช้เวลาประมวลผลรวมกว่า 1,200 ชั่วโมง พวกเขาตีพิมพ์ขั้นตอนแรกของบทพิสูจน์ในปี 1976 และตีพิมพ์บทพิสูจน์ฉบับสมบูรณ์เป็นบทความสองชิ้นในปี 1977 ก่อนจะรวบรวมรายละเอียดทั้งหมดไว้ในหนังสือที่ตีพิมพ์ในปี 1989 ผลงานนี้ทำให้ทั้งคู่ได้รับรางวัล Delbert Ray Fulkerson Prize ร่วมกันในปี 1979

นี่คือการพิสูจน์ทฤษฎีบทสำคัญทางคณิตศาสตร์ครั้งแรกในประวัติศาสตร์ที่ต้องพึ่งพาการประมวลผลของคอมพิวเตอร์อย่างขาดไม่ได้ ไม่ใช่เพียงเครื่องมือช่วยคำนวณเสริม แต่เป็นส่วนหนึ่งที่จำเป็นของตัวบทพิสูจน์เอง

ข้อถกเถียงเรื่องความแท้จริงของการพิสูจน์

การพิสูจน์ของแอปเพลและฮาเคินจุดชนวนการถกเถียงครั้งใหญ่ในวงการคณิตศาสตร์ เพราะเป็นครั้งแรกที่มนุษย์ไม่สามารถตรวจสอบบทพิสูจน์ทั้งหมดด้วยตาเปล่าได้ นักคณิตศาสตร์หลายคนตั้งคำถามว่า บทพิสูจน์ที่พึ่งพาการตรวจสอบของเครื่องจักรซึ่งมนุษย์ไม่สามารถตรวจทานได้ทุกขั้นตอน จะถือเป็น “การพิสูจน์ที่แท้จริง” ในความหมายดั้งเดิมของคณิตศาสตร์ได้หรือไม่ เพราะแนวคิดเรื่องการพิสูจน์มาแต่ดั้งเดิมนั้นต้องสามารถให้มนุษย์ตรวจสอบทีละขั้นตอนได้อย่างสมบูรณ์

แม้แต่แอปเพลเองก็ยอมรับถึงความกังวลนี้ ในปี 1984 เขากล่าวว่านักคณิตศาสตร์ส่วนใหญ่อาจไม่รู้สึกเชื่อมั่นอย่างสมบูรณ์กับผลลัพธ์ก่อนหน้านี้ของเขาด้านทฤษฎีกรุปที่ใช้คอมพิวเตอร์ช่วยพิสูจน์เช่นกัน เรื่องที่น่าสนใจคือ ในกระบวนการตรวจสอบความถูกต้องของบทพิสูจน์ทฤษฎีบทสี่สี ลูก ๆ ของแอปเพลยังช่วยตรวจทานแผนภาพต่าง ๆ ด้วยมือ โดยลอเรล บุตรสาวของเขาพบข้อผิดพลาดเล็ก ๆ น้อย ๆ ในแผนภาพมากถึงราว 800 จุด ซึ่งภายหลังได้รับการแก้ไขจนครบถ้วน

ข้อถกเถียงเรื่องความชอบธรรมของการพิสูจน์ด้วยคอมพิวเตอร์ที่เริ่มต้นจากผลงานของแอปเพลและฮาเคินนี้ ได้กลายเป็นประเด็นปรัชญาคณิตศาสตร์ที่สำคัญมาจนถึงปัจจุบัน และปูทางให้เกิดการพัฒนาเครื่องมือพิสูจน์เชิงรูปนัย (formal proof assistant) อย่าง Coq และ Lean ในเวลาต่อมา ซึ่งช่วยให้คอมพิวเตอร์ตรวจสอบความถูกต้องของบทพิสูจน์ได้อย่างเข้มงวดและน่าเชื่อถือมากยิ่งขึ้น

ชีวิตในบั้นปลาย

แอปเพลดำรงตำแหน่งหัวหน้าภาควิชาคณิตศาสตร์ที่มหาวิทยาลัยนิวแฮมป์เชียร์ตั้งแต่ปี 1993 และเกษียณอายุในปี 2003 ในฐานะศาสตราจารย์กิตติคุณ หลังเกษียณเขายังคงทำงานอาสาสมัครสอนคณิตศาสตร์และให้บริการสาธารณะในเมืองโดเวอร์ รัฐนิวแฮมป์เชียร์ อย่างต่อเนื่อง

แอปเพลได้รับการวินิจฉัยว่าเป็นมะเร็งหลอดอาหารในเดือนตุลาคม 2012 และเสียชีวิตเมื่อวันที่ 19 เมษายน ค.ศ. 2013 ที่เมืองโดเวอร์ รัฐนิวแฮมป์เชียร์ ขณะอายุ 80 ปี เพียงประมาณหนึ่งเดือนหลังจากลอเรล บุตรสาวของเขาเสียชีวิตลง เพื่อนร่วมงานคนหนึ่งบรรยายถึงเขาว่าเป็น “คนที่มีความอ่อนน้อมถ่อมตนอย่างเหลือเชื่อ”

มรดกที่ทิ้งไว้

ผลงานของเคนเนธ แอปเพลและวูล์ฟกัง ฮาเคินไม่เพียงไขปริศนาทฤษฎีบทสี่สีที่ค้างคามานานกว่าศตวรรษ แต่ยังเปลี่ยนวิธีคิดของวงการคณิตศาสตร์ต่อบทบาทของคอมพิวเตอร์ในการพิสูจน์ทฤษฎีบทไปอย่างสิ้นเชิง ทุกวันนี้การพิสูจน์ด้วยคอมพิวเตอร์กลายเป็นเรื่องปรกติในหลายสาขาของคณิตศาสตร์ ตั้งแต่การพิสูจน์ข้อความคาดการณ์เคปเลอร์ (Kepler conjecture) ไปจนถึงการตรวจสอบบทพิสูจน์ที่ซับซ้อนด้วยซอฟต์แวร์พิสูจน์เชิงรูปนัย ซึ่งทั้งหมดนี้มีรากฐานย้อนไปถึงความกล้าหาญทางปัญญาของแอปเพลและฮาเคินที่ยอมเผชิญหน้ากับคำถามว่า “การพิสูจน์คืออะไร” เป็นครั้งแรกในประวัติศาสตร์คณิตศาสตร์สมัยใหม่