GPT-6 Astra แก้ปัญหา Goldbach ฉบับ Liouville สำเร็จ และ Lean ตรวจสอบซ้ำอย่างอิสระผ่านแล้ว

动察 Beating ข่าวด่วน AI บัญชีชุมชนคณิตศาสตร์นิรนาม Captain Sude เปิดเผยหลักฐานใหม่ที่ GPT-6 Astra ค้นพบ ซึ่งแก้ปัญหาข้อสันนิษฐานโกลด์บัคเวอร์ชันลิอูวิลล์ได้สำเร็จ

ปัญหานี้ผ่อนปรน "จำนวนเฉพาะสองจำนวน" ในข้อสันนิษฐานโกลด์บัคแบบคลาสสิก ให้กลายเป็น "จำนวนเต็มสองจำนวนที่มีจำนวนตัวประกอบเฉพาะรวมกันเป็นจำนวนคี่" ก่อนหน้านี้ นักคณิตศาสตร์ Alexander P. Mangerel จากมหาวิทยาลัยเดอแรมพิสูจน์ได้เฉพาะเมื่อข้อสันนิษฐานรีมันน์แบบทั่วไปเป็นจริง และจำนวนคู่มีค่ามากพอเท่านั้น

ตอนนี้ Astra ได้ตัดข้อจำกัดทั้งสองออกไป พิสูจน์ว่าจำนวนคู่ทุกจำนวนที่มากกว่า 2 เป็นจริง แนวคิดหลักคือสมมติก่อนว่าจำนวนคู่จำนวนหนึ่งไม่สามารถแยกได้เช่นนี้ แล้วค่อยๆ อนุมานผลลัพธ์ที่ขัดแย้งกันเองออกมาทีละขั้น

หลักฐานฉบับสมบูรณ์ได้เขียนลงใน Lean 4 แล้ว โครงการสามารถคอมไพล์ได้ตามปกติ และที่เก็บการตรวจสอบอิสระก็ทำซ้ำได้สำเร็จ ไม่พบ `sorry` หรือสัจพจน์ทางคณิตศาสตร์เพิ่มเติมใดๆ

ข้อสันนิษฐานโกลด์บัคแบบคลาสสิกเองยังไม่ได้รับการแก้ไข เพราะจำนวนบวกสองจำนวนในที่นี้ยังสามารถเป็นจำนวนประกอบได้