Claude แปลงบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์เป็น Lean

เมื่อ 4 ก.ย. 2569 Anthropic เผยแพร่รายงานว่าใช้ Claude แปลงบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ให้อยู่ในภาษา Lean ซึ่งเป็นภาษาที่เครื่องตรวจความถูกต้องของบทพิสูจน์ได้ทีละขั้น จนได้บทพิสูจน์ที่เครื่องตรวจผ่านครบตั้งแต่ต้นจนจบ (Anthropic)

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

เกิดอะไรขึ้น

Anthropic ระบุว่าใช้เวลา 11 วัน โดย Claude ทำงานเองเป็นส่วนใหญ่ และเดินตามฉบับที่เรียบเรียงให้เข้าใจง่ายขึ้นของ Darmon, Diamond และ Taylor แทนการไล่ตามต้นฉบับโดยตรง (Anthropic) ส่วนคลังโค้ดให้เครดิตสายงานที่บทพิสูจน์นี้ยืนอยู่บนไว้ว่าเป็นของ Frey, Serre, Ribet, Wiles และ Taylor-Wiles (GitHub)

ตัวเลขของงานตามที่บริษัทรายงานคือ

• โค้ด Lean กว่า 13 ล้านบรรทัด ซึ่งบริษัทระบุว่ามากกว่าขนาดของ Mathlib อันเป็นคลังบทพิสูจน์กลางของวงการเกินห้าเท่า (Anthropic)
• ทฤษฎีบทย่อยที่สร้างขึ้นระหว่างทาง 30,300 ข้อ โดยมี 29,500 ข้อที่ถูกใช้ในบทพิสูจน์สุดท้าย (Anthropic)
• โทเคนขาออกที่ใช้ไปราว 6 พันล้านโทเคน (Anthropic)
• ความพยายามรอบแรกที่ล้มเหลวยังเหลือร่องรอยอยู่ราว 7 เปอร์เซ็นต์ของบรรทัดที่ไม่ใช่โค้ดสำเร็จรูป (Anthropic)

โมเดลที่ใช้ไม่ใช่รุ่นที่เปิดขาย บริษัทอธิบายว่าเป็นโมเดลวิจัยภายในสำหรับงานทั่วไปที่ความสามารถใกล้เคียงกับ Claude Fable 5.1 claude-fable-5-1 ซึ่งตัว Fable 5.1 เองเปิดขายไปแล้วตั้งแต่ 1 ก.ย. 2569 (Anthropic)

การทำงานใช้ Claude หลาย agent พร้อมกันบนแพลตฟอร์มชื่อ Prove2Me ซึ่งไม่ใช่ของ Anthropic แต่เป็นงานของ Tianyi Peng และคณะที่ Columbia (arXiv 2608.28433) รายงานระบุว่ารอบแรกๆ ล้มเหลวเพราะ agent หลุดจากสถานะของโครงการและเลิกทำงานร่วมกันอย่างได้ผล และมนุษย์ยังคงให้คำแนะนำระดับภาพรวมเป็นระยะ (Anthropic)

ส่วนที่ตรวจได้จริง แยกจากส่วนที่บริษัทรายงานเอง

นี่คือแกนที่ทำให้ข่าวนี้ต่างจากคำอ้างของผู้ขายทั่วไป เพราะผลลัพธ์หลักถูกตรวจโดยคนนอกไปแล้ว

ตรวจได้และมีคนนอกตรวจแล้ว คือตัวบทพิสูจน์เอง คลังโค้ดตั้งด่านไว้ในไฟล์ที่เป็นเป้าหมายการประกอบเริ่มต้น ให้การประกอบล้มทันทีถ้าบทพิสูจน์สุดท้ายไปพิงข้อตั้งต้นนอกเหนือจากสามข้อมาตรฐานของ Lean และคลังยังระบุว่าไม่มีการทิ้งช่องว่างไว้ให้เติมภายหลัง (GitHub) ที่สำคัญกว่านั้นคือ Kevin Buzzard ซึ่งเป็นนักคณิตศาสตร์ที่ทำโครงการแปลงบทพิสูจน์เดียวกันนี้อยู่ เขียนในบล็อกของตัวเองว่าเขาดึงโค้ดมาคอมไพล์เองและรันเครื่องตรวจอิสระแล้วผ่าน (Xena Project)

ตรวจจากภายนอกไม่ได้เลย คือตัวเลขกระบวนการทั้งหมด ได้แก่ระยะเวลา 11 วัน จำนวนโทเคน 6 พันล้าน จำนวนทฤษฎีบท 30,300 ข้อ สัดส่วน 7 เปอร์เซ็นต์จากความพยายามที่ล้มเหลว และสเปกของโมเดลที่ใช้ ทั้งหมดนี้มี Anthropic เป็นแหล่งเดียว การอ้างตัวเลขกลุ่มนี้ต่อจึงต้องระบุเสมอว่าเป็นตัวเลขที่บริษัทรายงานเอง

เรื่องที่คนเข้าใจผิดบ่อย

เข้าใจผิดว่า AI คิดคณิตศาสตร์ใหม่ได้แล้ว ความจริงคือ Anthropic เขียนกำกับไว้เองว่าต่างจากงานที่ผลิตคณิตศาสตร์ใหม่ สิ่งที่ใหม่ในงานนี้คือการตรวจสอบ ซึ่งบริษัทเปรียบว่าเหมือนการตรวจการคำนวณด้วยเครื่องคิดเลข (Anthropic) ฝั่ง Buzzard พูดตรงกว่านั้นว่าในแง่คณิตศาสตร์ งานชิ้นนี้แทบไม่ได้บอกอะไรใหม่กับวงการ เพราะเดินตามวรรณกรรมยุคแรกของบทพิสูจน์อย่างซื่อสัตย์โดยไม่ได้เพิ่มอะไรเข้าไป (Xena Project)

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

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

สิ่งที่ยังไม่มีหลักฐาน

ข้อจำกัดที่ซื่อสัตย์ที่สุดของงานลักษณะนี้คือทุกอย่างวางอยู่บนสมมติฐานว่าตัวเครื่องตรวจของ Lean เองไม่มีช่องโหว่ ซึ่งคลังโค้ดของโครงการรับข้อจำกัดนี้ไว้เองแล้ว การตรวจซ้ำด้วยเครื่องตรวจอิสระที่เขียนคนละภาษาช่วยลดความเสี่ยงนี้ลงแต่ไม่ได้ทำให้หมดไป (GitHub)

อีกข้อที่ยังไม่มีใครแสดงคือวิธีการชุดนี้จะย้ายไปใช้กับบทพิสูจน์อื่นที่ยังไม่มีใครเรียบเรียงไว้ให้ง่ายแล้วได้ผลเหมือนกันหรือไม่ งานนี้มีข้อได้เปรียบที่หายากคือมีวรรณกรรมที่เรียบเรียงมาอย่างดีให้เดินตาม

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

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

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

ส่วนงานที่ไม่มีเครื่องตรวจแบบนี้ เช่น การเขียนข้อความหาลูกค้าหรือการตัดสินใจเชิงกลยุทธ์ ยังต้องใช้คนตรวจเหมือนเดิม และเป็นจุดที่ผลการวิจัยเรื่องข้อจำกัดของการให้ AI ตรวจงาน AI ai-judge-blind-spots-2026 ยังใช้ได้อยู่ทั้งหมด คำถามที่ใช้คัดงานได้เร็วที่สุดจึงเป็นคำถามเดียวว่างานนี้มีอะไรบอกได้เองไหมว่าผลลัพธ์ผิด

คำถามที่ยังไม่มีคำตอบ

• มีใครนอกเหนือจาก Buzzard คอมไพล์และตรวจซ้ำอย่างเป็นอิสระอีกหรือไม่
• วิธีการชุดนี้จะได้ผลกับบทพิสูจน์ที่ยังไม่มีการเรียบเรียงให้ง่ายไว้ก่อนหรือไม่
• ต้นทุนจริงของงานลักษณะนี้เป็นเท่าไรเมื่อคิดเป็นเงิน เพราะบริษัทให้มาเฉพาะจำนวนโทเคน