OpenAI เปิดรีโป openai/math: ผลงานคณิตศาสตร์ 722 ฉบับจากโมเดลภายในที่ยังไม่เปิดตัว — อ้างพิสูจน์ quasi-Riemann hypothesis และ Unique Games Conjecture พร้อม Lean กว่า 25 ล้านบรรทัด แต่ยังไม่มีนักคณิตศาสตร์ภายนอกตรวจ และ AGMAI ย้ำว่า "ไม่รับรอง"

เมื่อ 21 ก.ย. OpenAI บอกว่าโมเดลภายในของตัวเอง แก้โจทย์ที่ค้างมานานได้ “มากกว่า 100 ข้อ” แต่ตอนนั้นยังไม่บอกว่าข้อไหน วันที่ 6 ต.ค. 2026 OpenAI เผยผลทั้งหมดผ่านโพสต์ “Sharing AI progress in mathematics” และรีโป GitHub openai/math (Apache-2.0, commit แรกเวลา 21:58 UTC หรือราวตีห้าของวันที่ 7 ต.ค. ตามเวลาไทย) ในรีโปมีต้นฉบับ 722 ฉบับ แบ่งเป็น 372 กลุ่มผลลัพธ์ (family) ครอบคลุมราว 17 สาขา ตั้งแต่ทฤษฎีจำนวนไปจนถึงสมการเชิงอนุพันธ์ย่อย แต่ละกลุ่มมีผลหลักหนึ่งชิ้นพร้อมบทพิสูจน์ทางเลือกหรือผลที่ตามมา

ตัวเลขนี้มากกว่าที่ประกาศไว้หลายเท่า และชื่อโจทย์ในรายการหลายข้อเป็นโจทย์ที่นักคณิตศาสตร์ทั้งสาขาไล่ตามกันมาหลายสิบปี แต่ต้องอ่านให้ครบสองด้าน ด้านแรก บางผลมาพร้อม บทพิสูจน์ใน Lean ที่ใครก็ดาวน์โหลดไปให้คอมพิวเตอร์ตรวจได้ ด้านที่สอง ยังไม่มีนักคณิตศาสตร์ภายนอกคนใดยืนยันผลเหล่านี้อย่างเป็นทางการ และไฟล์ catalogue ของรีโปเองยังเขียนสถานะ review ว่า unchecked

ในรีโปมีอะไร และสร้างขึ้นมาอย่างไร

README อธิบายว่าผลส่วนใหญ่มาจากขั้นตอนเดียวกัน คือป้อนโจทย์เปิด ราว 4,000 ข้อ ให้โมเดลภายในที่ยังไม่เปิดตัว ใช้ compute เฉลี่ย “สามชั่วโมงของ ChatGPT Pro thinking” ต่อหนึ่งผลลัพธ์ จากนั้นรวบรวมผลที่ผ่านเกณฑ์ความสำคัญจนได้ 372 กลุ่ม บางผลก็ต่อยอดจากผลก่อนหน้าที่โมเดลทำไว้เอง ส่วนข้อยกเว้นที่ README ระบุตรง ๆ มีสองเรื่อง คือ บริเวณที่ไม่มีศูนย์ของฟังก์ชันซีตา และ Hodge conjecture สำหรับ CM abelian varieties ซึ่งไม่ได้ผ่านขั้นตอนมาตรฐานนี้ และ write-up ของบทพิสูจน์ 11/12 นั้น “human edited for readability”

นอกจากต้นฉบับ PDF และ LaTeX ในรีโปยังมี:

• overview.pdf สรุปทั้ง 372 กลุ่ม 41 หน้า และ CONTENTS.md ที่ใช้เป็นแผนที่ไปยังแต่ละฉบับ
• reasoning_traces/ สรุปแบบย่อของการให้เหตุผลของโมเดลใน 10 ผลลัพธ์ เช่น irrationality exponent ของ π, Mahler conjecture และ isomorphism ของ free group factors
• lean/ ไลบรารี Lean 4 (toolchain v4.34.1 บน Mathlib) ที่ catalogue formalization.yaml ระบุว่าทำ formalization ของผลหลักไว้ 162 ฉบับ และ CONTENTS.md ลิงก์หน้า Lean ไว้ 235 จาก 372 กลุ่ม ช่อง automation ระบุว่าทำโดย agent และสถานะรวมคือ “Partial progress”

OpenAI บอกว่าบางผลที่ยังไม่มี Lean “could have issues” และจะแก้ไขเป็นเวอร์ชันใหม่โดยเก็บเวอร์ชันเก่าไว้ทั้งหมด

ผลที่เด่นที่สุด และอะไรตรวจได้จริงแล้ว

Quasi-Riemann hypothesis (family 003) คือหัวข้อที่ถูกพูดถึงมากที่สุด ข้ออ้างคือ Dirichlet L-function ทุกตัว รวมทั้งฟังก์ชันซีตาของ Riemann ไม่มีศูนย์ในครึ่งระนาบ Re s > 7/8 นี่ยังไม่ใช่ Riemann hypothesis ตัวจริงที่ต้องการเส้น 1/2 แต่เป็นคำถามที่ค้างกันมานานว่ามีแถบความกว้างคงที่ใดที่ไม่มีศูนย์หรือไม่ (ผลที่ดีที่สุดเดิมได้แค่บริเวณที่บางลงเรื่อย ๆ เมื่อเข้าใกล้ Re s = 1) ในกลุ่มเดียวกันยังมีบทพิสูจน์อีกแบบที่ได้ 11/12 และผลที่ตัด Landau–Siegel zeros แบบ uniform

สิ่งที่ทำให้ข้ออ้างนี้ต่างจาก PDF ทั่วไปคือ statement ใน Lean สั้นและอ่านเองได้ เพราะใช้ riemannZeta ตัวมาตรฐานของ Mathlib:

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0

วิธีตรวจคือใช้เครื่องมือ comparator ของ Lean FRO รันเทียบไฟล์ challenge กับบทพิสูจน์ใน OAI.NumberTheory.DirichletL.Nonvanishing โดยอนุญาตแค่ axiom มาตรฐานสามตัว (propext, Quot.sound, Classical.choice) หน้า lean/docs/003.md บอกขอบเขตไว้ชัดเจนเช่นกันว่า formalization ไม่ครอบคลุม “later applications” ในเปเปอร์ และค่าคงที่ของผล Siegel zero ไม่ได้ระบุเป็นตัวเลข

ผลอื่นที่มีหน้า Lean กำกับด้วย ได้แก่ Unique Games Conjecture ของ Khot (family 102, reduction จาก 3SAT พร้อม hardness ของ Max-Cut เกิน Goemans–Williamson และ Vertex Cover ต่ำกว่า 2), isomorphism ของ free group factors (287), ตัวอย่างค้านของ Kaplansky’s zero-divisor conjecture (196), irrationality ของค่าคงที่ Catalan (005) และ irrationality exponent ของ π เท่ากับ 2 (017) ส่วนผลใหญ่ที่ ยังไม่มี Lean เช่น Hilbert’s tenth problem บน ℚ (004), สูตร BSD แบบเต็มจาก Selmer corank ต่ำ (002) และ Hodge conjecture สำหรับ K3 ทุกตัว (032) ยังเป็นแค่ PDF ที่ต้องรอคนอ่าน

เราโคลนรีโป (ขนาด 3.1GB) มาสแกนดูเอง พบว่า lean/OAI มี 121,734 ไฟล์ รวมราว 25.9 ล้านบรรทัด และไม่พบ sorry หรือการประกาศ axiom เลย คำที่ grep เจอทั้งหมดอยู่ในคอมเมนต์ แต่ต้องย้ำว่าการสแกนข้อความ ไม่เท่ากับการคอมไพล์ README เองยังเตือนว่าไลบรารีใหญ่จนควร build ทีละส่วน และอาจต้องปรับ vm.max_map_count ของ Linux จนถึงเวลาที่เขียน เรายังไม่พบรายงานจากคนนอกที่รัน comparator ผ่านครบ

ปฏิกิริยาของวงการคณิตศาสตร์

วันเดียวกัน กลุ่ม AGMAI (Advisory Group on Mathematics and AI ที่ IAS ซึ่งมี Gowers, Hairer, Witten และคนอื่น ๆ) ออก แถลงการณ์ ว่าการปล่อยครั้งนี้เป็น “an important event for mathematics” แต่ “AGMAI’s advisory role should not be interpreted as a judgment of the impact of these results or an endorsement of the process” และบอกว่าการเปิดเผยเป็นแค่ “the beginning, not the completion” ของการที่มนุษย์จะเข้าใจผลเหล่านี้ ก่อนหน้านั้นในแนวปฏิบัติวันที่ 29 ก.ย. ซึ่งอิงจากแบบสำรวจนักคณิตศาสตร์กว่า 600 คน กลุ่มนี้เขียนไว้ตรง ๆ ว่า “we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models” และขอให้แล็บที่ปล่อยผลซึ่งยังไม่มีใครเข้าใจต้องสนับสนุนเงินทุนให้ชุมชนศึกษาผลนั้น โดยไม่เข้ามากำกับทิศทางเอง

Thomas Bloom ผู้ดูแล erdosproblems.com ก็ ประกาศปรับกติกาของเว็บ ในวันเดียวกัน เขาบอกว่าคลื่น “AI-produced solutions provided with no explanation” กำลังทำให้คนที่สนใจตัวคณิตศาสตร์จริง ๆ ท้อและถอยออกไป

มุมมอง AI Curator

ถ้าเอาเฉพาะตัวเลข นี่คือเหตุการณ์ใหญ่ที่สุดของ AI กับคณิตศาสตร์ในปีนี้ เพราะเป็นครั้งแรกที่บริษัท AI ปล่อยผลระดับเปลี่ยนสาขาออกมาเป็นกองพร้อมกันหลายร้อยชิ้น แทนที่จะปล่อยทีละชิ้นอย่างกรณี Navier–Stokes แต่สิ่งที่น่าสนใจกว่าตัวเลขคือ รูปแบบการพิสูจน์ความจริง ที่เปลี่ยนไป เมื่อมีผลออกมา 722 ฉบับในวันเดียว ไม่มีทางที่ peer review แบบเดิมจะตามทัน สิ่งที่ตามทันได้คือ Lean และ comparator ถ้าภายในไม่กี่สัปดาห์มีกลุ่มอิสระรันตรวจ QuasiRiemannHypothesis.json ผ่าน นั่นจะเป็นหลักฐานที่หนักแน่นกว่าคำประกาศใด ๆ ของ OpenAI ส่วนผลที่ยังเป็นแค่ PDF ก็ควรถูกมองเป็น “ข้ออ้าง” ไปจนกว่าจะมีคนตรวจ ไม่ว่าชื่อโจทย์จะดังแค่ไหน

สำหรับนักพัฒนา บทเรียนที่จับต้องได้คือ formal verification กำลังกลายเป็นวิธีเดียวที่ขยายตามปริมาณงานที่ AI สร้างได้ สิ่งที่เกิดกับคณิตศาสตร์วันนี้จะเกิดกับโค้ดต่อไป เมื่อเอเจนต์เขียนโค้ดเร็วกว่าที่คนรีวิวไหว การมี spec ที่เครื่องตรวจได้ (type, property test, contract หรือแม้แต่ Lean ในงานที่ต้องการความถูกต้องสูง) จะมีค่ามากกว่าการให้คนนั่งอ่าน diff ส่วนวงวิชาการไทย ซึ่งกลุ่มคนที่ใช้ Lean กับ Mathlib ยังเล็กมาก นี่คือจังหวะดีที่มหาวิทยาลัยจะเริ่มสอน proof assistant อย่างจริงจัง เพราะต่อจากนี้ทักษะ “อ่านและตรวจบทพิสูจน์ที่เครื่องเขียน” จะสำคัญไม่แพ้ทักษะเขียนบทพิสูจน์เอง

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

แหล่งข่าว

• openai/math — GitHub (README, CONTENTS.md, overview.pdf)
• Lean scope ของ family 003: The quasi-Riemann hypothesis
• On OpenAI’s Release of Mathematical Results — AGMAI (6 ต.ค. 2026)
• Responsible Release of AI-Generated Mathematics — AGMAI (29 ก.ย. 2026)
• Changes — Thomas Bloom, Erdős Problems Forum (6 ต.ค. 2026)