ในขณะที่ AI อย่าง OpenAI ได้เผยแพร่วารสารถึง 719 ฉบับที่อ้างว่าค้นพบคำตอบสำหรับปัญหาทางคณิตศาสตร์ที่ยากที่สุด แต่ Axiom มองว่าการตรวจสอบความถูกต้องนั้นแตกต่างอย่างสิ้นเชิง
Stacks Project เป็นการรวบรวมคณิตศาสตร์ที่ใหญ่ที่สุดเท่าที่มนุษย์เคยสร้างขึ้น ซึ่งมีการใช้กระบวนการที่คล้ายกับการพิสูจน์ทางคณิตศาสตร์แบบดั้งเดิม โดยใช้ Lean และ Proof assistant ในการตรวจสอบอย่างละเอียด
Axiom เชื่อว่าผลลัพธ์ที่ได้รับการตรวจสอบเหล่านี้จะกลายเป็นโครงสร้างพื้นฐานให้กับการพิสูจน์ในอนาคต แทนที่จะต้องเริ่มต้นใหม่ทั้งหมด ซึ่งสอดคล้องกับแนวคิดของ Terence Tao ที่ว่า ยิ่งพิสูจน์เป็นทางการมากเท่าไหร่ ก็จะยิ่งสามารถทำพิสูจน์ที่เป็นทางการได้มากขึ้นเท่านั้น
ศัพท์ที่ควรรู้
- OpenAI – บริษัทที่พัฒนา AI และได้เผยแพร่วารสารทางคณิตศาสตร์จำนวนมาก
- Stacks Project – โครงการที่รวบรวมคณิตศาสตร์ที่ได้รับการพิสูจน์และตรวจสอบอย่างเป็นทางการ
- Lean – ภาษาโปรแกรมที่ใช้ในการเขียนพิสูจน์ทางคณิตศาสตร์
- Proof assistant – โปรแกรมที่ช่วยตรวจสอบโค้ดที่ใช้ในการพิสูจน์ทีละบรรทัด
- Formal verification – กระบวนการตรวจสอบความถูกต้องของระบบ เช่น การออกแบบชิป
ที่มา: TechCrunch