OpenAI ปล่อยงานพิสูจน์คณิตศาสตร์ 10 ข้อพร้อม Lean certificate — ปลดล็อกปัญหาเปิดที่ค้างมาหลายสิบปี รวมถึง non-sofic group

เช้าวันที่ 1 สิงหาคม 2026 OpenAI เปิดรีโป openai/ten-proofs บน GitHub พร้อมเปเปอร์ชื่อ Ten Advances in Mathematics and Theoretical Computer Science ความยาว 249 หน้า เนื้อหาคือผลลัพธ์ทางคณิตศาสตร์และวิทยาการคอมพิวเตอร์เชิงทฤษฎี 10 ข้อ ที่ตามคำในบทคัดย่อคือ “obtained by an internal OpenAI model” — ได้มาจากโมเดลภายในของ OpenAI

สิ่งที่ทำให้ข่าวนี้ต่างจากข่าว “AI แก้โจทย์คณิตศาสตร์” ที่ผ่าน ๆ มา ไม่ใช่จำนวนข้อ แต่คือ สิ่งที่แนบมาด้วย: ทุกผลลัพธ์มีไฟล์ formal proof เขียนใน Lean 4 ที่ใครก็ได้ดาวน์โหลดมา compile ตรวจเองได้ ไม่ต้องเชื่อคำโฆษณาของแล็บ นี่คือความแตกต่างระหว่าง “โมเดลอ้างว่าพิสูจน์ได้” กับ “มีใบรับรองที่เครื่องตรวจแล้วว่าถูก”

สิบข้อนั้นคืออะไร

รีโปแยกเป็นไฟล์ .lean หนึ่งไฟล์ต่อหนึ่งผลลัพธ์ ตรงกับสิบบทในเปเปอร์:

#	ผลลัพธ์	ไฟล์
1	Sphere packing มิติสูง — หาอัตราการลดลงเชิงเลขชี้กำลังที่แน่นอนของ Cohn–Elkies linear program ได้	SpherePacking.lean
2	Binary และ spherical codes — ปรับขอบเขตบนคลาสสิกให้ดีขึ้นด้วยแฟกเตอร์เชิงเลขชี้กำลังทุกพารามิเตอร์	MetricCodes.lean
3	Non-sofic group — สร้างกลุ่มที่ไม่ sofic ออกมาได้จริง	NonSoficGroup.lean
4	Connes’s rigidity conjecture — สร้างตัวอย่างค้าน	ConnesRigidity.lean
5	Arithmetic circuit complexity — ขอบเขตล่างใหม่ของ permanent: วงจรไร้การหารต้องใช้ Ω(n²·log log n) เกต, formula ต้องใช้ Ω(n⁴/log n) leaves	Permanent.lean
6	Quantum parallel repetition — พิสูจน์ exponential parallel repetition สำหรับเกม entangled สองผู้เล่นแบบจำกัดทุกเกม	QuantumParallelRepetition.lean
7	Closest vector problem — reduction ตรงจาก 3SAT ให้ hardness ระดับแฟกเตอร์ n^(1/400)	GapCVP.lean
8	Ehrhart’s volume conjecture — พิสูจน์ขอบเขตคม (n+1)ⁿ/n! ในทุกมิติ	EhrhartVolumeInequality.lean
9	Multicolor Ramsey numbers — ขอบเขตล่างเหนือเลขชี้กำลัง พิสูจน์ R_k(3) = k^Θ(k) แก้ปัญหา Erdős ข้อ 183	MulticolorTriangleRamsey.lean
10	Compactness และ degeneracy — ล้มสองข้อความคาดการณ์ใน extremal graph theory แก้ปัญหา Erdős ข้อ 146 และ 180	CompactnessAndDegeneracy.lean

ข้อ 3 คือข้อที่วงคณิตศาสตร์พูดถึงมากที่สุด คำถามคือ “ทุกกลุ่มนับได้สามารถประมาณด้วย permutation แบบจำกัดได้หรือไม่” — เป็นคำถามที่ Mikhail Gromov และ Benjamin Weiss ตั้งไว้เมื่อปี 1999 และเปิดค้างมา 27 ปี เปเปอร์ระบุว่าอาร์กิวเมนต์ใช้ property-(T) expanders ร่วมกับ binary Leavitt algebra

ข้อ 4 ก็หนักไม่แพ้กัน: สร้างกลุ่ม property-(T) ที่ไม่ isomorphic กันเป็นจำนวนอนันต์ แต่มี group von Neumann algebra เดียวกัน — ซึ่งล้มข้อความคาดการณ์ของ Alain Connes โดยตรง

ทำไม Lean certificate ถึงสำคัญกว่าตัวผลลัพธ์

สำหรับนักพัฒนา ส่วนที่น่าสนใจที่สุดของรีโปนี้ไม่ใช่คณิตศาสตร์ แต่คือ วิธีที่ OpenAI เลือกจะพิสูจน์ว่าตัวเองไม่ได้โม้

รีโปใช้ Lean 4.32.0 + mathlib + Lake สั่ง build ได้ตรง ๆ:

lake exe cache get
lake build All

ไฟล์ formalization.yaml ระบุสิ่งที่ตรวจสอบได้ทันทีสองอย่าง อย่างแรกคือ รายการ axiom ที่พิสูจน์ทั้งหมดพึ่งพา มีแค่สามตัวคือ propext, Classical.choice, Quot.sound — ทั้งสามคือ axiom มาตรฐานของ Lean เอง แปลว่าไม่มี sorry ค้าง ไม่มีการแอบยัด axiom พิเศษเพื่อให้พิสูจน์ผ่าน ใครที่เคยตรวจ formalization จะรู้ว่านี่คือจุดที่งานปลอมมักโป๊ะ

อย่างที่สองคือรีโปยังมีโฟลเดอร์ ComparatorChallenges/ พร้อมไฟล์ config 12 ชุด สำหรับ ตรวจซ้ำด้วย Comparator ซึ่งเป็น proof checker อิสระที่ไม่ใช่ Lean เอง (ใช้ร่วมกับ landrun, lean4export, nanoda_bin) — พูดง่าย ๆ คือไม่ต้องเชื่อแม้แต่ Lean kernel ตัวเดียว ตรวจข้ามเครื่องมือได้อีกชั้น

รีโปเป็น Apache-2.0 และมีลิงก์ไปเปเปอร์หลัก (ten-proofs-oai.pdf) กับ reasoning walkthroughs (reasoning-walkthroughs.pdf) ซึ่งเป็นบันทึกเส้นทางการคิดที่นำไปสู่แต่ละผลลัพธ์

สิ่งที่ยัง “ยังไม่” — อ่านตรงนี้ก่อนตื่นเต้น

มีสามจุดที่ควรระบุให้ตรง เพราะข่าวรอบนี้ถูกเล่าเกินจริงไปหลายที่แล้ว

หนึ่ง — เปเปอร์ไม่ได้เอ่ยชื่อโมเดล บทคัดย่อเขียนแค่ “an internal OpenAI model” คำว่า Astra ที่สื่อหลายเจ้าใช้พาดหัว (รวมถึง The Decoder) มาจากคำพูดของพนักงาน OpenAI บนโซเชียลและการรายงานของสื่อ ไม่ได้มาจากตัวเปเปอร์หรือรีโป ตัวเลขค่าใช้จ่าย “ราว 2,000 ดอลลาร์ที่เรต API” ที่สื่ออ้างก็ไม่ปรากฏในเปเปอร์ 249 หน้าฉบับนี้เช่นกัน — เราตรวจแล้วไม่พบ

สอง — โมเดลนี้ยังไม่มีให้ใช้ ไม่ว่าจะชื่ออะไรก็ตาม มันคือเวอร์ชันภายใน ไม่ใช่สิ่งที่เรียกผ่าน API ได้วันนี้

สาม — สถานะการรีวิวคือ agent-reviewed ฟิลด์ review.status ใน formalization.yaml เขียนไว้ตรง ๆ ว่า agent-reviewed ไม่ใช่ human-reviewed และไม่ใช่ peer-reviewed แน่นอนว่า Lean kernel ตรวจความถูกต้องของการพิสูจน์ให้แล้ว แต่สิ่งที่ Lean ไม่ได้ ตรวจให้คือ “ข้อความที่ formalize ไว้ตรงกับข้อความคาดการณ์ต้นฉบับที่นักคณิตศาสตร์เข้าใจกันจริงหรือเปล่า” — จุดนี้ยังต้องรอสายตามนุษย์ในวงการแต่ละสาขา และนั่นคืองานหลายเดือน ไม่ใช่หลายวัน

มุมมอง AI Curator

ผมคิดว่าความสำคัญจริงของงานชิ้นนี้อยู่ที่ รูปแบบการเผยแพร่ ไม่ใช่ผลลัพธ์

ตลอดสองปีที่ผ่านมา ข่าว “AI แก้โจทย์คณิตศาสตร์ได้” มีมาเรื่อย ๆ และเกือบทุกครั้งจบลงที่การเถียงกันว่าโจทย์ปนอยู่ใน training data หรือเปล่า ผลลัพธ์ถูกเชอร์รีพิกมาจากการรันกี่รอบ และใครเป็นคนเขียนพิสูจน์กันแน่ระหว่างโมเดลกับนักวิจัยที่นั่งข้าง ๆ การแนบ Lean certificate ที่พึ่งพาแค่ axiom มาตรฐานสามตัว ตัดข้อโต้แย้งกลุ่มหลังทิ้งไปเกือบหมดในครั้งเดียว — เพราะถ้าพิสูจน์ผิด lake build จะพัง ไม่มีทางเถียงเป็นอย่างอื่น

นี่คือสิ่งที่ผมอยากเห็นทุกแล็บทำ และเป็นบรรทัดฐานที่ควรลามออกจากคณิตศาสตร์ ถ้าโมเดลอ้างว่าเขียนโค้ดที่ปลอดภัยขึ้น ให้แนบ proof obligation ที่ verifier ตรวจได้ ถ้าอ้างว่าแก้บั๊กได้ ให้แนบ test ที่ fail ก่อนและ pass หลัง หลักการเดียวกัน: ย้ายภาระการพิสูจน์จาก “เชื่อผมสิ” ไปเป็น “รันดูเอง”

แต่ก็ต้องพูดอีกด้านให้ครบ — วิธีนี้ใช้ได้เพราะคณิตศาสตร์เป็นโดเมนที่มี ground truth ตรวจด้วยเครื่องได้ ปัญหาที่ธุรกิจส่วนใหญ่จ้าง AI ไปทำนั้นไม่มีคุณสมบัตินี้ การที่โมเดลปิดสร้าง non-sofic group ได้ ไม่ได้แปลว่ามันจะเขียน migration ให้ระบบ core banking ได้ถูกโดยอัตโนมัติ อย่าลากเส้นข้ามโดเมนเร็วเกินไป

สำหรับคนไทย มุมที่ผมคิดว่ามีค่าที่สุดในระยะสั้นคือ Lean และ mathlib กำลังกลายเป็นทักษะที่มีราคา ไม่ใช่ในฐานะเครื่องมือของนักคณิตศาสตร์บริสุทธิ์ แต่ในฐานะ ชั้นตรวจสอบผลงาน AI งานที่เกิดขึ้นแน่ ๆ หลังจากนี้คือคนที่อ่าน formalization ออกแล้วบอกได้ว่า “ข้อความที่เขียนใน Lean ตรงกับที่ตั้งใจจะพิสูจน์จริงไหม” — ซึ่งเป็นงานที่โมเดลยังทำแทนไม่ได้ตามที่ agent-reviewed บอกไว้เอง มหาวิทยาลัยไทยที่มีภาควิชาคณิตศาสตร์และวิทยาการคอมพิวเตอร์เข้มแข็ง มีช่องให้เข้าไปยืนตรงนี้ก่อนคนอื่นในภูมิภาค และต้นทุนเริ่มต้นคือแค่ elan กับเครื่องคอมพ์หนึ่งเครื่อง ไม่ใช่คลัสเตอร์ GPU

รีโปนี้ดาวน์โหลดได้เดี๋ยวนี้ ใครสงสัยว่าจริงไหม lake build All ตอบให้ได้เอง — ซึ่งก็คือประเด็นทั้งหมดของมัน

แหล่งข่าว

• openai/ten-proofs — Lean certificates accompanying proofs in mathematics and theoretical computer science (GitHub, Apache-2.0)
• Ten Advances in Mathematics and Theoretical Computer Science — เปเปอร์ฉบับเต็ม 249 หน้า (PDF)
• Reasoning walkthroughs (PDF)
• The Decoder — OpenAI announces its “next major model” Astra by dropping ten previously unsolved math solutions