🔴 OpenAI: โมเดลที่ยังไม่ปล่อยชื่อ Astra ผลิตผลลัพธ์ใหม่สิบข้อในโจทย์คณิตศาสตร์ที่ค้างมาอย่างน้อยสิบปี · แนบใบรับรอง Lean 4 ที่เครื่องตรวจได้ทุกข้อ (1 ส.ค. · HN 405+) ⚙
OpenAI เผยแพร่ "Ten advances in mathematics and theoretical computer science" โดยระบุว่า "The results were achieved by an internal version of Astra, our next major model." ซึ่งเป็นโมเดลที่ยังไม่ปล่อยและยังไม่มีใครนอกบริษัทได้ใช้
เกณฑ์ความยากที่ต้นฉบับใช้: "ten results to problems that have been open and have seen no progress on the main result for at least a decade, and in most cases much longer."
สิ่งที่ทำให้ข่าวนี้ต่างจากข่าว AI ทำคณิตศาสตร์ครั้งก่อนๆ ไม่ใช่ผลลัพธ์ แต่คือหลักฐาน: ทุกข้อมาพร้อม ใบรับรอง Lean 4 ที่เครื่องตรวจได้ บน GitHub ใต้ Apache-2.0 (ต้องใช้ Lean 4.32.0 + mathlib + Lake) พร้อมไดเรกทอรี ComparatorChallenges ให้คนนอกตรวจเอง · ใครมี Lean compiler ตรวจความถูกต้องเชิงตรรกะได้ทันทีโดยไม่ต้องเชื่อคำพูดของ OpenAI
ผลลัพธ์ที่ยกมาได้ เช่น ขอบเขตบนใหม่ของการจัดเรียงทรงกลมมิติสูงลงถึงระดับ Cohn-Elkies threshold · การสร้างที่แสดงว่ามีกลุ่มที่ไม่เป็น sofic อยู่จริง · ตัวอย่างค้านของ Connes's rigidity conjecture · ขอบเขตล่างแบบ superexponential ของ multicolor triangle Ramsey numbers ที่แก้ปัญหา Erdős ข้อ 183 · และตัวอย่างค้านที่แก้ปัญหา Erdős ข้อ 146 กับ 180
🔴 ตัวเลขที่ถูกอ่านผิดกันทั้งอินเทอร์เน็ตและเราเกือบผิดตาม: ต้นฉบับเขียนว่า "The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates" คือ ~$2,000 รวมทั้งสิบข้อ เฉลี่ยราว $200 ต่อข้อ · ไม่ใช่ $2,000 ต่อข้อ · Noam Brown ของ OpenAI ตอกย้ำเองในกระทู้ว่า "We didn't spend a lot on each problem."
🔴 จุดที่สื่อรายงานผิดคนละทางสองแบบ: ต้นฉบับเขียนว่า "These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate." แปลว่าโมเดลเป็นคนทำ Lean formalization เอง ส่วนคนช่วยตอนเรียบเรียงเป็นต้นฉบับบทความ · ห้ามพูดว่าคนเป็นคนแปลงเป็น Lean และห้ามพูดว่าคน "แค่จัดรูปแบบ"
⚠ สองคำที่ต้องแก้ก่อนใช้: "การสร้างกลุ่ม non-sofic ที่ชัดแจ้งเป็นครั้งแรก" เป็นคำของสื่อ ต้นฉบับเขียนแค่ "a construction establishing the existence of non-sofic groups" · และ "ปรับปรุงขอบเขต sphere packing ครั้งแรกตั้งแต่ 1978" ผิด ที่ถูกคือปรับปรุง exponent ครั้งแรกนับจาก Kabatiansky-Levenshtein 1978 เพราะ Cohn-Zhao (2014) เคยปรับปรุงในระดับค่าคงที่ไปแล้ว
เสียงค้านที่หนักที่สุดไม่ได้เถียงว่าคณิตศาสตร์ผิด แต่เถียงเรื่องสิ่งที่ไม่ได้บอก: ลองไปกี่โจทย์ก่อนได้สิบข้อนี้ · แต่ละข้อลองกี่รอบ · compute จริงเท่าไร · ความเห็นที่ได้คะแนนสูงสุดเขียนว่า "the $2000 number could be completely misleading, similar to P-value hacking by not disclosing the total experimental setup." · ⚠ แต่ต้องพูดอีกด้านคู่กัน: Noam Brown ยอมรับเองว่าทีมลองโจทย์ใหญ่อื่นแล้วไม่สำเร็จ ดังนั้น "ไม่เปิดเผยความล้มเหลวเลย" แรงเกินไป
⚠ สถานะ ณ วันนี้: ยังไม่ผ่าน peer review และยังไม่มีการตรวจสอบระดับชุมชน · แต่ก็ห้ามพูดว่าไม่มีคนนอกอ่านเลย เพราะเอกสารระบุชื่อผู้อ่านล่วงหน้าไว้ เช่น Sorin Popa (ส่วน Connes rigidity) และ Henry Bradford, Michael Chapman, Alon Dogon, Francesco Fournier-Facio (ส่วน non-sofic groups)
▲ ทำไมต้องรู้ · ข่าวนี้เปลี่ยนคำถามที่คนทำงานสาย AI ถามกันบ่อยที่สุด จาก "AI แทนงานคิดได้ไหม" เป็น "งานแบบไหนที่มันแทนได้" คำตอบที่ได้ตรงกับหลักการที่ว่า AI จะแข็งแรงเป็นพิเศษกับงานที่มีเครื่องมือตรวจอัตโนมัติว่าทำถูกหรือผิด เช่น Lean ที่เป็นกรรมการของคณิตศาสตร์เชิงรูปนัย ส่วนงานวิจัยเชิงประจักษ์ที่ไม่มีกรรมการแบบนั้น AI ยังทำได้ไม่ดีเท่า อีกบทเรียนหนึ่งที่นำไปใช้ได้จริงคือการอ่านตัวเลขที่บริษัทเทคโนโลยีประกาศ ข่าวนี้เปิดหลักฐานที่ใครก็ตรวจได้ฟรี (ไฟล์ Lean) แต่ไม่เปิดเผยว่าลองแก้โจทย์ไปกี่ครั้งกว่าจะได้สิบข้อนี้ ทำให้ประเมินความยากจริงไม่ได้ ข้อควรระวังคือใบรับรอง Lean พิสูจน์แค่ว่าไม่มีช่องโหว่เชิงตรรกะ แต่ไม่ได้พิสูจน์ว่าสิ่งที่ formalize ไว้ตรงกับโจทย์ที่วงการเข้าใจ ส่วนนั้นยังต้องให้ผู้เชี่ยวชาญอ่านอยู่ดี
OpenAI · openai/ten-proofs (GitHub) · Simon Willison · HN · ต้นฉบับ PDF · openai-astra-ten-proofs