การแปลงบทพิสูจน์ครั้งประวัติศาสตร์: 13 ล้านบรรทัดโค้ดของ Lean 4

Anthropic ได้เปิดตัวผลงานวิจัยสำคัญอย่างเป็นทางการสู่สาธารณะเมื่อวันที่ 4–5 กันยายน 2026 โดยเป็นคลังโค้ดการแปลงบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ (Fermat's Last Theorem หรือ FLT) สู่ระบบภาษาพิสูจน์เชิงตรรกะคอมพิวเตอร์ Lean 4 ที่ผ่านการตรวจสอบความถูกต้องโดยสมบูรณ์ โครงการนี้ถือเป็นบทพิสูจน์ในระบบ Lean ที่มีขนาดใหญ่ที่สุดเท่าที่เคยมีการสร้างขึ้นมาในประวัติศาสตร์ โดยมีขอบเขตโค้ดรวมประมาณ 13 ล้านบรรทัด (หรือประมาณ 10.5 ล้านบรรทัดหากตัดส่วนโค้ดสำเร็จรูปที่สร้างแบบ boilerplate ออก)

โครงสร้างของผลงานชิ้นนี้ประกอบด้วย 60,475 โมดูล และสามารถพิสูจน์ทฤษฎีบทย่อยขั้นกลาง (intermediate theorems) ได้ถึง 29,511 รายการ พร้อมบทตั้งเฉพาะที่ (local lemmas) ราว 533,000 รายการ โดยการประมวลผลจริงเริ่มต้นขึ้นในช่วงเช้ามืดของวันที่ 7 สิงหาคม 2026 และใช้เวลาทำงานต่อเนื่องประมาณ 11 วัน จนเสร็จสิ้นการพิสูจน์ทฤษฎีบทสุดท้ายในวันที่ 17 สิงหาคม 2026

กระบวนการพิสูจน์นี้อ้างอิงตามแนวทางการพิสูจน์ของ Darmon–Diamond–Taylor ในปี 1995 ซึ่งเป็นการขยายและจัดระเบียบโครงสร้างข้อพิสูจน์ Frey–Ribet–Wiles–Taylor เดิม โดยโครงการนี้พัฒนาต่อยอดจากคลัง `mathlib` (อิงเวอร์ชัน Lean 4.33.1 และ Mathlib v4.33.0) พร้อมทั้งนำเข้าและปรับปรุงไฟล์ 106 ไฟล์จากโครงการ FLT ของ Imperial College London ภายใต้การนำของ Kevin Buzzard ตลอดจนคลัง `flt-regular`

ความสมบูรณ์เชิงตรรกะและสถาปัตยกรรมตัวแทน Claude

จุดเด่นทางวิศวกรรมที่สำคัญที่สุดของงานวิจัยนี้คือความสมบูรณ์แบบของหลักฐานทางตรรกะ (soundness) โดยเคอร์เนลหลักของ Lean ตรวจสอบโค้ดทั้งหมดผ่านเกณฑ์มาตรฐานอย่างเข้มงวด อิงตามสัจพจน์พื้นฐานมาตรฐานเพียงสามข้อของ Lean ได้แก่ `propext`, `Classical.choice` และ `Quot.sound` โดยไม่มีการละเว้นส่วนใดของบทพิสูจน์ด้วยคำสั่ง `sorry` ไม่มีสัจพจน์แปลกปลอมที่ยังไม่ได้รับการพิสูจน์ และไม่มีการหลบเลี่ยงการตรวจสอบผ่าน `native_decide`

นอกจากนี้ เพื่อกำจัดข้อสงสัยเกี่ยวกับความถูกต้องของคอมไพเลอร์ เคอร์เนลอิสระภายนอกอย่าง `nanoda` เวอร์ชัน 0.4.13 ซึ่งเขียนขึ้นด้วยภาษา Rust ได้ทำการตรวจสอบและยอมรับการประกาศนิยามทั้งหมด 1,052,234 รายการโดยไม่พบข้อผิดพลาดแม้แต่จุดเดียว พร้อมทั้งผ่านบททดสอบความเข้ากันได้ตามมาตรฐาน `leanprover/comparator` อีกด้วย

เบื้องหลังการดำเนินการนี้ ขับเคลื่อนโดยตัวแทน Claude หลายสิบอินสแตนซ์ที่ทำงานร่วมกันผ่านแพลตฟอร์มพิสูจน์ทฤษฎีบทแบบทำงานร่วมกันชื่อ Prove2Me ซึ่งพัฒนาโดยทีมของ Tianyi Peng นักวิจัยของ Anthropic ร่วมกับมหาวิทยาลัยโคลัมเบีย ทั้งนี้ โครงการใช้โทเคนขาออก (output tokens) ไปทั้งสิ้นประมาณ 6,000 ล้านโทเคน จากโมเดลวิจัยภายในองค์กรที่มีประสิทธิภาพใกล้เคียงกับ Claude Fable 5.1

มุมมองของชุมชนนักพัฒนา: ระหว่างก้าวสำคัญของวงการกับปัญหาโค้ดเทอะทะ

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

อย่างไรก็ตาม ผู้ดูแลคลังโค้ดคณิตศาสตร์และนักพัฒนาระบบ Lean ได้แสดงข้อกังขาเกี่ยวกับความคุ้มค่าในการนำโค้ดไปใช้งานต่อ (usability) โดยระบุว่าโค้ดที่สร้างโดย AI มีความยาวเกินจำเป็น เขียนขึ้นในรูปแบบที่มนุษย์อ่านและทำความเข้าใจได้ยาก และเต็มไปด้วยการเรียกใช้กลยุทธ์พิสูจน์ที่ซ้ำซ้อน (tactical bloat) ส่งผลให้คลัง `mathlib` หลักยังไม่มีแผนที่จะรวมบทตั้ง 29,511 รายการนี้เข้าสู่ระบบหลักในปัจจุบัน

นอกจากนี้ ชุมชนนักวิจัยยังเน้นย้ำข้อเท็จจริงว่านี่เป็นการแปลงบทพิสูจน์ที่มีอยู่แล้ว (autoformalization) ไม่ใช่การค้นพบความรู้ทางคณิตศาสตร์ใหม่แต่อย่างใด ส่วนกระแสข่าวลือในโลกออนไลน์ที่อ้างว่า Anthropic กำลังใช้ระบบเดียวกันนี้เพื่อพิสูจน์โจทย์รางวัลมิลเลนเนียมอย่างสมการ Navier–Stokes นั้น ยังคงเป็นเพียงการคาดเดาที่ไม่มีข้อมูลยืนยันอย่างเป็นทางการ

นัยสำคัญต่อภาคธุรกิจและอุตสาหกรรมเทคโนโลยีในประเทศไทย

สำหรับผู้นำธุรกิจและผู้บริหารฝ่ายเทคโนโลยีในประเทศไทย ผลงานชิ้นนี้คือสัญญาณชัดเจนว่าความสามารถของ AI ได้ก้าวข้ามจากการเดาข้อความน่าจะเป็น (probabilistic generation) ไปสู่การยืนยันตรรกะที่แน่นอน 100% (deterministic formal verification) ซึ่งแก้ไขปัญหาภาพหลอน (hallucination) ได้อย่างเด็ดขาดเมื่อทำงานควบคู่กับระบบตรวจสอบที่มีเคอร์เนลยืนยันความถูกต้อง

องค์กรไทยในอุตสาหกรรมที่ห้ามเกิดข้อผิดพลาด เช่น สถาบันการเงินที่พัฒนาโปรโตคอลระบบการชำระเงินความเร็วสูง อุตสาหกรรมอุปกรณ์การแพทย์ และระบบควบคุมระบบรางหรือโครงข่ายพลังงาน สามารถนำแนวคิด multi-agent verification นี้ไปประยุกต์ใช้ในการตรวจสอบความถูกต้องของซอฟต์แวร์ระดับฐานราก (smart contracts หรือ safety-critical firmware) เพื่อป้องกันช่องโหว่ร้ายแรงก่อนการใช้งานจริง

อย่างไรก็ตาม บทเรียนสำคัญสำหรับทีมวิศวกรรมในไทยคือ 'ต้นทุนและความสามารถในการดูแลรักษา' การพึ่งพาโมเดล AI ในการสร้างโค้ดขนาดนับสิบล้านบรรทัดโดยไม่วางโครงสร้างสถาปัตยกรรมที่มนุษย์เข้าใจได้ จะสร้างหนี้ทางเทคนิค (technical debt) มหาศาล ภาคธุรกิจจึงควรวางตำแหน่งของระบบตัวแทนอัตโนมัตินี้ให้เป็นผู้ช่วยสร้างข้อพิสูจน์ภายใต้กรอบการออกแบบของมนุษย์ ไม่ใช่การปล่อยให้โมเดลสร้างโค้ดสีดำที่ไม่มีใครสามารถบำรุงรักษาได้ในระยะยาว

ทำไมเรื่องนี้สำคัญ

ความสำเร็จนี้พิสูจน์ว่าระบบ AI อัตโนมัติสามารถตรวจสอบและแปลงตรรกะความรู้ระดับสูงที่มีความซับซ้อนมหาศาลได้อย่างถูกต้อง 100% ซึ่งเป็นรากฐานสำคัญสำหรับการพัฒนาซอฟต์แวร์ความปลอดภัยสูงและระบบภารกิจวิกฤตขององค์กรธุรกิจ

ข้อมูลอ้างอิงหลัก