14 · บทพิสูจน์ที่ไม่มีใครอ่านจบ
ถ้าคุณนั่งอยู่ในห้องบรรยายที่ Isaac Newton Institute เมืองเคมบริดจ์ ในเดือนมิถุนายน 1993 คุณจะได้เห็น Wiles จบการบรรยายด้วยการบอกว่า ทฤษฎีบทสุดท้ายของแฟร์มาต์พิสูจน์ได้แล้ว ห้องปรบมือให้บทพิสูจน์ที่ยังไม่มีใครในห้องได้ตรวจ
เมื่อบทพิสูจน์ยาวเกินกว่าคนจะอ่านไหว คนตรวจที่ไว้ใจได้ที่สุดคือโปรแกรมที่สั้นพอให้คนอ่านไหว มันคือการย้ายความไว้ใจจากกรรมการที่อ่านไม่จบ ไปไว้ที่โปรแกรมตัวเล็กที่คนอ่านจบได้ และค่าธรรมเนียมมีสองอย่าง โปรแกรมตัวนั้นมีบั๊กได้ และมันไม่ได้ตรวจว่าโจทย์ในเครื่องคือโจทย์ที่คนตั้งใจถาม
proof assistant คือโปรแกรมที่รับบทพิสูจน์ซึ่งเขียนด้วยภาษาเฉพาะ แล้วตรวจทีละขั้นว่าขั้นไหนผิดกฎ Lean เป็นหนึ่งในโปรแกรมแบบนี้ และ kernel คือแกนกลางเล็ก ๆ ข้างในที่เป็นผู้ตัดสินจริง
กรรมการทันบ้าง ไม่ทันบ้าง
ช่วงตรวจในฤดูร้อนปีนั้น Nick Katz เพื่อนร่วมงานของ Wiles ที่ Princeton พบช่องโหว่ Wiles ซ่อมได้ในวันที่ 19 กันยายน 1994 โดยต่อยอดงานที่เคยทำกับ Richard Taylor บทพิสูจน์ลง Annals of Mathematics เดือนพฤษภาคม 1995 คราวนี้กรรมการทัน
ทฤษฎีบทสี่สี ข้อที่ว่าแผนที่ใดก็ใช้สี่สีพอ โชคไม่ดีเท่า บทพิสูจน์ของ Kempe ปี 1879 ผิด และ Heawood จับได้ในอีก 11 ปีต่อมา บทพิสูจน์ที่ยืนได้มาในปี 1976 Appel กับ Haken ลดปัญหาเหลือรูปแบบ 1,936 แล้ว 1,482 แบบ ใช้เวลาคอมพิวเตอร์กว่า 1,200 ชั่วโมง ทศวรรษ 1990 มีทีมลดเหลือ 633 แบบ ปี 2005 Gonthier ให้ proof assistant ชื่อ Coq ตรวจทั้งหมด 10 กันยายน 2026 Quanta Magazine รายงานบทพิสูจน์ใหม่ที่ใช้ 8,202 แบบ ได้วิธีระบายสีที่ใช้ราว n log n ขั้นแทน n² แต่เรียกมันว่า "บทพิสูจน์ด้วยคอมพิวเตอร์อีกชิ้นหนึ่ง" และไม่มีแหล่งไหนบอกว่ามันผ่าน proof assistant แล้ว Thomassen หนึ่งในผู้เขียนบอกว่า "สิ่งที่อยากได้คือบทพิสูจน์ที่ไม่ต้องใช้คอมพิวเตอร์ และจะไม่มีวันหยุดคิดเรื่องนั้น"
สิบสองคน สี่ปี
สิงหาคม 1998 Thomas Hales ประกาศว่าพิสูจน์ข้อคาดการณ์ของ Kepler ได้ Annals รับจะตีพิมพ์ถ้ากรรมการสิบสองคนรับรอง
บันทึกนี้แต่งขึ้น ข้อเท็จจริงทุกข้อในบันทึกเป็นของจริง
สิงหาคม 1998 กระดาษราว 250 หน้า กับโปรแกรมและข้อมูลราว 3 GB ตามที่มีบันทึก สิบสองคนต้องรับรองทั้งหมด
ปีที่สี่ หัวหน้าคณะสรุปส่งวารสาร เรามั่นใจ 99% ส่วนที่คอมพิวเตอร์คำนวณ เรารับรองไม่ได้ สี่ปี สิบสองคน ได้ตัวเลขมาหนึ่งตัว และมันไม่ใช่ร้อย
Annals ตีพิมพ์ปี 2005 โดยไม่มีคำรับรองครบ Hales ไม่รอ ปี 2003 เขาเริ่มโครงการ Flyspeck ให้ HOL Light กับ Isabelle ตรวจทั้งหมด จบวันที่ 10 สิงหาคม 2014 ลง Forum of Mathematics, Pi ปี 2017 สิบหกปีจากวันประกาศ
หนึ่งหมื่นหน้า
การจำแนก finite simple groups ยาวกว่า 10,000 หน้า ในราว 500 บทความ จากผู้เขียนกว่า 100 คน Gorenstein ผู้คุมงานประกาศว่า "ในเดือนกุมภาพันธ์ 1981 การจำแนก finite simple groups เสร็จสมบูรณ์" แล้วก็พบช่องโหว่ ช่องใหญ่ที่สุดกิน Aschbacher กับ Smith เจ็ดปี ปี 2004 Aschbacher เขียนว่าการจำแนก "(สำหรับตอนนี้)" ถือเป็นทฤษฎีบทได้ ซ่อมเสร็จแล้วยังขอวงเล็บไว้ Plus เขียนว่าไม่มีใครในโลกเข้าใจบทพิสูจน์นี้ครบ ผู้แสดงความเห็นที่ระบุตัวว่าเป็น Ron Solomon แย้งว่ามีอย่างน้อยสามคนที่เข้าใจ "อย่างน้อยดีเท่ากับที่ Danny Gorenstein เข้าใจ"
ทฤษฎีบทในเคียวโต
สิงหาคม 2012 Shinichi Mochizuki เผยแพร่ทฤษฎี IUT ยาวกว่า 500 หน้า อ้างว่าพิสูจน์ abc conjecture ได้ ปี 2018 Peter Scholze กับ Jakob Stix เขียนรายงาน Why abc is still a conjecture ชี้ไปที่ Corollary 3.12 Stix เรียกช่องโหว่ว่า "ร้ายแรง แก้ไม่ได้" Mochizuki ตอบว่ามาจาก "ความเข้าใจผิดพื้นฐานบางประการ" Calegari สรุปว่า "abc เป็นทฤษฎีบทในเคียวโต แต่เป็นข้อคาดการณ์ที่อื่นทุกแห่ง"
ปี 2021 งานลงวารสาร PRIMS ที่ Mochizuki เป็นบรรณาธิการบริหาร ส่วนเขาถอนตัวหรือไม่ เล่มนี้ไม่พบหลักฐาน ปี 2023 Nobuo Kawakami ผู้ก่อตั้ง Dwango ตั้ง IUT Challenger Prize หนึ่งล้านดอลลาร์ ให้บทความแรกที่ผ่าน peer review และชี้ "ข้อบกพร่องสำคัญ" ใน IUT ได้ รางวัลของการหักล้าง ไม่ใช่การพิสูจน์ โครงการ LANA ที่เขียน IUT ลง Lean รายงานเดือนกรกฎาคม 2026 ว่ายัง "ไม่ให้คำตัดสินสุดท้าย" สถานะวันนี้ งานลงวารสารแล้ว นักทฤษฎีจำนวนวงกว้างยังไม่ยอมรับ ไม่มีการหักล้างหรือยืนยันที่วงการรับ และ Lean ยังปิดขั้นที่เถียงกันไม่ได้
99.9% ไม่พอ
ธันวาคม 2020 Scholze ท้าบนบล็อกของ Kevin Buzzard ให้เขียนทฤษฎีบทหนึ่งของเขาลง Lean เพราะ "ทฤษฎีบทนี้สำคัญต่อรากฐานอย่างยิ่ง การมั่นใจ 99.9% จึงไม่พอ" และเพราะ "ในการสอบคัดเลือกเข้าโอลิมปิกคณิตศาสตร์ระหว่างประเทศ ฉันได้คะแนนเต็มจากคำตอบที่ผิดถึงสองครั้ง" ทีมของ Johan Commelin ทำเสร็จวันที่ 14 กรกฎาคม 2022 แต่ Scholze ชี้ขอบไว้เอง การตรวจว่าโจทย์ในเครื่องคือโจทย์ที่ถูก "ยังเป็นสิ่งที่มนุษย์ต้องทำ" และตราประทับเหมาว่าถูกทั้งหมดจะทำให้เขา "ระแวงอย่างยิ่ง" เพราะแน่ใจว่าตัวเองพลาดไว้บ้าง Equational Theories Project ของ Terence Tao ก็มีขอบเดียวกัน เมษายน 2025 Lean ยืนยันความสัมพันธ์ครบ 22,028,942 คู่ แต่ยืนยันตามนิยามที่คนพิมพ์ใส่ไว้
ตัวตรวจก็มีบั๊ก
หลักนี้เรียกว่า de Bruijn criterion ตามชื่อ N. G. de Bruijn ตัวตรวจต้องเล็กและอิสระพอให้คนขี้สงสัยอ่านเองหรือเขียนเองได้ ใน Lean ตัวนี้คือ kernel
25 กรกฎาคม 2026 Ramana Kumar เผยแพร่ "บทหักล้าง" ข้อคาดการณ์ Collatz ที่ทำด้วยความช่วยเหลือของ AI Lean รับไว้เพราะบั๊กใน kernel และ nanoda ตัวตรวจอิสระรุ่นเก่าหนึ่งสัปดาห์ก็รับ ด้วยบั๊กอีกตัว 28 กรกฎาคม Kiran Gopinathan ย่อมันเหลือบทพิสูจน์สั้น ๆ ว่า False เป็นจริง และเปิดบั๊กหมายเลข 14576 ทีม Lean ส่งโค้ดแก้ในหนึ่งชั่วโมง de Moura ผู้สร้าง Lean เขียนว่า "นี่คือบั๊กของตัวโปรแกรม ไม่ใช่รูในทฤษฎีของ Lean" และการตรวจด้วย kernel อิสระยังใช้ได้ เพราะของปลอมต้องอาศัยบั๊กสองตัวในโปรแกรมสองตัว ขอแค่ใช้รุ่นล่าสุดของทั้งคู่
เครื่องเขียน คนอ่านโจทย์
ปี 2025 Gemini Deep Think ของ Google ได้คะแนนระดับเหรียญทอง IMO ด้วยบทพิสูจน์ภาษาธรรมดาที่กรรมการ IMO ให้คะแนน ปี 2026 ปัญหา Erdős ข้อ 728 ได้บทพิสูจน์ใน Lean ที่ผู้เขียน "ถือได้ว่า" AI แก้ได้เอง และ DeepMind รายงานว่าแก้ข้อที่ยังเปิดอยู่ได้ 9 จาก 353 ข้อ
4 กันยายน 2026 Anthropic รายงานว่า Claude ทำงานแทบเองทั้งหมด 11 วัน เขียนบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ลง Lean ยาว 13 ล้านบรรทัด ผู้เขียนเล่มนี้เป็นโมเดลที่บริษัทเดียวกันสร้าง จึงพิมพ์ผลนี้คู่กับการตรวจของคนนอกเท่านั้น Buzzard คอมไพล์และรันโปรแกรมเทียบโจทย์เอง แล้วเขียนว่า "ในทางคณิตศาสตร์ งานนี้ของ anthropic แทบไม่บอกอะไรเราเลย ฉันพูดไว้แล้วว่ามั่นใจ 99.9% ว่าบทพิสูจน์ FLT ไม่มีปัญหา"
ห้องที่เคมบริดจ์ได้ฟังบทพิสูจน์ที่ยังไม่มีใครภายนอกได้ตรวจ สามสิบสามปีต่อมา ทฤษฎีบทเดียวกันยาวสิบสามล้านบรรทัดถูกเครื่องตรวจจนจบ และคนนอกก็ยังต้องตรวจซ้ำเอง เพราะเครื่องตรวจก็มีบั๊ก และคนยังต้องอ่านโจทย์
บทถัดไป · 16 / 2015 The Apprenticeช่วงพากย์ · นัดที่ 14 · ห้องตรวจบทพิสูจน์ ปี 1993–2026
น้าไว: สิบสามล้านบรรทัดครับ เครื่องตรวจผ่านหมดทุกบรรทัด!
อาจารย์ช้า: อาจารย์ไม่อ่านสิบสามล้านบรรทัดครับ อ่านแค่ตัวตรวจ กับโจทย์บรรทัดเดียว
น้าไว: แล้วถ้าตัวตรวจมีบั๊กล่ะครับ
อาจารย์ช้า: ปีนี้มีแล้ว จับได้ในสามวันครับ อาจารย์เริ่มเร็วขึ้นแล้วนะน้า แต่มั่นใจได้แค่เก้าสิบเก้าจุดเก้า ซึ่งมีคนบอกไว้แล้วว่าไม่พอ
สกอร์บอร์ด
อายุของปลอม: บทนี้ไม่มีคนปลอม มีแต่ข้ออ้างที่ยังตรวจไม่จบ ทางพิสูจน์ abc ค้างมาตั้งแต่ 2012 ถึง 2026
การตรวจที่จับได้ใช้เวลา: Kepler ใช้ 16 ปีจากวันประกาศถึงวันที่เครื่องตรวจจบ
แบบของการตรวจไม่ทัน: ตรวจแพง