AI ของ Axiom Math ตรวจสอบทฤษฎีช่องว่างจำนวนเฉพาะ 246 ใน Lean

Axiom Math กล่าวว่า ระบบ AxiomProver ของบริษัทได้สร้างหลักฐาน Lean 4 ที่ตรวจสอบด้วยเครื่องจักรซึ่งเป็นผลลัพธ์ที่แข็งแกร่งที่สุดที่รู้จักเกี่ยวกับช่องว่างระหว่างจำนวนเฉพาะ: ทฤษฎีที่ระบุว่ามีคู่จำนวนเฉพาะไม่จำกัดจำนวนที่ต่างกันไม่เกิน 246. บริษัทได้เผยแพร่ผลลัพธ์นี้เมื่อวันที่ 17 สิงหาคม 2026 ในรูปแบบพิมพ์เขียวการทำรูปแบบอย่างเป็นทางการแบบโต้ตอบ ซึ่งให้เครดิตแก่ผู้ร่วมทำงาน 41 คนจากคณิตศาสตร์ วิศวกรรม และผู้ตรวจสอบหลัก, พร้อมกับ IEEE Spectrum รายงานเป็นครั้งแรก.

ขอบเขต 246 นี้เป็นขอบเขตสุดยอดของความรู้ของมนุษย์ในการต่อสู้ระยะยาวกับสมมติฐานจำนวนเฉพาะคู่ (twin prime conjecture) ซึ่งเป็นสมมติฐานศตวรรษที่ 19 ที่กล่าวว่าจำนวนเฉพาะที่ห่างกันสองจำนวนจะปรากฏอย่างต่อเนื่องตลอดไป. หน้าโครงการของ Axiom Math อธิบายงานนี้ว่าเป็นการทำรูปแบบอย่างเป็นทางการแบบรวมของบทความของ James Maynard ปี 2013 “Small gaps between primes” พร้อมกับส่วนที่ตามมาจากความร่วมมือ Polymath8b ที่ทำให้ขอบเขตของ Maynard จาก 600 ลดลงเหลือ 246. หลักฐานที่ตรวจสอบด้วยเครื่องจักรถูกจัดระเบียบเป็นห้องสมุด Lean สาธารณะชื่อ PrimeGapsLib, โดยมีทฤษฎี 246 เป็นผลลัพธ์หลักของห้องสมุดนี้.

“ทฤษฎีนี้ในขณะนี้เป็นจุดศูนย์กลางของความรู้ของมนุษย์เกี่ยวกับจำนวนเฉพาะ” เคน โอโนะ นักคณิตศาสตร์ผู้ก่อตั้งของ Axiom Math กล่าว.

การตรวจสอบอย่างเป็นทางการหมายถึงการแปลงหลักฐานเป็นภาษาที่โปรแกรมขนาดเล็กที่เชื่อถือได้ซึ่งเรียกว่า kernel สามารถตรวจสอบได้ทีละบรรทัด. ผลลัพธ์ไม่ได้เป็นการรับประกันแบบสัมบูรณ์ — ต้องแปลงข้อความอ้างอิงอย่างถูกต้องและตัวตรวจสอบต้องเป็นเชิงเสียง — แต่ช่วยขจัดความบกพร่องของผู้ตรวจสอบมนุษย์ออกจากกระบวนการ. จนถึงตอนนี้ ระบบ AI ที่แข่งขันในมาตรฐานคณิตศาสตร์ส่วนใหญ่ถูกวัดจากปัญหาการแข่งขันที่มีหลักฐานสั้นและเป็นอิสระ; ช่องว่างระหว่างผลลัพธ์เหล่านั้นกับการทำรูปแบบระดับการวิจัยยังคงกว้าง, ซึ่งเป็นรูปแบบที่เห็นได้จาก ระบบก่อนหน้าที่โดดเด่นในเรขาคณิตโอลิมปิก ในขณะที่ยังคงไม่แตะต้องคณิตศาสตร์การวิจัยอย่างมาก.

จาก 70 ล้านถึง 246

สมมติฐานเองที่อัลฟอนส์ เดอ โพลินยัก (Alphonse de Polignac) สร้างขึ้นอย่างแม่นยำในศตวรรษที่ 19 ยังคงไม่มีการพิสูจน์. ขอบเขตจำกัดแรกที่เป็นที่รู้จักปรากฏในปี 2013 เมื่อหย่ง จาง (Yitang Zhang) พิสูจน์ว่ามีคู่จำนวนเฉพาะไม่จำกัดจำนวนที่อยู่ภายในระยะ 70 ล้านจากกัน. ไม่กี่เดือนต่อมา เมย์นาร์ด (Maynard) ได้นำวิธีการกรองที่ปรับปรุงใหม่และลดขอบเขตลงเหลือ 600 — งานที่มีส่วนช่วยให้เขาได้รับเหรียญฟิลด์ส์เมดัลในปี 2022 — และความร่วมมือ Polymath8b ซึ่งรวมเมย์นาร์ดและเทอเรนซ์ เต้า (Terence Tao) นำขอบเขตนี้ไปถึง 246. พิมพ์เขียวของ Axiom Math แสดงลำดับความก้าวหน้านี้เป็นโครงการที่ตั้งเป้าหมายให้ทำรูปแบบอย่างเป็นทางการ.

การทำรูปแบบอย่างเป็นทางการดำเนินตามขั้นตอนที่บริษัทอธิบายในสามขั้นตอน. นักวิจัยแรกเขียนหลักฐานเป็นพิมพ์เขียว — ทุกคำนิยาม, เลมม่า, และทฤษฎีได้รับป้ายกำกับ, คำอธิบายที่แม่นยำ, และรายการผลลัพธ์ที่อ้างอิง — สร้างกราฟการพึ่งพาที่จัดลำดับงาน. จากนั้น AxiomProver, ระบบหลายเอเจนต์ของบริษัทสำหรับการวิจัยคณิตศาสตร์ผ่านหลักฐานอย่างเป็นทางการ, สร้างหลักฐาน Lean 4 ที่เครื่องตรวจสอบได้โดยอิงจาก Mathlib, ห้องสมุดคณิตศาสตร์ของชุมชน, และ PrimeNumberTheoremAnd, โครงการทำรูปแบบที่มีอยู่แล้วซึ่งนำโดยอเล็กซ์ คอนโทรริช (Alex Kontorovich) และเทอเรนซ์ เต้า. ทีมของ Axiom จากนั้นตรวจสอบโค้ดที่สร้างขึ้นและจัดระเบียบเป็น PrimeGapsLib.

ผลลัพธ์หลักที่ระบุของห้องสมุดนี้ไปไกลกว่าทฤษฎีหัวข้อหลักเล็กน้อย. นอกจากขอบเขต 246 แล้ว ยังทำรูปแบบขอบเขต 600 ของเมย์นาร์ด และรวมถึงความท้าทายการตรวจสอบแบบอิสระ — สร้างขึ้นเฉพาะบน Mathlib โดยปล่อยช่องหลักฐานว่างไว้ — ที่ให้ผู้ใดที่มีเครื่องมือเปรียบเทียบ Lean สามารถยืนยันได้อย่างอิสระว่าหลักฐานของห้องสมุดตรงกับทฤษฎีที่ระบุ. บริษัทเตือนว่าการตรวจสอบเต็มรูปแบบอาจใช้เวลาหลายชั่วโมง; เวอร์ชันที่ลดขนาดครอบคลุมผลลัพธ์สองอื่นสามารถทำได้ในไม่กี่นาที.

ตำแหน่งของผลลัพธ์นี้ในข้ออ้างอิงการทำรูปแบบอย่างเป็นทางการของ AI

ผลลัพธ์นี้ปรากฏในปีที่ข้ออ้างเกี่ยวกับระบบ AI ที่ทำคณิตศาสตร์ระดับการวิจัยเพิ่มขึ้นอย่างต่อเนื่อง, ส่วนใหญ่อิงกับคะแนนการแข่งขันหรือหลักฐานสั้น. Axiom Math เป็นหนึ่งในผู้อ้างที่ก้าวร้าวที่สุด: AxiomProver ได้รับเครดิตจากการแก้ปัญหาที่เปิดอยู่ก่อนหน้า, รวมถึงงานที่บริษัทได้ตีพิมพ์ในวารสารที่ผ่านการตรวจสอบโดยผู้ทรงคุณวุฒิ, และ ระบบ AI ได้แก้ปัญหา Erdős ที่ค้างคามานานหลายรายการแล้ว. การทำรูปแบบ 246 นี้เป็นผลลัพธ์ประเภทต่าง — ไม่ใช่ทฤษฎีใหม่, แต่เป็นการสร้างใหม่ที่ตรวจสอบด้วยเครื่องจักรของหนึ่งในหลักฐานที่เทคนิคที่สุดในทฤษฎีจำนวนสมัยใหม่.

การเปรียบเทียบที่ใกล้เคียงที่สุดคือเมื่อต้นปีนี้, Math, Inc. ใช้เอเจนต์ Gauss ของตนเพื่อทำหลักฐานอย่างเป็นทางการของผลลัพธ์การบรรจุทรงกลมของ Maryna Viazovska ที่ได้รับเหรียญฟิลด์ส์เมดัลในมิติ 8 และ 24. สิดฮาร์ธ ฮารีฮารัน (Sidharth Hariharan), นักศึกษาปริญญาเอก Carnegie Mellon ที่เป็นหัวหน้าการทำพิมพ์เขียวมนุษย์ในโครงการนั้นและปัจจุบันเป็นนักฝึกงานที่ Axiom Math และเป็นผู้ร่วมทำคณิตศาสตร์ที่ระบุในโครงการ 246, อธิบายว่าผลลัพธ์ใหม่เป็นความสำเร็จที่ครอบคลุมมากกว่า. เหตุผลของเขา, ตามที่เขาอธิบาย, คือ Axiom ถูกสร้างเพื่อการนำกลับมาใช้ใหม่: แทนที่จะเป็นการทำรูปแบบครั้งเดียวของหลักฐานเดียว, PrimeGapsLib เป็นห้องสมุดที่ได้รับการดูแลซึ่งรวมผลลัพธ์ช่องว่างจำนวนเฉพาะเพื่อสนับสนุนงานทำรูปแบบและการวิจัยในอนาคต.

ความแตกต่างนี้สำคัญต่อวิธีการอ่านผลลัพธ์. การตรวจสอบครั้งเดียวแสดงให้เห็นว่าระบบสามารถรับมือกับหลักฐานที่ยากได้. ห้องสมุดแสดงถึงสิ่งที่ใกล้เคียงกับโครงสร้างพื้นฐาน — เครื่องมือทำรูปแบบที่นำกลับมาใช้ใหม่ซึ่งผลลัพธ์อื่นสามารถสร้างบนมันได้ — ซึ่งเป็นทิศทางที่ ระบบการพิสูจน์อย่างเป็นทางการกำลังเคลื่อนที่ ขณะที่พวกมันเปลี่ยนจากการแก้โจทย์เป็นการตรวจสอบคณิตศาสตร์จริง. การอ้างสิทธิ์ความสามารถที่นี่ตั้งอยู่บนศิลปวัตถุที่เป็นสาธารณะและสามารถเรียกใช้ซ้ำได้ ไม่ใช่คะแนนมาตรฐาน: พิมพ์เขียว, โค้ด Lean, และความท้าทายเปรียบเทียบที่ออกแบบให้ผู้วิจัยภายนอกสามารถตรวจสอบหลักฐานด้วยตนเอง.

Ono มองคณิตศาสตร์เป็นสนามทดสอบสำหรับความทะเยอทะยานที่ใหญ่ขึ้น. หากคุณสมบัติของซอฟต์แวร์ — ไม่ว่าจะเป็นโปรแกรมที่หยุดทำงานหรือผลลัพธ์ที่ถูกต้องสำหรับทุกอินพุต — สามารถแสดงเป็นข้อความคณิตศาสตร์ที่แม่นยำ, ระบบที่พัฒนาจาก AxiomProver จะสามารถพิสูจน์อย่างเป็นทางการได้, เขาอ้าง, ชี้ไปสู่การตรวจสอบโค้ดที่สร้างโดย AI ที่เริ่มทำงานในระบบโครงสร้างพื้นฐาน, การเงิน, และระบบความปลอดภัย.

“โลกกำลังจะทำงานบนโค้ดคอมพิวเตอร์ที่ไม่มีใครได้อ่าน” โอโนะกล่าว. “AI มาถึงแล้วและเราไม่สามารถมองข้ามได้ — การทำรูปแบบหลักฐานเป็นสนามทดสอบสำหรับการแก้ปัญหาที่ผมคิดว่าเป็นความท้าทายสำคัญที่สุดที่เราจะเผชิญจาก AI.”

ในขณะนี้ ผลลัพธ์ที่ส่งมอบมีขอบเขตแคบและสามารถตรวจสอบได้: พิมพ์เขียวที่มีผู้ร่วมเขียน 41 คน, ห้องสมุด Lean สาธารณะ, และหลักฐานที่ตรวจสอบด้วยเครื่องจักรที่ยืนยันว่าจำนวนเฉพาะที่อยู่ภายในระยะ 246 จากกันจะไม่มีที่สิ้นสุด — เพื่อนบ้านที่ตรวจสอบได้ใกล้ที่สุดของสมมติฐานจำนวนเฉพาะคู่, และเป็นผลงานคณิตศาสตร์การวิจัยที่ลึกที่สุดที่ระบบ AI ตรวจสอบจนจบทั้งหมดจนถึงตอนสุดท้าย.