# Claude พิสูจน์แฟร์มาต์ใน 11 วัน คำตัดสิน: SHIP IT.

Published: 2026-09-07

Claude ใช้เวลา 11 วันและประมาณ 6 พันล้านโทเค็นในการเขียนบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ด้วยภาษา Lean จำนวน 13 ล้านบรรทัด ซึ่งเป็นการตรวจสอบโดยคอมพิวเตอร์แบบครบวงจรเป็นครั้งแรก ในขณะที่นักคณิตศาสตร์ที่ได้ทำการปรับให้เป็นรูปแบบทางการมาตั้งแต่ปี 2024 กล่าวว่ามัน "ไม่ได้บอกอะไรเราเลย" ทางคณิตศาสตร์ แต่ก็ยังรู้สึกตื่นเต้นอยู่ดี ในวันเดียวกัน: ชิน จิน-ซอ นักหมากรุกโกะอันดับ 1 ของโลก เอาชนะ KataGo 2–1 ด้วยแต้มต่อสองเม็ด คำตัดสิน: SHIP IT.

Canonical: https://thedailydiff.dev/th/video/2026-09-04-fermat-lean/

## วิดีโอนี้ครอบคลุมอะไรบ้าง

- Claude ปรับทฤษฎีบทสุดท้ายของแฟร์มาต์ให้เป็นรูปแบบทางการใน Lean 4
- Chromium sandbox RCE (CVE-2026-85046) ที่ถูกใช้ประโยชน์ในโลกจริง ค่าหัว $1,000
- ชิน จิน-ซอ เอาชนะ KataGo ด้วยแต้มต่อสองเม็ด

## บทถอดเสียงที่แปลแล้ว

แปลจากการบรรยายภาษาอังกฤษต้นฉบับ เสียงและคำบรรยายที่มีให้จะควบคุมโดย YouTube

0:00 แฟร์มาต์กล่าวว่าบทพิสูจน์อันน่าทึ่งของเขาจะไม่พอดีกับขอบกระดาษ และวันนี้ Anthropic ได้เผยแพร่ขอบกระดาษนั้น: สิบสามล้านบรรทัดของ Lean ใหญ่กว่า Mathlib ห้าเท่า พิสูจน์ทฤษฎีบทที่นักคณิตศาสตร์ทุกคนเชื่ออยู่แล้ว มันเป็นเวลาสิบโมงถึงสิบเอ็ดโมงในทบิลิซีเมื่อ Anthropic โพสต์ ดังนั้นผมก็เลยตื่นเป็นเรื่องปกติ เมื่อวาน Google ได้ออก Chrome 152 พร้อมกับการแก้ไขความปลอดภัยสิบสองรายการ หนึ่งในนั้นคือบั๊ก V8 ที่ถูกใช้ประโยชน์ในโลกจริง และจ่ายเงินให้ผู้รายงาน หนึ่งพันดอลลาร์ ซึ่งน้อยกว่ารถเก๋งที่เราจะพูดถึงในภายหลัง

0:26 เมื่อวานนี้ Mullvad ยังกล่าวด้วยว่ากำลังจะปิด DNS แบบเข้ารหัสสาธารณะใน วันที่ 2 พฤศจิกายน และจ่ายเงินให้ Quad9 ทำแทน และเช้านี้ Rust React Compiler กลายเป็นเนทีฟใน Vite ในขณะที่ Hacker News ค้นพบ IBM Bob เอเจนต์เขียนโค้ด AI จากนั้น Claude ก็ปรับทฤษฎีบทสุดท้ายของแฟร์มาต์ให้เป็นรูปแบบทางการ และในหน้าแรกเดียวกัน ปรมาจารย์ชาวเกาหลีเอาชนะเอนจินโกะที่แข็งแกร่งที่สุดในโลก ดังนั้นวันนี้มนุษยชาติจึงทำได้หนึ่งในสอง ในวิดีโอนี้: Claude พิสูจน์อะไรจริงๆ, ค่าใช้จ่ายเท่าไหร่

0:52 ทำไมนักคณิตศาสตร์ที่ใช้ชีวิตในการทำสิ่งนี้ถึงบอกว่ามันไม่เปลี่ยนแปลงอะไรเลยและ ยังตื่นเต้นอยู่ดี และมนุษย์เอาชนะเครื่องจักรในหมากรุกโกะได้อย่างไร วันนี้วันศุกร์ที่ 4 กันยายน และนี่คือ The Daily Diff ทฤษฎีบทสุดท้ายของแฟร์มาต์: ไม่มีจำนวนเต็มบวก a, b, c ที่สอดคล้องกับ a ยกกำลัง n บวก b ยกกำลัง n เท่ากับ c ยกกำลัง n สำหรับ n ที่มากกว่า 2 แฟร์มาต์ขีดเขียนไว้ที่ขอบกระดาษประมาณปี 1637 และเสียชีวิตโดยไม่ได้แสดงผลงานของเขา ทำให้เขากลายเป็นนักพัฒนาคนแรกที่ปิดงานด้วยคำว่า 'works on my machine' รางวัล 100,000 มาร์กทองในปี 1908 ดึงดูดบทพิสูจน์ที่ผิดพลาด 621 บท

1:25 ในปีแรก และแอนดรูว์ ไวลส์ก็สามารถพิสูจน์ได้สำเร็จในปี 1995 ใน 129 หน้าที่ต้องใช้เวลาหลายเดือนในการตรวจสอบ การทำให้เป็นรูปแบบทางการหมายถึงการเขียนบทพิสูจน์นั้นใหม่เพื่อให้ Lean ซึ่งเป็นผู้ช่วยพิสูจน์ สามารถตรวจสอบทุกขั้นตอนได้ด้วยกลไก และเควิน บัซซาร์ดที่ Imperial ได้นำความพยายามของมนุษย์ เพื่อให้ทำเช่นนั้นมาตั้งแต่ปี 2024; เพียงพิมพ์เขียวอย่างเดียวก็ยาว 86 หน้า เทียนยี่ เพ็ง นักวิจัยของ Anthropic ได้ชี้แนะเอเจนต์ Claude หลายสิบตัวไปที่มัน แทน บนแพลตฟอร์มที่ชื่อว่า Prove2Me ซึ่งเก็บ DAG ของข้อความทฤษฎีบท เพื่อให้เอเจนต์รู้ว่าจะพิสูจน์อะไรต่อไป เพราะหากไม่มีสิ่งนี้ ฝูงแรก

2:00 ก็จะหลงทางว่าใครกำลังพิสูจน์อะไร ซึ่งเป็นสิ่งที่เกิดขึ้นเมื่อเลเยอร์การจัดระเบียบของคุณ คือ regex ที่มีงบประมาณการตลาด สิบเอ็ดวันต่อมา โหนดรากอ่านว่า PROVED: สิบสามล้านบรรทัดของ Lean ทฤษฎีบทกลาง 29,500 ทฤษฎี ประมาณหกพันล้านโทเค็นจาก โมเดลภายในที่เทียบเท่ากับ Claude Fable 5.1 การสร้างจะล้มเหลวหากบทพิสูจน์ไม่ได้อยู่บนสัจพจน์มาตรฐานสามข้อของ Lean: ไม่ใช่ ขอโทษ ไม่มี native decide ไม่โกง การตรวจสอบก็ไม่ถูกเช่นกัน: การสร้างใหม่

2:29 จากศูนย์ใช้เวลาห้าชั่วโมงครึ่ง บน 96 คอร์และ RAM 153 กิกะไบต์ และชื่อทฤษฎีบทเป็น ที่สร้างโดยเครื่อง ดังนั้น repo จึงอธิบายตัวเองว่าเขียนขึ้นเพื่อตรวจสอบมากกว่า ที่จะอ่าน ซึ่งเป็นวิธีที่ผมจะอธิบาย Java สำหรับองค์กรเช่นกัน ตอนนี้คือข้อขัดแย้ง โพสต์ของ Anthropic กล่าวว่า Lean แสดงความถูกต้องโดยปราศจากข้อสงสัย เควิน บัซซาร์ด ชายผู้ถูกแซงหน้า ได้คอมไพล์ repo บนเครื่อง 500 กิกะไบต์ ที่ Anthropic ให้ยืมมา ยืนยันว่าตรวจสอบผ่าน และจากนั้นก็เขียนว่า

2:56 อ้างอิง: ทางคณิตศาสตร์แล้วงานนี้ไม่ได้บอกอะไรเราเลย เขาค่อนข้างแน่ใจอยู่แล้ว 99.9 เปอร์เซ็นต์ว่าทฤษฎีบทเป็นจริง และบทพิสูจน์นี้ไม่ได้เพิ่มคณิตศาสตร์ใหม่ใดๆ สิ่งที่มันแสดงคือสิ่งที่การจัดรูปแบบอัตโนมัติสามารถทำได้ ตอนนี้ และส่วนนั้นเขาตื่นเต้นจริงๆ เขาได้รับหนึ่งล้านปอนด์เป็นเวลาห้าปี Anthropic ใช้เวลาสิบเอ็ดวัน และการคำนวณแบบง่ายๆ ของผู้แสดงความคิดเห็นระบุว่าหกพันล้านโทเค็นมีราคาตามรายการ ประมาณ 300,000 ดอลลาร์ ดังนั้นเครื่องจักรจึงถูกกว่า เว้นแต่คุณจะนับการฝึกอบรมเครื่องจักร ซึ่งไม่มีใครทำ

3:24 รายละเอียดที่ดีที่สุด: อีเมลมาถึงขณะที่เขาอยู่ที่เทศกาลดนตรีในเวลส์พร้อม 4G หนึ่งขีด จากชื่อที่ไม่เคยได้ยินมาก่อน เขาจึงคิดว่าเป็นอีเมลหลอกลวง และอ่านมันในอีกหนึ่งสัปดาห์ต่อมา ซึ่งเป็นการตอบสนองที่ถูกต้องต่อหัวเรื่องใดๆ ที่มีคำว่า 'end-to-end formalization' อยู่ด้วย ขณะเดียวกัน มนุษย์ก็เอาชนะได้อีกครั้ง ชิน จิน-ซอ นักเล่นโกะมือหนึ่งของโลก เอาชนะ KataGo เอนจินโกะโอเพนซอร์สที่แข็งแกร่งที่สุด ไปสองเกมต่อหนึ่งเกมในกรุงโซล โดยมีการให้หมากสองเม็ด ซึ่งเป็นช่องว่างระหว่างมืออาชีพอันดับต้นๆ กับมืออาชีพหน้าใหม่

3:50 เกมตัดสินคือการชนะ 11.5 แต้มใน 221 กระบวนท่า โดยมีโอกาสชนะ 99 เปอร์เซ็นต์ตั้งแต่กลางเกม และเขาได้รับเงินรางวัล 250 ล้าน วอน ประมาณ 170,000 ดอลลาร์ บวกกับ Genesis G90 ดังนั้นรางวัลสำหรับการ เอาชนะ AI เหนือมนุษย์คือ 170 เท่าของรางวัลของ Google สำหรับการหลบหนี Chrome sandbox คำอธิบายของเขา: ในช่วงแรกเขาเลียนแบบการเดินของ AI แล้วแพ้; เขาชนะโดยการ สร้างกระดานในสไตล์ของเขาเอง ซึ่งเป็นคำแนะนำที่เป็นประโยชน์ที่สุดเกี่ยวกับ AI ที่ฉัน ได้ยินมาตลอดทั้งปี และมันมาจากเกมกระดาน มีอีกสองบรรทัดใน The Daily Diff

4:22 Rust React Compiler จาก oxc ตอนนี้เป็น native ใน Vite โดยมีแฟล็กเดียว; โค้ดเบสขนาด 1,036 ไฟล์ ใช้เวลาคอมไพล์จาก 14.3 วินาที เหลือ 0.81 วินาทีใน ขั้นตอนการคอมไพล์ ส่วนใหญ่โดยการลบ Babel ออกจาก package.json ซึ่งเป็นกิจวัตรการดูแลผิวของฉันด้วย และ IBM ได้เปิดตัว Bob ซึ่งเป็น AI คู่หูในการเขียนโค้ดที่ทักทายคุณว่า 'สวัสดี' ฉันชื่อ Bob สร้าง subagents ปรับปรุงโค้ดเมนเฟรม และจัดส่งผลิตภัณฑ์วิเคราะห์ที่ชื่อว่า Bobalytics ดังนั้นที่ไหนสักแห่งธนาคารกำลังตื่นเต้นมาก และไม่มีใครอ่านใบอนุญาต

4:51 นั่นเป็นส่วนต่างที่มากสำหรับวันศุกร์วันเดียว; หากคุณต้องการอ่านสิ่งนี้มากกว่าฟังฉัน พูด The Daily Diff จะส่งถึงกล่องจดหมายของคุณทุกเช้า — ฟรีที่ thedaily diff.dev ลิงก์อยู่ด้านล่าง ดังนั้น คำตัดสินของวันนี้: SHIP IT kernel บอกว่าใช่ Buzzard บอกว่าใช่ คณิตศาสตร์ไม่ได้เปลี่ยนไป แต่วิธีที่เราตรวจสอบคณิตศาสตร์เพิ่งเปลี่ยนไป นั่นคือ The Daily Diff ของวันนี้ ฉันนิโก้จาก Axrisi

5:09 รวมอย่างมีความรับผิดชอบ

## แหล่งที่มา

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com