OpenAI อ้างโมเดล Astra แก้ปัญหาคณิตศาสตร์ที่ค้างมานับสิบปีได้ 10 ข้อ พร้อมใบรับรอง Lean

OpenAI เผยแพร่รายงานเมื่อวันที่ 1 สิงหาคม 2026 ระบุว่าได้นำโมเดลรุ่นภายในของ Astra ซึ่งเป็นตระกูลโมเดลรุ่นถัดไปของบริษัท ไปแก้โจทย์คณิตศาสตร์และวิทยาการคอมพิวเตอร์เชิงทฤษฎีจำนวน 10 ข้อ ที่ "ไม่มีความคืบหน้าในผลลัพธ์หลักมาอย่างน้อยหนึ่งทศวรรษ"

โจทย์ที่อ้างว่าแก้ได้ครอบคลุมหลากหลายสาขา ตั้งแต่เรขาคณิตมิติสูง ทฤษฎีรหัส ความซับซ้อนของวงจรเลขคณิต ทฤษฎีกรุป พีชคณิตตัวดำเนินการ ความซับซ้อนเชิงควอนตัม การเข้ารหัสแบบแลตทิซ ไปจนถึงคอมบินาทอริกส์เชิงสุดขั้ว ตัวอย่างที่โดดเด่นได้แก่ การปรับปรุงขอบเขตบนเชิงเส้นกำกับของความหนาแน่นการอัดทรงกลมในมิติสูงจนแตะเกณฑ์ Cohn–Elkies การสร้างกรุปที่ไม่เป็น sofic และตัวอย่างค้านต่อข้อคาดการณ์เรื่องความแข็งของ Connes

จุดที่ทำให้เรื่องนี้ต่างจากการเคลมทั่วไปคือความสามารถในการตรวจสอบ แต่ละบทพิสูจน์มาพร้อม Lean 4 certificate ที่เผยแพร่ในรีโป openai/ten-proofs พร้อมบันทึก chain-of-thought และเอกสาร PDF ที่โมเดลเขียนอธิบายย้อนกลับว่าบทพิสูจน์ประกอบขึ้นมาอย่างไร OpenAI ระบุว่าค่าประมวลผลรวมสำหรับทั้งสิบข้ออยู่ที่ราว 2,000 ดอลลาร์ตามอัตราค่า token ของ GPT-5.6 Sol

Simon Willison ตั้งข้อสังเกตสำคัญว่า OpenAI ไม่ได้เปิดเผยว่ามีโจทย์อีกกี่ข้อที่ใช้งบประมาณระดับเดียวกันแล้ว "แก้ไม่ได้" ซึ่งเป็นตัวเลขที่จำเป็นต่อการประเมินอัตราความสำเร็จจริง เขายังอยากเห็น prompt ที่ใช้จริงด้วย ขณะที่ในวงการคณิตศาสตร์เองก็เริ่มมีเสียงสะท้อนเชิงปรัชญาถึงบทบาทของนักคณิตศาสตร์ในยุคที่ AI พิสูจน์ทฤษฎีบทได้ OpenAI ยังไม่ระบุกำหนดเปิดตัว Astra สู่สาธารณะ