Claude ทำการพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มา (Fermat's Last Theorem) ในรูปแบบทางการด้วย Lean
เมื่อเร็วๆ นี้ Anthropic ได้เสร็จสิ้นภารกิจการวิจัยครั้งใหญ่ โดยโมเดลภายในได้ทำงานต่อเนื่องเป็นเวลา 11 วัน เพื่อทำการพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มา (Fermat's Last Theorem) ในรูปแบบทางการ (formalize) โดยใช้ภาษาสำหรับการพิสูจน์อย่าง Lean 4
นี่ไม่ใช่การค้นพบทางคณิตศาสตร์ใหม่ แต่อย่างใด เนื่องจาก Andrew Wiles ได้พิสูจน์ทฤษฎีบทนี้ไปแล้วในปี 1995 สิ่งที่ Anthropic ทำคือการแปลงการพิสูจน์ที่มีอยู่แล้วนั้นให้กลายเป็นโค้ด ซึ่งช่วยให้คอมพิวเตอร์สามารถตรวจสอบทุกขั้นตอนทางตรรกะได้อย่างแม่นยำและแน่นอนที่สุด
ขนาดของโปรเจกต์นี้ถือว่ามหาศาล: • โมเดลสร้างโค้ด Lean ออกมาถึง 13 ล้านบรรทัด • พิสูจน์ทฤษฎีบทระดับกลาง (intermediate theorems) ได้ถึง 30,300 ทฤษฎีบท • ใช้ output tokens ไปเกือบ 6 พันล้านโทเคน
โมเดลส่วนใหญ่ทำงานด้วยตัวเอง โดยมนุษย์จะคอยให้คำแนะนำในระดับสูงเป็นครั้งคราวเท่านั้น กระบวนการนี้เสร็จสิ้นลงในช่วงกลางดึกในขณะที่ไม่มีใครเฝ้าดูอยู่ และระบบได้บันทึกความสำเร็จนี้โดยอัตโนมัติ
มีสองสิ่งที่สำคัญที่ควรทราบ:
- โมเดลนี้เป็นเครื่องมือวิจัยภายใน คุณยังไม่สามารถเข้าถึงผ่าน API ได้ และมันไม่ใช่โมเดล Claude แบบเดียวกับที่คุณใช้งานอยู่ในปัจจุบัน
- คุณค่าที่แท้จริงสำหรับนักพัฒนาอยู่ที่เลเยอร์การประสานงาน (coordination layer) ที่เรียกว่า Prove2Me
Prove2Me เป็นเครื่องมือโอเพนซอร์ส (open source) ที่ใช้ dependency graph ในการจัดการงาน แทนที่จะเป็นเพียงรายการตรวจสอบ (checklist) แบบธรรมดา แต่มันจะสร้างแผนผังที่แสดงให้เห็นว่าการพิสูจน์แต่ละอย่างเชื่อมโยงกันอย่างไร
โครงสร้างนี้ช่วยแก้ปัญหาหลักสองประการสำหรับเวิร์กโฟลว์ของเอเจนต์ (agent workflows):
- ช่วยป้องกันไม่ให้เอเจนต์หลายตัวทำงานซ้ำซ้อนกัน
- ช่วยให้เอเจนต์มีหน่วยความจำร่วมกัน (shared memory) เพื่อไม่ให้ลืมเป้าหมายหลัก
เวิร์กโฟลว์ของเอเจนต์ส่วนใหญ่มักล้มเหลวเนื่องจากสูญเสียบริบท (context) เมื่อเวลาผ่านไป การใช้กราฟภายนอกที่ใช้ร่วมกันแทนที่จะเป็นหน้าต่างแชทที่ยาวเหยียด จะช่วยให้การทำงานยังคงอยู่ในเส้นทางที่ถูกต้อง
คุณควรศึกษาโครงสร้าง (architecture) ของ Prove2Me หากคุณกำลังสร้างเวิร์กโฟลว์ของเอเจนต์ แม้ว่าคุณจะไม่ได้ใช้โมเดลวิจัยของ Anthropic แต่แนวทางการประสานงานภารกิจของพวกเขาก็ถือเป็นต้นแบบ (blueprint) สำหรับการทำงานที่ต้องใช้ระยะเวลานาน (long horizon work)
ที่มา: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36
ชุมชนการเรียนรู้เพิ่มเติม: https://t.me/GyaanSetuAi