Fermat's Last Theorem โจทย์คณิตศาสตร์ที่ค้างมา 358 ปี ตอนนี้มี…
เล่าย้อนนิดนึง ปี 1637 Fermat เขียนไว้ที่ขอบหนังสือว่าไม่มีจำนวนเต็มบวก a b c ที่ทำให้ a^n + b^n = c^n เมื่อ n มากกว่า 2 แล้วทิ้งท้ายว่าเขามี "proof ที่วิเศษมาก แต่ขอบกระดาษแคบเกินจะเขียน" คนทั้งโลกหากันมา 350 กว่าปี จนปี 1995 Sir Andrew Wiles ถึงพิสูจน์ได้ ยาว 129 หน้า และใช้เวลาหลายเดือนกว่าคนจะตรวจว่าถูก
แต่ proof ที่มนุษย์อ่านกันมันข้ามขั้นที่ "เห็นชัดอยู่แล้ว" ไปเยอะ ถ้าอยากให้คอมตรวจได้ 100% ต้องแปลงเป็นภาษาอย่าง Lean ที่ต้องเขียนทุกขั้นไม่ให้ขาดแม้แต่ขั้นเดียว วงการเลยมีโปรเจคที่ Kevin Buzzard จาก Imperial College เริ่มตั้งแต่ปี 2024 และคาดว่าจะใช้เวลาหลายปี แค่ blueprint ช่วงแรกก็ 86 หน้าแล้ว
Anthropic เพิ่งประกาศเมื่อ 4 ก.ย. ว่า Claude ทำเสร็จใน 11 วัน เขียน Lean ไป 13 ล้านบรรทัด พิสูจน์ทฤษฎีบทย่อยระหว่างทาง 30,300 ข้อ ใช้จริงใน proof สุดท้าย 29,500 ข้อ ขนาดใหญ่กว่า Mathlib ซึ่งเป็นคลัง proof หลักของวงการถึง 5 เท่า และ Lean ยืนยันแล้วว่าใช้แค่ axiom มาตรฐาน 3 ข้อ ไม่มีสมมติฐานอื่นแอบแฝง
วิธีทำคือใช้ Claude หลายสิบ agent ทำงานพร้อมกันบน harness ที่สร้างจาก Claude Code ช่วงแรกล้มเหลวเพราะ agent หลุดสถานะโปรเจคแล้วเลิกทำงานร่วมกัน (งานที่ล้มเหลวเหลืออยู่ในผลสุดท้ายแค่ราว 7%) ที่สำเร็จเพราะย้ายไปใช้ Prove2Me แพลตฟอร์มจาก Columbia ที่เก็บทฤษฎีบททั้งหมดเป็น DAG ให้ agent เห็นว่าอันไหนพิสูจน์แล้ว อันไหนควรทำต่อ แก้ปัญหาเรื่องความจำเสื่อมของ agent ได้ตรงจุด
มนุษย์แทบไม่ได้ป้อนคณิตศาสตร์เลย มีแค่คำสั่งระดับสูงเป็นครั้งคราวจาก Tianyi Peng นักวิจัยที่ดูแลโปรเจค เช่น "Jacobian as a scheme sounds high priority" แล้วตอนที่ proof สำเร็จ Claude เขียนในความคิดตัวเองว่า "The FLT root reads PROVED. Historic moment (modulo re-check)."
ค่าใช้จ่ายไม่น้อย ใช้ output token ราว 6 พันล้าน token จากโมเดลวิจัยภายในที่เทียบเท่า Claude Fable 5.1 แต่ที่น่าสนใจคือทีมลองอีกงานเล็ก ๆ ใช้แค่ Claude Max 3 บัญชี formalize ทฤษฎีบท Three Primes ของ Vinogradov เสร็จใน 3 วัน แปลว่าถ้ามี scaffold ดี ๆ นักคณิตศาสตร์ทั่วไปก็ทำแบบนี้ได้ด้วย subscription ธรรมดา
Kevin Buzzard ที่รีวิว proof แล้วบอกว่า ถ้า formalize FLT อัตโนมัติได้แล้ว เท่ากับเราก้าวใหญ่ไปสู่การ formalize วรรณกรรมคณิตศาสตร์สมัยใหม่ทั้งหมด จะได้เครื่องมือไล่หาข้อผิดพลาดในองค์ความรู้ที่มีอยู่ และเบาภาระคนตรวจงาน
ผมก็เห็นว่าจุดที่ควรจับตาไม่ใช่แค่ว่า AI พิสูจน์โจทย์ดังได้ แต่คือเรื่อง "การตรวจสอบ" เพราะต่อจากนี้ AI จะผลิต proof ออกมาเร็วกว่าที่มนุษย์จะตรวจทัน ทางเดียวที่วงการจะเชื่อผลพวกนั้นได้คือให้คอมตรวจให้ และงานนี้พิสูจน์ว่ามันทำได้แล้วในระดับโจทย์ที่ยากที่สุดโจทย์หนึ่ง
Proof ฉบับเต็มเปิดบน GitHub อ่านรายละเอียดได้ที่ https://www.anthropic.com/research/formalizing-fermats-last-theorem
อยากใช้ AI กับงานจริงเป็นระบบ?
เรียน Claude Method — วิธีคิดและลงมือใช้ Claude/AI กับงานจริง ตั้งแต่วันแรก
📍 โพสต้นฉบับบน Facebook: AI กับ Peesamac