นักคณิตศาสตร์เดินหน้าพิสูจน์ 'ทฤษฎีบทสุดท้ายของแฟร์มาต์' ปัญหายาก 350 ปีด้วยคอมพิวเตอร์

จะพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ใหม่อีกครั้งด้วยภาษาคอมพิวเตอร์

• ศาสตราจารย์ Kevin Buzzard แห่ง Imperial College London มีแผนจะเขียนการพิสูจน์เชิงรูปนัยของ ทฤษฎีบทสุดท้ายของแฟร์มาต์ (FLT) ด้วย Lean theorem prover ตั้งแต่เดือนตุลาคม 2024 เป็นต้นไป
• Engineering and Physical Sciences Research Council [EPSRC] ของสหราชอาณาจักรตกลงจะสนับสนุนทุนวิจัยให้ศาสตราจารย์ Buzzard เป็นเวลา 5 ปีนับจากเดือนนั้น
• แผนโครงการที่สร้างด้วยปลั๊กอิน plasTeX ชื่อ Lean blueprints มีกำหนดเผยแพร่ในช่วงปลายเดือนเมษายน 2024

ทฤษฎีบทสุดท้ายของแฟร์มาต์ยังไม่ได้รับการพิสูจน์ไปแล้วหรือ?

พิสูจน์แล้ว นักคณิตศาสตร์ชาวอังกฤษ Andrew Wiles เปิดเผยบทพิสูจน์ในปี 1994 และได้รับการตีพิมพ์อย่างเป็นทางการในปี 1995 แต่จนถึงตอนนี้ยังไม่มีการพิสูจน์เชิงรูปนัยที่เขียนด้วยภาษาของตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบ [ITP]

ตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบ? การพิสูจน์เชิงรูปนัย? นั่นคืออะไร?

• ตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบ [ITP]: โปรแกรมคอมพิวเตอร์ที่ช่วยให้มนุษย์เขียนการพิสูจน์เชิงรูปนัย หรือเรียกอีกอย่างว่า proof assistant
• การพิสูจน์เชิงรูปนัย: การพิสูจน์ที่สามารถตรวจสอบได้ด้วยโปรแกรมคอมพิวเตอร์ที่เรียกว่า proof verifier โดยปกติ proof assistant ก็มักทำหน้าที่เป็น proof verifier ด้วย

ตัวพิสูจน์ทฤษฎีบทเป็นปัญญาประดิษฐ์หรือไม่?

Neural theorem prover [NTP] อาจถือว่าใช่ แต่ตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบจำนวนมากรวมถึง Lean ไม่ได้เป็นโปรแกรมที่อาศัย machine learning

ช่วยแนะนำ Lean theorem prover หน่อย

• เป็นทั้งตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบและภาษาการเขียนโปรแกรมเชิงฟังก์ชันล้วน
• สร้างอยู่บน dependent type theory
• มีความสามารถอย่าง type class, ไวยากรณ์ที่ขยายได้, macro และ metaprogramming
• เมื่อเทียบกับ proof assistant อื่น ๆ ฐานผู้ใช้ของ Lean มี(นักคณิตศาสตร์ที่ทำวิจัยในสาขานอกเหนือจากรากฐานคณิตศาสตร์)อยู่มากเป็นพิเศษ

ทำไมถึงต้องเขียนการพิสูจน์เชิงรูปนัยของทฤษฎีบทสุดท้ายของแฟร์มาต์?

หากอ้างคำพูดของศาสตราจารย์ Kevin Buzzard จาก โพสต์บน X ว่า "เพื่อทำให้คอมพิวเตอร์เข้าใจทฤษฎีจำนวนสมัยใหม่ และท้ายที่สุดจะได้ช่วยนักทฤษฎีจำนวนได้"

ลิงก์

• ข้อความที่ศาสตราจารย์ Kevin Buzzard โพสต์ในแชต Lean Zulip เมื่อวันที่ 3 ตุลาคม 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
• ไลบรารีคณิตศาสตร์ของ Lean: https://github.com/leanprover-community/mathlib4
• บทความจาก New Scientist: https://institutions.newscientist.com/article/…
• บทความจาก Popular Mechanics: https://popularmechanics.com/science/math/…

[calofmijuck]

ขอเป็นกำลังใจให้ครับ สำหรับผู้ที่สนใจ Formal proof ก็ขอแนะนำให้ลองฟังบรรยาย Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) ของศาสตราจารย์ Terrence Tao ดูเช่นกันครับ