หมุดหมายประวัติศาสตร์: การตรวจสอบทฤษฎีบทแฟร์มาด้วยคอมพิวเตอร์
เมื่อวันที่ 4-5 กันยายน 2026 บริษัท Anthropic ได้ประกาศความสำเร็จครั้งประวัติศาสตร์ในวงการวิทยาการคอมพิวเตอร์และคณิตศาสตร์ โดยระบบตัวแทนอัตโนมัติ (AI agents) ที่ขับเคลื่อนด้วยโมเดล Claude สามารถสร้างการพิสูจน์เชิงรูปนัย (Formalization) สำหรับทฤษฎีบทสุดท้ายของแฟร์มา (Fermat's Last Theorem หรือ FLT) ในภาษา Lean 4 ได้สำเร็จสมบูรณ์และผ่านการตรวจสอบโดยระบบคอมพิวเตอร์ทั้งระบบ
การพิสูจน์ครั้งนี้เป็นการแปลงข้อพิสูจน์อันลือลั่นในปี 1995 ของ เซอร์ แอนดรูว์ ไวลส์ (Sir Andrew Wiles) โดยเฉพาะการอิงตามแนวทางการนำเสนอของ ดาร์มอน-ไดมอนด์-เทย์เลอร์ (Darmon–Diamond–Taylor exposition) ซึ่งใช้ทฤษฎีบทแลงแลนด์ส-ทันเนลล์ (Langlands–Tunnell theorem) และทฤษฎีบทการลดระดับของริเบต์ (Ribet's level-lowering theorem) ให้อยู่ในรูปของตรรกศาสตร์เชิงสัญลักษณ์ที่เครื่องจักรสามารถตรวจสอบความถูกต้องได้ทุกขั้นตอน
ความสำเร็จดังกล่าวส่งผลให้ทฤษฎีบทสุดท้ายของแฟร์มา ซึ่งเป็นโจทย์ข้อสุดท้ายที่ยังคั่งค้างอยู่ในรายชื่อ "100 Famous Theorems" ของ ฟรีค วีไดค์ (Freek Wiedijk) ได้รับการคอมไพล์และพิสูจน์อย่างเป็นทางการครบทั้งหมด ปิดฉากความท้าทายที่มีมานานหลายทศวรรษของการนำทฤษฎีบทคณิตศาสตร์ระดับตำนานเข้าสู่ระบบตรวจสอบด้วยคอมพิวเตอร์
เจาะลึกสถิติและสถาปัตยกรรม: 13.4 ล้านบรรทัดของโค้ด Lean 4
ในแง่ของขนาดและสเกลทางวิศวกรรม โค้ดการพิสูจน์ชุดนี้มีขนาดรวมประมาณ 13.4 ล้านบรรทัดของภาษา Lean 4 โดยหากตัดส่วนโค้ดสำเร็จรูป (boilerplate) ที่ระบบสร้างขึ้น จะมีเนื้อหาการพิสูจน์แท้จริงราว 10.5 ล้านบรรทัด ตัวระบบสามารถพิสูจน์ทฤษฎีบทย่อยได้ทั้งหมด 30,300 ทฤษฎีบท ซึ่งในจำนวนนี้มี 29,511 ทฤษฎีบทที่ถูกรวมเข้าสู่กราฟการพึ่งพาหลัก (main dependency graph) อย่างสมบูรณ์
กระบวนการทั้งหมดดำเนินการต่อเนื่องเป็นเวลาประมาณ 11 วัน โดยเริ่มตั้งแต่วันที่ 7 สิงหาคม 2026 ภายใต้การทำงานคู่ขนานของตัวแทน Claude หลายสิบตัว และบริโภคโทเค็นขาออก (output tokens) ไปรวมทั้งสิ้นประมาณ 6 พันล้านโทเค็น โครงการนี้ผสานการทำงานร่วมกับ Prove2Me ซึ่งเป็นเฟรมเวิร์กประสานงานตัวแทนอัจฉริยะแบบ Directed Acyclic Graph (DAG) ที่พัฒนาโดยห้องปฏิบัติการของ Tianyi Peng แห่งมหาวิทยาลัยโคลัมเบีย
ประเด็นสำคัญด้านความน่าเชื่อถือคือ ตัวโค้ดทั้งหมดผ่านการตรวจสอบความถูกต้องโดยไม่มีการใช้ตัวเว้นวรรคสมมติฐานชั่วคราว หรือคำสั่ง `sorry` แม้แต่จุดเดียว และพึ่งพาเพียงสัจพจน์มาตรฐาน (standard axioms) ทั้ง 3 ข้อของภาษา Lean เท่านั้น นอกจากนี้ยังได้รับการตรวจสอบยืนยันความถูกต้องซ้ำผ่านระบบตรวจสอบอิสระภายนอก เช่น `comparator` และ `nanoda`
ข้อจำกัดและการให้เครดิต: สร้างบนรากฐานมนุษย์ ไม่ใช่การแก้โจทย์ใหม่
แม้จะเป็นความก้าวหน้าทางวิศวกรรมที่น่าทึ่ง แต่จำเป็นต้องระบุให้ชัดเจนว่า Claude ไม่ได้ "ค้นพบ" วิธีแก้ปัญหาคณิตศาสตร์ใหม่ที่ยังไม่มีใครแก้ได้ ทฤษฎีบทสุดท้ายของแฟร์มาได้รับการพิสูจน์โดยมนุษย์เรียบร้อยแล้วตั้งแต่ปี 1995 สิ่งที่โมเดลทำคือการแปลงบทพิสูจน์ทางคณิตศาสตร์ภาษาธรรมชาติที่มีอยู่เดิมให้กลายเป็นโค้ดเชิงรูปนัยที่ตรวจสอบได้โดยคอมพิวเตอร์ (Formalization)
นอกจากนี้ โครงการดังกล่าวยังพึ่งพาคลังข้อมูล Mathlib และดัดแปลงไฟล์ตั้งต้นจำนวน 106 ไฟล์โดยตรงจากโครงการ Imperial College London FLT ของ ศ. เควิน บัซซาร์ด (Kevin Buzzard) รวมถึงคลังข้อมูล `flt-regular` ซึ่ง ศ. บัซซาร์ด ได้ร่วมทำการคอมไพล์และตรวจสอบโค้ดชุดนี้ด้วยตนเอง
ในแง่คุณภาพของโค้ด ผู้ดูแลคลังไลบรารี Mathlib ตั้งข้อสังเกตว่า โค้ดความยาว 13.4 ล้านบรรทัดนี้เกิดขึ้นจากการสร้างของเครื่องจักร (machine-generated autoformalization) จึงยังมีโครงสร้างที่เทอะทะและไม่ประณีตพอที่จะรวมเข้าเป็นส่วนหนึ่งของ Mathlib มาตรฐานที่มนุษย์ดูแลได้ทันที นอกจากนี้ยังต้องแยกแยะความสำเร็จนี้ออกจากข่าวลือที่แพร่สะพัดว่า Anthropic แก้ปัญหา Navier–Stokes ซึ่งเป็นหนึ่งใน Millennium Prize Problems ได้ ซึ่งข่าวดังกล่าวเป็นเพียงข่าวลือที่ไม่มีหลักฐานยืนยัน
เสียงสะท้อนจากชุมชนนักพัฒนาและนักวิจัย
ในกลุ่มนักวิจัยด้านการพิสูจน์ทฤษฎีบทเชิงรูปนัย (Formal Verification) และนักคณิตศาสตร์ ผู้เชี่ยวชาญต่างยกย่องว่านี่คือหมุดหมายสำคัญที่พิสูจน์ว่าโมเดลภาษาขนาดใหญ่ (LLM) สามารถรักษาความสอดคล้องเชิงตรรกะระยะยาวโดยไม่เกิดอาการหลอน (hallucination) เมื่อมีระบบตรวจสอบไวยากรณ์และกฎเกณฑ์คอยกำกับอย่างรัดกุม
อย่างไรก็ตาม ในหมู่นักพัฒนาและนักวิชาการมีข้อถกเถียงเกี่ยวกับการสื่อสารด้านการตลาด โดยหลายฝ่ายออกมาเตือนไม่ให้มองข้ามความพยายามของชุมชนโอเพนซอร์สและนักคณิตศาสตร์ที่เป็นมนุษย์ ซึ่งได้วางโครงสร้างพื้นฐานมานานหลายปี พร้อมชี้ว่าการยกย่องให้เป็นความสำเร็จของ AI เพียงฝ่ายเดียวถือเป็นการบิดเบือนข้อเท็จจริง
ผู้ปฏิบัติงานยังชี้ให้เห็นถึงความท้าทายในโลกความเป็นจริงว่า แม้ระบบจะสามารถสร้างบทพิสูจน์ที่คอมไพล์ผ่านได้ แต่ภาระในการตรวจสอบ (maintenance burden) และการทำความเข้าใจโค้ดขนาดยักษ์ 13.4 ล้านบรรทัดยังคงเป็นโจทย์ยากสำหรับมนุษย์ ซึ่งสะท้อนถึงช่องว่างระหว่าง "โค้ดที่ถูกต้องตามหลักตรรกะ" กับ "โค้ดที่มนุษย์สามารถนำไปใช้งานและบำรุงรักษาต่อได้"
นัยสำคัญต่อภาคธุรกิจและอุตสาหกรรมเทคโนโลยีในไทย
สำหรับผู้นำเทคโนโลยีและองค์กรธุรกิจในประเทศไทย ความก้าวหน้านี้ส่งสัญญาณชัดเจนว่า เทคโนโลยี AI กำลังก้าวข้ามจากการเป็นเพียงเครื่องมือสร้างข้อความหรือตัวช่วยเขียนโค้ดเบื้องต้น ไปสู่การเป็น "ระบบตรวจสอบตรรกะขั้นสูง" (Automated Formal Verification) ที่รับประกันความถูกต้องแม่นยำได้ 100% ตามข้อกำหนด
ภาคส่วนที่จะได้รับประโยชน์สูงสุดในไทยคือ สถาบันการเงินและฟินเทค (FinTech) ที่ต้องการตรวจสอบสัญญาอัจฉริยะ (Smart Contracts) และระบบแกนกลางของธนาคาร (Core Banking) รวมถึงอุตสาหกรรมที่มีความเสี่ยงสูง เช่น การแพทย์ ระบบควบคุมการบิน และระบบโครงสร้างพื้นฐานสำคัญของประเทศ (Critical Infrastructure) ซึ่งเดิมทีการทำ Formal Verification มีต้นทุนค่าใช้จ่ายของบุคลากรผู้เชี่ยวชาญสูงมากจนไม่สามารถทำได้ในวงกว้าง
องค์กรไทยควรเริ่มพิจารณาการนำสถาปัตยกรรมประเภท Agent Coordinator ที่ทำงานร่วมกับ Verifier ในลักษณะเดียวกับ Prove2Me มาปรับใช้ในกระบวนการ CI/CD เพื่อให้ AI ช่วยตรวจสอบช่องโหว่ความปลอดภัยระดับลึกในซอฟต์แวร์ก่อนการปล่อยใช้งานจริง ซึ่งจะช่วยลดความเสี่ยงจากการถูกโจมตีทางไซเบอร์และยกระดับมาตรฐานวิศวกรรมซอฟต์แวร์ของไทยสู่ระดับสากล
ความสำเร็จนี้พิสูจน์ว่า AI สามารถทำการตรวจสอบตรรกะระดับลึก (Formal Verification) ในสเกลหลายล้านบรรทัดได้จริง ซึ่งสามารถนำมาประยุกต์ใช้ในการตรวจสอบซอฟต์แวร์ระดับภารกิจวิกฤต ความปลอดภัยทางไซเบอร์ และสัญญาอัจฉริยะในภาคการเงินของไทย