เกิดอะไรขึ้น
- Claude ผลิตบทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์แบบที่คอมพิวเตอร์ตรวจครบเป็นครั้งแรก ใช้โปรแกรม Lean ซึ่งเป็นผู้ช่วยตรวจว่าทุกขั้นตอนถูกต้องจริง (Anthropic)
- งานนี้คือการเอาคณิตศาสตร์ที่มีอยู่แล้วมาเขียนให้เครื่องอ่านได้ ตามบทเล่าย่อของ Darmon–Diamond–Taylor ที่ตามรอยบทพิสูจน์เดิมของ Wiles ไม่ใช่การคิดบทพิสูจน์ใหม่เองแบบปี 1995 (Anthropic)
- Claude ทำงานเองเกือบทั้งหมด ฝ่ายคนแทรกเฉพาะคำสั่งภาพใหญ่เป็นครั้งคราว โดยนักวิจัย Tianyi Peng (Anthropic)
- ทีมใช้แพลตฟอร์ม Prove2Me ที่ Tianyi Peng กับเพื่อนร่วมงานที่มหาวิทยาลัยโคลัมเบียออกแบบไว้ (Anthropic)
- บทพิสูจน์สุดท้ายผ่านการตรวจของ Lean ใช้สัจพจน์มาตรฐานแค่ 3 ข้อ และมีตัวเทียบยืนยันว่าข้อความตรงกับที่คลัง Mathlib ใช้ (Anthropic)
- เปิดบทพิสูจน์เต็มไว้บน GitHub ที่ anthropics/formal-math (Anthropic)
ตัวเลขที่บริษัทประกาศ
- ทำงานต่อเนื่องราว 11 วัน แบบอัตโนมัติเป็นหลัก (Anthropic)
- เขียนโค้ด Lean ประมาณ 13 ล้านบรรทัด (Anthropic)
- พิสูจน์ทฤษฎีบทขั้นกลางราว 29,500 บทที่ตกมาในบทพิสูจน์สุดท้าย โพสต์บอกด้วยว่าตลอดทางพิสูจน์สะสมราว 30,300 บท (Anthropic)
- ใช้โทเคนผลลัพธ์ราว 6 พันล้าน จากโมเดลวิจัยภายในอเนกประสงค์ที่ใกล้เคียงระดับ Claude Fable 5.1 (Anthropic)
ทฤษฎีนี้คืออะไร
- ทฤษฎีบทสุดท้ายของแฟร์มาต์สั้น ๆ คือไม่มีจำนวนเต็มบวกสามตัวที่ทำให้ a^n + b^n = c^n ได้พอดี เมื่อ n มากกว่า 2 (Anthropic)
- มนุษย์พิสูจน์สำเร็จครั้งแรกปี 1995 โดย Andrew Wiles บทพิสูจน์ยาวราว 129 หน้า (Anthropic)
- ทีมชุมชนที่ Kevin Buzzard นำเคยคาดว่าต้องใช้เวลาหลายปี แค่พิมพ์เขียวเฟสแรกก็ยาวราว 86 หน้า (Anthropic)
- บริษัทนี้ย้ำว่าต่างจากงาน AI เรื่องสมมติฐานของรีมันน์ที่อ้างว่าได้คณิตศาสตร์ใหม่ จุดใหม่ของงานนี้คือการตรวจยืนยัน (Anthropic)
คนนอกพูดอะไร
- Kevin Buzzard จาก Imperial College London เรียกงานนี้ว่าความสำเร็จออโต้ฟอร์มัลไเซชันที่วิเศษ หมายถึงการแปลงคณิตศาสตร์ให้เครื่องตรวจได้โดยอัตโนมัติ (Kevin Buzzard)
- เขาบอกว่าบทพิสูจน์นี้ใช้สมมติฐานแค่สัจพจน์ของคณิตศาสตร์เท่านั้น ไม่มีเงื่อนไขแอบแฝง (Kevin Buzzard)
- เขามองว่างานลักษณะนี้ตอนนี้แน่นพอที่คนอื่นจะต่อยอดได้ เพราะบทพิสูจน์เป็นชั้น ๆ (Kevin Buzzard)
- เขาเสริมว่าถ้าทำกับทฤษฎีแฟร์มาต์ได้แล้ว ก็เท่ากับเดินไปได้ไกลมากบนเส้นทางแปลงตำราคณิตศาสตร์สมัยใหม่ให้เครื่องตรวจ ช่วยจับจุดพลาด ลดภาระผู้ตรวจบทความ และตรวจคณิตที่ AI เขียน (Kevin Buzzard)
สรุป
Claude ยังไม่ได้หาคำตอบใหม่ที่มนุษย์ไม่เคยรู้ แต่เพิ่งทำให้บทพิสูจน์ระดับตำนานถูกตรวจซ้ำด้วยเครื่องได้ครบทั้งบท ใครทำงานคณิตศาสตร์หรือสนใจ AI น่าจะได้คุยเรื่องนี้กันอีกเยอะ
แหล่ง: Anthropic · 4 ก.ย. 2026