Claude พิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ใน 11 วัน, งานที่มนุษย์ตั้งเป้าไว้ 5 ปี

โดย Nokka (นก-กา) | กันยายน 2026

บทความนี้เขียนโดย AI (GLM-5.3) ผ่าน Hermes Agent — ตรวจสอบและเรียบเรียงโดย Nokka

วันที่ 4 กันยายน 2026 Kevin Buzzard นักคณิตศาสตร์ประจำ Imperial College London เขียนบทความลงบล็อกส่วนตัวของเขาโดยใช้ชื่อหัวข้อสั้น ๆ ว่า "Anthropic has beaten me to it" แปลตรงตัวได้ว่า Anthropic มาก่อนผมไปแล้ว [3]

คนที่พูดประโยคนี้ไม่ใช่นักคณิตศาสตร์ธรรมดา เขาคือคนที่ได้ทุนวิจัยห้าปี (2024-2029) เพื่อทำโปรเจกต์ที่คณิตศาสตร์ทั่วโลกเชียร์ให้สำเร็จ นั่นคือการ formalize ทฤษฎีบทสุดท้ายของแฟร์มาต์ (Fermat's Last Theorem) ด้วยภาษา Lean แล้วทีมวิจัยของ Anthropic เอาโมเดล Claude มาทำงานนั้นจบในเวลา 11 วัน [1][2]

ปัญหาที่รออยู่ 358 ปี

ทฤษฎีบทสุดท้ายของแฟร์มาต์เป็นข้อความที่ดูง่ายเหลือเชื่อ สมการ xⁿ + yⁿ = zⁿ ไม่มีคำตอบเป็นจำนวนเต็มบวกเมื่อ n มากกว่า 2 เขียนจบในหนึ่งบรรทัดเด็กมัธยมอ่านรู้เรื่อง แต่ทายไว้ตั้งแต่ปี 1637 โดย Pierre de Fermat ที่อวดในขอบหนังสือว่ามีบทพิสูจน์อย่างวิเศษแต่ที่ว่างไม่พอจะเขียน มนุษย์เพิ่งพิสูจน์ได้จริงเมื่อปี 1995 โดย Andrew Wiles ในงานที่ยาว 129 หน้า กวาดรางวัล Abel มาครอง [1]

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

11 วันของ Claude

ระหว่างวันที่ 7 ถึง 17 สิงหาคม Claude ทำงานแบบอิสระเป็นหลักผ่านแพลตฟอร์ม Prove2Me ที่รวม agent หลายสิบตัวให้แบ่งงานกันบนแผนผังทฤษฎีบท ผลลัพธ์ที่ได้คือบทพิสูจน์ที่ตรวจสอบด้วยเครื่องครบทั้งเส้นทางเป็นครั้งแรกของโลก ตัวเลขที่ตามมาคือโค้ด Lean 13 ล้านบรรทัด ทฤษฎีบทย่อยที่พิสูจน์แล้ว 30,300 ตัว (ใช้จริงในบทพิสูจน์สุดท้าย 29,500 ตัว) ใหญ่กว่าคลังคณิตศาสตร์ชุมชน Mathlib ที่มันอาศัยอยู่ถึงห้าเท่า กิน output token ประมาณหกพันล้าน จากโมเดลวิจัยภายในที่กำลังอยู่ระดับใกล้ Claude Fable 5.1 [1][2]

สิ่งที่มนุษย์ทำมีขนาดเล็กมากจนน่าขำ นักวิจัยของ Anthropic ชื่อ Tianyi แทรกคำแนะนำระดับสูงเป็นครั้งคราวเท่านั้น เช่นประโยคว่า Jacobian แบบ scheme น่าจะสำคัญมาก หรือเร่งงาน Mazur theorem ให้เสร็จเร็วหน่อย [1] ที่เหลือคือกลไกล้งานของ agent ที่ตรวจสอบกันเอง มีบันทึกที่น่าทึ่งจริง ๆ คือวันสุดท้ายมี agent ตัวหนึ่งพบว่า lemma ที่ตัวเองผ่านการตรวจไปแล้วมีข้อผิดพลาดจริง เพราะยกเลิกการคูณด้านที่ต้องใช้ monomorphism แต่ใช้ epimorphism แล้วพิมพ์ข้อความลง log ว่าตัวเองพลาดเอง ต้องรีบโพสต์แจ้งแก้ไขทันที [2]

จบงานเมื่อสี่ทุ่มหนึ่งนาทีของคืนวันที่ 17 สิงหาคม agent หลายตัวเห็นสถานะทฤษฎีบทหลักเปลี่ยนเป็น Proved พร้อมกัน หนึ่งตัวเขียนว่านี่คือช่วงเวลาประวัติศาสตร์ของการทัพนี้ แล้วตัวถัดไปเขียนเติมใน log ว่าก่อนจะเชื่อต้องไปเช็คเองด้วย query อิสระอีกครั้ง [2]

ความชาญฉลาดของการออกแบบอยู่ที่การ์ดแจกงาน ทีมงานแรกเคยล้มเหลวเพราะ agent ทำงานแบบกระจัดกระจายจนคลาดสถานะโครงการ สิ่งที่ช่วยทีมรอบสองคือการบังคับให้ทุกตัวทำงานบนแผนผังอ้างอิงทฤษฎีบทแบบ DAG ที่แชร์กัน งานที่เคยล้มเหลวก็ไม่ไร้ค่านัก มันกลายเป็นวัตถุดิบราวเจ็ดเปอร์เซ็นต์ของบรรทัดที่ไม่ใช่ boilerplate ในบทพิสูจน์ฉบับสุดท้าย [4]

แล้วคนที่แพ้ พูว่าอะไร

Buzzard คือตัวละครที่ทำให้เรื่องนี้มีมนุษย์ธรรม เขาไม่ได้โกรธหรือเสียขวัญ แต่เขียนรีวิวด้วยความละเอียดถี่ถ้วนของคนในวงการจริง เขา compile โค้ดทั้งหมดด้วยมือตัวเอง รันเครื่องมือ comparator เทียบข้อความทฤษฎีบทกับ Mathlib แล้วยืนยันว่าผ่านหมดจริง [3]

แต่เขาก็ไม่ลืมชี้ความต่างที่สำคัญ ทางเดินของ Anthropic คือเส้นทางบทพิสูจน์ยุค 1990s (สาย Darmon-Diamond-Taylor ผ่าน Langlands-Tunnell และ Ribet) ไม่ใช่เส้นทางสมัยใหม่ที่เขากำลังทำเองอยู่ และงานนี้พิสูจน์แบบ restricted คือใช้ได้กับ prime p ≥ 17 เท่านั้น ไม่ใช่ทฤษฎีบทฉบับทั่วไปที่ Mathlib ต้องการ ที่เหลือพิสูจน์ตามได้เพราะมีคน formalize ส่วน prime เล็กไว้ก่อนหน้าแล้ว ที่สำคัญเขาสรุปตรง ๆ ว่างานนี้ไม่ได้เพิ่มอะไรทางคณิตศาสตร์ [3]

ทว่าประโยคปิดท้ายของเขาคือสิ่งที่คนทั้งวงการจ้องมอง เขาเขียนว่าถ้ามีงานวรรณกรรมหลายพันหน้าถูก formalize ได้ครบทั้งเส้นทางด้วยฝูง AI ภายใน 11 วันแบบนี้แล้ว อนาคตเราจะเห็นการ formalize งานวิจัยสด ๆ เกิดขึ้นแบบทำทันทีทันใจ [3]

ข้อจำกัดที่ Anthropic ยอมรับเอง

เพื่อไม่ให้เรื่องนี้กลายเป็นข่าวโฆษณาชาติ ฝ่ายวิจัยของ Anthropic เขียนส่วน cons ของงานเอาไว้อย่างซื่อสัตย์ และหลายข้อน่าสนใจยิ่งกว่าตัวความสำเร็จ [2]

อันดับแรกโค้ดนี้อ่านเป็นคณิตศาสตร์ไม่ได้ มันเขียนโดยไม่มีคอมเมนต์อธิบาย ชื่อ helper เป็นชื่อเครื่อง ไม่เป็นไปตามมาตรฐาน Mathlib ที่ต้องมี doc string ทุก definition ไฟล์กว่า 900 ไฟล์ยาวเกินเพดาน 1,500 บรรทัด (ทั้งที่ Mathlib เองมีแค่ 2 ไฟล์) อันดับสองมันไม่เป็นทฤษฎีบททั่วไป เวอร์ชัน Ribet กับ Wiles ในงานนี้ถูกพิสูจน์แบบ restricted ที่เอามาใช้กับโจทย์นี้โดยเฉพาะ อันดับสามมันเปราะบางราวหนึ่งในห้าของบรรทัดทั้งหมดเป็นสำเนาที่ copy กันมาเอง มี lemma ตัวเดียวถูกประกาศซ้ำในกว่า 300 ไฟล์ และการ build ครั้งเดียวกิน 96 cores กับ RAM 512 GiB นานเกือบหกชั่วโมง

คำถามที่ทีมตอบไว้ล่วงหน้าคือโค้ดชุดนี้จะเข้า Mathlib ไหม คำตอบคือไม่ ในรูปนี้ แต่ชิ้นส่วนโครงสร้างพื้นฐานที่ต้องสร้างขึ้นมาใหม่เพราะ Mathlib ยังไม่มี อย่าง Hecke algebras กับ deformation rings น่าจะถูกหยิบไปพัฒนาต่อโดยมนุษย์นำเป็นหลักได้ [2]

มองไปข้างหน้า

สิ่งที่ผมคิดว่าคนทำ AI ควรเก็บกลับไปจากงานนี้ไม่ใช่ว่า AI เก่งกว่านักคณิตศาสตร์ (ไม่ใช่ และ Buzzard ย้ำเรื่องนี้ชัดเจน) แต่เป็นสองเรื่อง หนึ่ง pattern การทำงานของ agent ที่แบ่งงานบนแผนผัง DAG ตรวจกันเอง ยอมรับความผิดพลาดแล้วแก้ทันที และสองประตูที่เปิดออกไปว่าเมื่อการตรวจสอบความถูกต้องกลายเป็นของถูก งานวิจัยสดจะถูกตรวจได้แบบทันทีทันใจในอนาคตอันใกล้ วันนั้นบทพิสูจน์ของ Wiles ที่ใช้เวลาหกปีจะถูกอ่านอย่างละเอียดโดยเครื่องไม่ใช่เจ็ดปี และนักคณิตศาสตร์จะได้เวลากลับไปคิดโจทย์ใหม่

แหล่งอ้างอิง

[1] Anthropic, "Formalizing Fermat's Last Theorem" (4 ก.ย. 2026), https://www.anthropic.com/research/formalizing-fermats-last-theorem

[2] Anthropic, "Formalizing Fermat's Last Theorem in Lean: A timeline and selected excerpts from Claude's reasoning" (2026), https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf

[3] Buzzard, K., "FLT: Anthropic has beaten me to it", Xena Project (4 ก.ย. 2026), https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

[4] jamilxt, "AI Agents Failed to Prove Fermat's Last Theorem. Then They Got a Shared To-Do List", dev.to (2026), https://dev.to/jamilxt/ai-agents-failed-to-prove-fermats-last-theorem-then-they-got-a-shared-to-do-list-h0k