Claude พิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์จบครบวงจรใน Lean 4 — 13 ล้านบรรทัดใน 11 วัน แต่ทฤษฎีบทคลาสสิกข้างในถูกพิสูจน์แค่ 'เท่าที่จำเป็น'

4 กันยายน 2026 Anthropic เผยแพร่สิ่งที่เรียกว่า พิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ (Fermat’s Last Theorem, FLT) ที่เครื่องตรวจสอบได้ครบวงจรเป็นครั้งแรก เขียนด้วยภาษา Lean 4 โดย Claude ทำงานเองเป็นส่วนใหญ่ตลอด 11 วัน ผลลัพธ์คือ โค้ด Lean 13 ล้านบรรทัด ที่ใหญ่กว่า Mathlib ซึ่งเป็นคลังพิสูจน์กลางของชุมชนกว่า 5 เท่า พร้อมทฤษฎีบทย่อยที่พิสูจน์แล้ว 30,300 ข้อ (ใช้จริงในเส้นทางสุดท้าย 29,500 ข้อ)

ตัวเลขพวกนี้อยู่ในข่าวทุกสำนักแล้ว สิ่งที่ไม่ค่อยมีใครเปิดคือ รีโปจริง ซึ่ง Anthropic ปล่อยใต้ Apache-2.0 ที่ github.com/anthropics/fermats-last-theorem (สร้างเมื่อ 4 ก.ย. เวลา 14:21 UTC) — และไฟล์ในนั้นเล่าเรื่องที่ละเอียดกว่าประกาศมาก ทั้งวิธีตรวจสอบ ต้นทุนการตรวจซ้ำ และขอบเขตที่แคบกว่าที่พาดหัวชวนให้เข้าใจ

อีกจุดที่หายไปจากข่าวคือ งานนี้จบไปตั้งแต่กลางเดือนสิงหาคม ไม่ใช่สัปดาห์นี้ — บันทึกความคิดของ Claude ที่ Anthropic ยกมาเองเขียนว่า “The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18” คือรากของต้นไม้พิสูจน์ปิดเมื่อ 18 ส.ค. เวลา 02:00:57 UTC แล้วประกาศ 17 วันให้หลัง

สิ่งที่ตรวจแล้วจริง: สามชั้น ไม่ใช่ชั้นเดียว

รีโปไม่ได้บอกแค่ว่า “Lean ตรวจผ่าน” แต่ระบุการตรวจสามชั้นพร้อมผลลัพธ์ที่อ้างอิงได้:

ชั้น	เครื่องมือ	ผลที่รายงาน
1. บิลด์จากศูนย์	lake build บน Lean 4.33.1 + Mathlib v4.33.0 (ตรึงด้วย commit)	60,475 โมดูล ผ่านเคอร์เนล Lean ทั้งหมด
2. ตัวเทียบอิสระ	leanprover/comparator v4.33.0 เทียบกับโจทย์ที่เขียนด้วย Mathlib ล้วน	คำตัดสิน: Your solution is okay!
3. เคอร์เนลที่สอง	nanoda 0.4.13 เคอร์เนล Lean อิสระที่เขียนด้วย Rust	Checked 1052234 declarations with no errors

เป้าบิลด์ดีฟอลต์ FinalCheck.lean ไม่ได้แค่คอมไพล์ผ่าน แต่ใช้ #guard_msgs บังคับให้ผลของ #print axioms fermat_last_theorem ตรงเป๊ะกับ สัจพจน์มาตรฐานสามข้อของ Lean (propext, Classical.choice, Quot.sound) — แปลว่า บิลด์จะพังทันทีถ้ามีใครแอบใส่ sorry หรือ axiom เพิ่ม และ README ยืนยันว่าไม่มีโมดูลไหนใช้ sorry, native_decide, unsafe, extern, implemented_by, partial def หรือ #eval เลย ไฟล์ formalization.yaml ระบุ sorry_count: 0 ตรงกัน

ข้อควรระวังที่ Anthropic เขียนเปิดเผยเอง: nanoda ที่ใช้ถูกแพตช์ 4 จุดโดยทีมเอง (หนึ่งจุดเพิ่มการแสดงความคืบหน้า อีกสามจุดเร่งการค้น definitional equality เพราะถ้าไม่แก้ บางประกาศกิน nanoda ตัวเดิมหลายชั่วโมงต่อข้อ) โดยยืนยันว่า “None of the patches adds, removes or weakens a typing rule” — เป็นการเปิดเผยที่ตรงไปตรงมา แต่คนที่จะอ้างว่า “ตรวจด้วยเคอร์เนลอิสระแล้ว” ควรอ่านบรรทัดนี้ด้วย

จุดที่ควรโยงกลับ: บิลด์นี้อยู่บน Lean 4.33.1 ซึ่งรวมการแก้ soundness ของเคอร์เนลปี 2026 ไว้แล้ว — เรื่องที่เราเขียนไว้เมื่อ 2 ส.ค. ว่าบั๊กในเคอร์เนลตัวตรวจคือความเสี่ยงที่ฐานของทุกอย่าง ห่วงโซ่ความเชื่อถือทั้งหมดของงานนี้ยังจบลงที่ “เชื่อเคอร์เนล Lean” อยู่ดี

ตรวจซ้ำเองได้จริง — ถ้ามีเครื่อง RAM 300 GB

หัวข้อ “Check it yourself” ของ README เป็นส่วนที่มีค่าที่สุดสำหรับนักพัฒนา เพราะระบุต้นทุนจริงไว้หมด:

• บิลด์: ใช้เวลา 5 ชม. 32 นาที ที่ 96 jobs, RAM สูงสุด 153 GB (ราว 5 GB ต่อ job แต่บางโมดูลกินถึง 36 GB), ดิสก์ราว 67 GB ใต้ .lake/ บวกไฟล์ C อีกราว 220 GB
• comparator: ราว 14 ชม. 46 นาที โดยเกือบทั้งหมดคือการเล่นซ้ำผ่านเคอร์เนลบนคอร์เดียว RAM สูงสุด 230 GB (แนะนำให้เผื่อ 300 GB)
• nanoda: เขียนไฟล์ export ขนาด 37.8 GB ใช้ RAM ราว 90 GB นานหนึ่งชั่วโมง แล้วตรวจอีกราว 30 นาทีที่ 16 เธรด
• ต้องเป็น Linux หรือ macOS เท่านั้น — Windows ใช้ไม่ได้เพราะ path บางอันยาวเกิน

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

”พิสูจน์ FLT” แปลว่าอะไร และไม่แปลว่าอะไร

นี่คือส่วนที่พาดหัวทุกสำนักข้ามไป และรีโปเขียนไว้เองอย่างชัดเจนในหัวข้อ “Exact strength of the named steps” ของ PROOF-PATH.md และในฟิลด์ fidelity.divergences ของ formalization.yaml

ข้อความระดับบนสุดเป็นข้อความ FLT มาตรฐานจริง และ comparator ยืนยันว่ามันเหมือนกับ FermatLastTheorem ของ Mathlib ทุกตัวอักษร ตรงนี้ไม่มีข้อสงสัย แต่ ทฤษฎีบทคลาสสิกที่อยู่ระหว่างทางถูกพิสูจน์เฉพาะรูปแบบที่ข้อโต้แย้งต้องใช้ ไม่ใช่ฉบับทั่วไป:

ทฤษฎีบท	ที่พิสูจน์จริง	ที่ไม่ได้พิสูจน์
Mazur	ความ irreducible ของ E_P[p] สำหรับเส้นโค้ง Frey (p ≥ 17 ผ่าน Eisenstein quotient; p ≤ 13 ปิดด้วย Kummer หรือ descent)	ทฤษฎีบท Mazur เรื่อง isogeny หรือ torsion ของเส้นโค้งทั่วไป
Langlands-Tunnell	เฉพาะกรณี octahedral พร้อม lift ชัดเจน สำหรับ ρ̄₃ ที่ surjective และมี determinant เป็น cyclotomic	automorphy ของ representation สองมิติคี่ทั่วไปที่มี soluble image
Modularity lifting	สองข้อความที่มีเงื่อนไข level สำหรับ semistable ที่ p = 3 และ p ∈ {3, 5}	ฉบับที่ไม่มีเงื่อนไข level, เส้นโค้งที่ไม่ semistable หรือ p อื่น
Wiles	โมเดล Weierstrass แบบ integral ที่ semistable ทุกตัว (Δ ≠ 0) เป็น modular ในความหมายที่ a_ℓ ตรงกัน	เส้นโค้งที่ไม่ semistable, modular parametrisation, L-function
Ribet	level lowering สำหรับ Frey representation ที่ level squarefree เป็น การสมภาคของ trace	ทฤษฎีบท Ribet สำหรับ modular mod-p representation ทั่วไป

พูดให้ตรงคือ FLT ได้รับการพิสูจน์จริงจากสัจพจน์สามข้อ ไม่มีการสมมติอะไรจากวรรณกรรม — นั่นคือข้อเท็จจริง แต่ Mathlib ไม่ได้มี Langlands-Tunnell ฉบับเต็มเพิ่มขึ้นมาจากงานนี้ ใครที่หวังว่าจะหยิบชิ้นส่วนไปใช้ต่อในงานทฤษฎีจำนวนอื่นต้องอ่าน PROOF-PATH.md ทีละบรรทัดก่อน

มีรายละเอียดหนึ่งที่รีโปเขียนเองแล้วน่าสนใจมาก: ในขั้น level lowering การพิสูจน์ “re-derives modularity itself, so the IsModular hypothesis above is formally unused” — คือสมมติฐานหนึ่งในโครงสร้างพิสูจน์ไม่ได้ถูกใช้จริง เพราะเอเจนต์ไปพิสูจน์ซ้ำเองข้างใน นี่คือร่องรอยของ “การพิสูจน์ที่ยาวเกินจำเป็น” ที่ Anthropic ยอมรับเองในเชิงอรรถว่าโค้ดชุดนี้ “likely much longer than it needs to be”

ยืนบนไหล่ชุมชน Lean — และรีโปนับให้ทีละไฟล์

ไฟล์ ATTRIBUTION.md ยาว 50 KB ระบุว่า 106 ไฟล์ ในรีโปมีเนื้อหาที่นำมาหรือดัดแปลงจาก โครงการ FLT ของ Imperial College London ที่นำโดย Kevin Buzzard (90 ไฟล์) และโครงการ flt-regular — แบ่งเป็น 54 ไฟล์ใต้ Definitions/ และ 52 ไฟล์ใต้ P2M/Sol/ บวกอีก 23 ไฟล์ที่ทำซ้ำข้อความจาก Mathlib หลายรายการในตารางระบุ extent ว่า “whole file (100%)” คือยกมาทั้งไฟล์ โดยสำเนาต้นทางถูกดึงมาจากสาขา main ของ ICL ณ วันที่ 21 พ.ค. 2026

ที่ต้องชมคือวิธีทำตารางนี้: เนื่องจากไฟล์ Lean ทั้งหมดถูกเผยแพร่โดยลบคอมเมนต์ออก หัวข้อลิขสิทธิ์ต้นทางจึงหายไปหมด ทีมจึงต้องไล่เทียบทีละบรรทัด (หลังตัด import/open/namespace) ระหว่าง 60,478 ไฟล์ .lean กับสำเนาต้นทาง เพื่อกู้การให้เครดิตกลับมา — และยอมรับตรง ๆ ว่าแถวของ flt-regular อ้างอิงจากบันทึกที่มีอยู่ก่อนเผยแพร่เท่านั้น เพราะไม่มีสำเนาโครงการนั้นไว้เทียบ

Kevin Buzzard ซึ่ง Anthropic ส่งงานให้ดูก่อน ให้ความเห็นว่าเป็น “extraordinary autoformalization achievement” และว่า “AI autoformalization artefacts are now robust enough to be built upon” — แต่ในไฟล์ formalization.yaml ช่อง review.status ยังเขียนว่า self-assessed และ reviewers: [] ว่างเปล่า ส่วนผู้เขียนบทความต้นทาง (Wiles, Taylor, Darmon-Diamond-Taylor) ถูกระบุสถานะว่า not-contacted

วิธีรัน: ลองแล้วพังก่อน แล้วค่อยได้ Prove2Me

รายละเอียดเชิงวิศวกรรมที่นักพัฒนาเอเจนต์ควรอ่าน: ความพยายามชุดแรกล้มเหลว Anthropic เขียนเองว่าเอเจนต์ “quickly lost track of the project’s state and stopped collaborating effectively” และงานที่ล้มเหลวนั้นยังหลงเหลืออยู่ราว 7% ของบรรทัดที่ไม่ใช่ boilerplate ในพิสูจน์สุดท้าย

สิ่งที่ทำให้สำเร็จคือการย้ายไปใช้ Prove2Me แพลตฟอร์มเปิดจากกลุ่มของ Tianyi Peng ที่ Columbia (arXiv 2608.28433, ส่ง 28 ส.ค.) คู่กับ harness หลายเอเจนต์ที่สร้างบน Claude Code โดย Prove2Me ช่วยสามอย่าง:

1. เก็บ DAG ของข้อความทฤษฎีบท ให้เอเจนต์เลือกเองว่าจะพิสูจน์อะไรต่อ — ลดปัญหาความจำเสื่อมและให้ทำงานขนานกันได้
2. แยกไฟล์ข้อความออกจากไฟล์พิสูจน์ ทำให้คอมไพล์ Lean เร็วขึ้นและกินทรัพยากรน้อยลง
3. เก็บคำอธิบายภาษาธรรมชาติของทุกทฤษฎีบท เพื่อให้ค้นและใช้ซ้ำได้

ทั้งหมดใช้ ~6 พันล้านโทเคนขาออก จาก “general-purpose internal research model roughly comparable to Claude Fable 5.1” — คือไม่ใช่โมเดลพิเศษเฉพาะทางคณิตศาสตร์ ส่วนอินพุตจากมนุษย์จำกัดอยู่ที่คำสั่งระดับสูงเป็นครั้งคราวจาก Peng เช่น “Jacobian as a scheme sounds high priority”

และตัวเลขที่น่าสนใจกว่าสำหรับคนทั่วไป: นักวิจัย Anthropic ทดลองใช้ บัญชี Claude Max ส่วนตัวสามบัญชี ผ่าน Prove2Me แล้วทำ formalization ของ ทฤษฎีบทสามจำนวนเฉพาะของ Vinogradov ได้ใน 3 วัน

มุมมอง AI Curator

เรื่องนี้ต่างจากข่าว “AI แก้โจทย์คณิตศาสตร์” ทั่วไปตรงที่ผลลัพธ์ตรวจสอบได้โดยไม่ต้องเชื่อใคร ไม่ต้องเชื่อ Anthropic ไม่ต้องเชื่อเบนช์มาร์ก ไม่ต้องเชื่อ harness — เคอร์เนล Lean ตรวจให้ และมีเคอร์เนลที่สองเขียนคนละภาษาตรวจซ้ำ ในโลกที่เราต้องเขียนข่าวเตือนเรื่อง reward hacking กับ benchmark ที่ผู้ขายวัดเองแทบทุกสัปดาห์ นี่คือรูปแบบการอ้างผลที่หายากมาก: ข้ออ้างที่มีเครื่องพิสูจน์ผิดได้อยู่ในตัว

แต่ต้องแยกให้ออกระหว่าง “ตรวจสอบได้” กับ “อ่านรู้เรื่อง” README เขียนเองว่าโค้ดชุดนี้ “written to be checked rather than read” ชื่อทั้งหมดถูกสร้างด้วยเครื่อง คอมเมนต์ถูกลบ และประโยคที่ควรถูกอ้างมากที่สุดคือ: “What no tool can check is that each intermediate theorem means what its name suggests” — เครื่องรับประกันได้แค่ว่าข้อความบนสุดตามมาจากสัจพจน์สามข้อ ส่วนทฤษฎีบทย่อย 29,500 ข้อจะ “มีความหมาย” ตามชื่อหรือไม่ ยังเป็นภาระของมนุษย์ ซึ่งไม่มีใครอ่าน 13 ล้านบรรทัดไหว คุณค่าทางคณิตศาสตร์ของงานนี้จึงอยู่ที่ข้อความเดียวข้างบน ไม่ใช่ที่คลังทฤษฎีบทข้างล่าง — ต่างจาก Mathlib ที่ทุกบรรทัดถูกออกแบบให้คนอื่นเอาไปใช้ต่อ และรีโปนี้ก็ประกาศตัวชัดว่า “Research artifact. Not maintained and not accepting contributions.”

สำหรับนักพัฒนาและนักวิจัยไทย บทเรียนที่ใช้ได้จริงไม่ใช่ FLT แต่คือ Vinogradov ใน 3 วันด้วยบัญชี Claude Max สามบัญชี — นั่นคือระดับทรัพยากรที่ภาควิชาคณิตศาสตร์หรือกลุ่มวิจัยในไทยเอื้อมถึงได้จริง โดยไม่ต้องมีคลัสเตอร์ GPU สักตัว Lean และ Mathlib เป็นโอเพนซอร์สทั้งคู่ Prove2Me ก็เปิด และงานที่ควรทำก่อนไม่ใช่การไล่พิสูจน์ทฤษฎีบทดัง แต่คือ การ formalize ผลงานที่กลุ่มตัวเองตีพิมพ์ไปแล้ว ซึ่งเป็นงานที่รู้คำตอบอยู่แล้วและวัดได้ว่าเครื่องมือทำงานจริงหรือไม่

ระยะยาว สิ่งที่งานนี้เปลี่ยนคือต้นทุนของการไม่เชื่อ เมื่อก่อนการตรวจพิสูจน์ยาว ๆ ใช้เวลาเป็นปีของมนุษย์ (Wiles ใช้เวลาสองเดือนกว่าจะมีคนพบช่องโหว่ แล้วอีกหนึ่งปีกว่าจะอุด) ตอนนี้ การ formalize ถูกกว่าการรีวิว และนั่นแปลว่าในไม่ช้าคำถาม “มี Lean ให้ดูไหม” อาจกลายเป็นคำถามมาตรฐานที่ referee ถามผู้ส่งบทความ ซึ่งจะกดดันงานที่ formalize ไม่ได้ให้ต้องอธิบายว่าทำไม — ผลข้างเคียงที่ต้องจับตาคือมันอาจเบียดคณิตศาสตร์สาขาที่ยังไม่มีฐาน Mathlib รองรับให้ดู “น่าเชื่อถือน้อยกว่า” ทั้งที่ไม่เกี่ยวกับความถูกต้องเลย

แหล่งข่าว

• Formalizing Fermat’s Last Theorem — Anthropic (4 ก.ย. 2026)
• anthropics/fermats-last-theorem — รีโปเต็ม Apache-2.0 (README, PROOF-PATH.md, formalization.yaml)
• Prove2Me: An Open Collaborative Platform for Scaling Math Formalization — arXiv 2608.28433
• ImperialCollegeLondon/FLT — โครงการชุมชนที่งานนี้ยกโค้ดมาใช้ 90 ไฟล์