AlphaProof Nexus ของ DeepMind ผ่าน peer review ลง Science — เอเจนต์พิสูจน์ด้วย Lean แก้ปัญหา Erdős ที่เปิดอยู่ได้ 9 จาก 353 ข้อ และแค่ 'Ralph loop' + compiler ก็ทำได้เท่ากัน

งานวิจัย “Advancing mathematics research with AI-driven formal proof search” ของ Google DeepMind (ผู้เขียน 21 คน มี Pushmeet Kohli และ Swarat Chaudhuri เป็นผู้ติดต่อหลัก) ลงตีพิมพ์ในวารสาร Science เมื่อ 8 ต.ค. 2026 (DOI 10.1126/science.aej2213) The Decoder นำมารายงานวันนี้ ระบบในงานนี้ชื่อ AlphaProof Nexus เป็นเฟรมเวิร์กให้เอเจนต์ใช้ LLM เขียนบทพิสูจน์ในภาษา Lean โดยมี compiler คอยตรวจทุกขั้นตอน ผลงานเด่นคือแก้ ปัญหา Erdős ที่ยังเปิดอยู่ได้ 9 จาก 353 ข้อ ในจำนวนนี้มี 2 ข้อที่เปิดค้างมา 56 ปีตั้งแต่ปี 1970 และพิสูจน์ ข้อคาดการณ์ (conjecture) จากฐานข้อมูล OEIS ได้ 44 จาก 492 ข้อ

ตัวผลงานไม่ใช่ข่าวใหม่ DeepMind เผยแพร่ preprint บน arXiv (2605.22763) และเปิด repo บทพิสูจน์ตั้งแต่เดือน พ.ค. ซึ่งตอนนั้นบล็อกเราไม่ได้รายงาน สิ่งที่ใหม่สัปดาห์นี้คืองานผ่าน peer review ในวารสารวิทยาศาสตร์ระดับบนสุด จังหวะนี้น่าสนใจ เพราะในสัปดาห์เดียวกัน OpenAI ต้องถอนบทความคณิตศาสตร์บางส่วนในชุด 722 manuscript ที่เขียนเป็นภาษาธรรมชาติ

ทำงานอย่างไร

จาก preprint เวอร์ชันล่าสุด (v2, 8 มิ.ย.) ผู้ใช้ป้อนไฟล์ Lean ที่มีทฤษฎีบทเป้าหมาย โดยใส่ sorry แทนตำแหน่งบทพิสูจน์ และใช้ marker EVOLVE-BLOCK / EVOLVE-VALUE ระบุว่าเอเจนต์แก้ไขโค้ดส่วนไหนได้ ระบบจะทำงานจนได้บทพิสูจน์ที่ไม่มี sorry เหลืออยู่

• เอเจนต์พื้นฐาน (A): ประกอบด้วย subagent หลายตัวที่ทำงานแยกกันโดยไม่แชร์สถานะ แต่ละตัวเป็น “Ralph loop” ซึ่ง Gemini 3.1 Pro คิดแบบ chain-of-thought แล้วแก้ sketch ด้วยเครื่องมือ search-and-replace หลังจบแต่ละรอบ ระบบจะ compile ด้วย Lean ถ้าไม่ผ่าน ข้อความ error จะกลายเป็นข้อมูลนำทางในรอบถัดไป
• เอเจนต์เต็มรูปแบบ: ประสานงาน subagent ด้วย evolutionary algorithm ให้ Gemini 3.0 Flash เป็นผู้จัดอันดับ sketch และเรียก AlphaProof (ระบบ RL ที่ได้เหรียญเงิน IMO 2024) มาช่วยพิสูจน์ lemma ย่อย ค่าใช้จ่ายของ AlphaProof อยู่ที่ราว 27.5 TPU-ชั่วโมง (ประมาณ 60 ดอลลาร์) ต่อปัญหาบน TPU v6e

ทีมรายงานว่าค่า inference ของเอเจนต์ตัวที่เก่งที่สุดอยู่ที่ “ไม่กี่ร้อยดอลลาร์ต่อปัญหา” แต่ยอมรับว่าตัวเลขนี้ไม่รวมต้นทุนของการรันบนปัญหา Erdős ทั้ง 353 ข้อเพื่อหาว่าข้อไหนพอแก้ได้ ซึ่ง “เป็นการลงทุนด้านการคำนวณที่สำคัญในตัวเอง”

ข้อค้นพบที่ทีมเองบอกว่า “น่าประหลาดใจ”

ในการวิเคราะห์ย้อนหลัง เอเจนต์พื้นฐาน (A) ก็แก้ปัญหา Erdős ได้ครบทั้ง 9 ข้อ เพียงแต่ใช้ต้นทุนสูงกว่าในข้อที่ยากที่สุด ทีมเขียนว่าตอนวางแผนโปรเจกต์ loop แบบง่ายยังทำได้ไม่ดีบน benchmark ระดับแข่งขัน จึงตัดสินใจลงทุนกับเอเจนต์เต็มรูปแบบ แต่ “ภูมิทัศน์ของ LLM เปลี่ยนไปมาก” ตั้งแต่นั้น ทีมให้เครดิตความสำเร็จของเอเจนต์พื้นฐานกับทั้งความก้าวหน้าของโมเดล และ “พลังของ feedback จาก compiler ที่ช่วยยึดการให้เหตุผลของ LLM ไว้กับความจริง” ทีมยังคาดว่าความได้เปรียบของระบบที่ซับซ้อนกว่า “อาจลดลง” เมื่อโมเดลเก่งขึ้น

ทีมเขียนข้อจำกัดไว้ชัดเจนเช่นกัน ความสำเร็จกระจุกอยู่ในสาขาที่ไลบรารี Mathlib ของ Lean ครอบคลุมดีแล้ว เช่น combinatorics, convex optimization และทฤษฎีจำนวน ซึ่งโจทย์มักแตกเป็นเป้าหมายย่อยได้ง่าย ทีมระบุว่า “ปัญหา Erdős ส่วนใหญ่ยังอยู่นอกเอื้อม” นอกจากนี้ผู้เชี่ยวชาญยังต้องตรวจทุกข้อว่าข้อความใน Lean ตรงกับโจทย์ต้นฉบับจริง ระหว่างทาง เอเจนต์ช่วยจับ misformalization ได้ด้วย เช่น ความกำกวมของคำว่า “density” ในโจทย์บางข้อ บทพิสูจน์ทั้งหมดเปิดให้ดูใน repo google-deepmind/alphaproof-nexus-results (Apache-2.0)

มุมมอง AI Curator

ประเด็นที่ควรจำจากงานนี้ไม่ใช่ตัวเลข 9 ข้อ แต่คือวิธีการตรวจสอบ สัปดาห์นี้มีตัวอย่างสองแบบให้เทียบกัน ฝั่ง OpenAI ผลิต manuscript ภาษาธรรมชาติจำนวนมาก แล้วต้องถอนและแก้ทีหลังเมื่อนักคณิตศาสตร์ตรวจเจอข้อผิดพลาด ฝั่ง DeepMind ให้ compiler เป็นคนตรวจทุกขั้น มนุษย์เหลือหน้าที่ตรวจแค่ว่า “โจทย์ถูกแปลงเป็น Lean ถูกต้องหรือไม่” แบบหลังช้ากว่าและทำได้ในขอบเขตแคบกว่า แต่ผลลัพธ์ที่ได้เชื่อถือได้จริง และเพิ่งผ่าน peer review มา

สำหรับนักพัฒนา ข้อค้นพบเรื่องเอเจนต์พื้นฐานมีค่ามาก มันยืนยันสิ่งที่วงการ coding agent เรียนรู้มาตลอดปีนี้ว่า loop ง่ายๆ ที่มีตัวตรวจคำตอบที่เข้มงวด มักชนะสถาปัตยกรรมที่ซับซ้อน เมื่อโมเดลเก่งพอ ตัวตรวจในงานนี้คือ Lean compiler ในงานของเราคือ test suite, type checker หรือ oracle แบบ byte-match ที่เราเห็นในงาน decompile เกมเมื่อวาน ถ้าจะสร้างเอเจนต์สำหรับโดเมนไหน คำถามแรกควรเป็น “เราตรวจผลลัพธ์อัตโนมัติได้แม่นแค่ไหน” ก่อนจะคิดเรื่อง multi-agent หรือ orchestration ซึ่งตรงกับผลการศึกษาของ Vals AI ที่เรารายงานเช้านี้ว่าทีมเอเจนต์เปลือง token มากแต่คุณภาพเพิ่มขึ้นน้อย

ในบริบทไทย งานสาย formal verification ยังมีคนทำน้อยมาก แต่ต้นทุนเข้าถึงลดลงเร็ว เพราะสิ่งที่ต้องมีคือ Lean, Mathlib และ API ของโมเดล frontier ไม่ใช่ TPU ระดับแล็บ อาจารย์และนักศึกษาคณิตศาสตร์ที่อยากลองควรเริ่มจาก repo formal-conjectures ของ DeepMind ที่รวบรวมโจทย์เปิดซึ่งแปลงเป็น Lean ไว้แล้ว การมีส่วนร่วมในขั้น “แปลงโจทย์ให้ถูกต้อง” ก็คือคอขวดเดียวกับที่งานนี้ยอมรับว่ายังต้องใช้มนุษย์

---

แหล่งข่าว

• The Decoder — Google Deepmind’s AlphaProof Nexus solved dozens of open math problems and actually got peer reviewed (12 ต.ค. 2026)
• Science — Advancing mathematics research with AI-driven formal proof search (DOI 10.1126/science.aej2213, 8 ต.ค. 2026)
• arXiv 2605.22763 — preprint ฉบับเต็ม
• GitHub — google-deepmind/alphaproof-nexus-results