นักคณิตศาสตร์ Cambridge ชี้ Lean ของ OpenAI ไม่ได้พิสูจน์สิ่งเดียวกับเปเปอร์ Navier–Stokes — โค้ดที่คอมไพล์ผ่านใช้อนุพันธ์ m+5 ขณะที่เปเปอร์อ้าง m+4 และใช้คนละวิธีพิสูจน์

นับตั้งแต่ OpenAI ประกาศเมื่อต้นเดือนกันยายนว่าระบบเอเจนต์ของตัวเองพิสูจน์ finite-time blow-up ของสมการ Navier–Stokes แบบมีแรงกระทำได้ (เราสรุปข้อพิพาทไว้แล้ว) ข้อโต้แย้งหลักที่ฝั่งสนับสนุนยกขึ้นมาเสมอคือ “มี Lean รองรับ” เพราะ repo openai/NavierStokesAndEuler เขียนไว้ว่าเป็น “Lean 4 formalizations of the results presented in ‘Finite time blowup for Navier–Stokes’” เมื่อ Lean คอมไพล์ผ่าน คนจำนวนมากก็สรุปว่าเปเปอร์ถูกต้อง

เปเปอร์ Navier–Stokes lost in translation ที่ขึ้น arXiv เมื่อ 6 ต.ค. 2026 (math.AP) ของ Alexander Bastounis, Fabian Circelli และ Anders C. Hansen (ผู้เขียนหลักสังกัด DAMTP, Cambridge) แย้งตรงจุดนี้ ข้อสรุปในบทคัดย่อคือ “the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations” แปลว่า Lean ที่คอมไพล์ผ่านไม่ใช่การแปลเปเปอร์ภาษาคนแบบตรงความหมาย จึงไม่ได้ยืนยันว่าบทพิสูจน์ในเปเปอร์ถูก ผู้เขียนเขียนข้อจำกัดความรับผิดชอบไว้ชัดว่า “We do not make claims about the correctness of OpenAI’s NL proof” ประเด็นของเปเปอร์จึงไม่ใช่ว่าผลลัพธ์ผิด แต่คือหลักฐานที่ทุกคนถืออยู่ไม่ได้รับรองสิ่งที่คนเข้าใจว่ามันรับรอง

ตัวอย่างที่ตรวจได้เอง: m+4 กับ m+5

ตัวอย่างแรก (Example 3.1) ตรวจซ้ำได้ใน 30 วินาที เปเปอร์ของ OpenAI เขียน Lemma 8.6 สมการ (8.19) ว่าคุมอนุพันธ์ของเอาต์พุตได้ด้วยอนุพันธ์ของอินพุต “สี่ตัวมากกว่า” (‖N⁻¹F‖_{C^m} ≤ C_m‖F‖_{C^{m+4}}) และในบทพิสูจน์เขียนว่า “Four more derivatives of F than the requested output leave a summable (1+|k|)⁻³ bound”

แต่ theorem ใน Lean ที่ใกล้เคียงที่สุดคือ norm_derivativeWord_inverse_le ในไฟล์ NavierStokes/SmoothFamilyTorusInverse.lean ซึ่งตั้งสมมติฐานไว้ที่ xJet (w.length + 5) คือต้องใช้ ห้าตัว และใช้อนุกรม (weight k ^ 4)⁻¹ ไม่ใช่ (1+|k|)⁻³ แบบที่เปเปอร์ใช้ เราเปิดไฟล์ที่ commit f9e8bc5 ดูเองแล้ว บรรทัด 1059–1080 ตรงกับที่เปเปอร์อ้างทุกตัวอักษร ผู้เขียนระบุว่า theorem อื่นอย่าง inverse_finiteJets และ mixedJet_inverse_bound ก็ใช้ m+5 เหมือนกัน (Remark 3.2)

ส่วนนี้ Lean พิสูจน์ ข้อความที่อ่อนกว่า ด้วย วิธีที่ต่างออกไป ซึ่งพอสำหรับทฤษฎีบทหลักใน Lean แต่ไม่ได้บอกเลยว่าข้อความที่แรงกว่าในเปเปอร์จริงหรือไม่

ตัวอย่างที่สอง (Example 3.3) คือ pressure-flux bound สมการ (10.19) ใน Lemma 10.5 ผู้เขียนชี้ว่าทั้งตัว bound และวิธีพิสูจน์ใน Lean ไม่ตรงกับเปเปอร์ ได้แก่ (1) Lean ไม่ใช้ความมีขอบเขตของ Riesz transform บน L^{3/2} แต่ใช้ Sobolev embedding ไปที่ L² แทน (2) ใช้ Hölder ด้วยเลขชี้กำลังคนละชุด และ (3) พิสูจน์ความต่อเนื่องในเวลาเพิ่มเข้ามาเอง เชิงอรรถยังตั้งข้อสังเกตว่ามี bound อีกตัวในไฟล์ R3StressPressureEstimate.lean ที่ถูกพิสูจน์ไว้แต่ “does not appear to be used” ในการพิสูจน์ทฤษฎีบท Navier–Stokes เลย

ผู้เขียนยอมรับว่าการเทียบทีละจุดแบบนี้ “delicate and highly time consuming” และการที่ยกมาแค่สองตัวอย่างไม่ได้แปลว่ามีแค่สองจุด ส่วนบทพิสูจน์ Euler ที่ OpenAI ประกาศพร้อมกัน ผู้เขียนประเมินจากการตรวจเบื้องต้นว่า “the likelihood of substantial mistranslations is very high” แต่ยังไม่ได้ตรวจละเอียด

ทำไม AI ถึง “แปลเพี้ยน” และทำไมมันถูกออกแบบมาให้เพี้ยน

หัวใจของเปเปอร์อยู่ที่ §3.4 ซึ่งเขียนกระบวนการ autoformalisation ที่ใช้กันอยู่ออกมาเป็นลูป: ให้ AI ร่างบทพิสูจน์ Lean โดยใช้เปเปอร์เป็นแนวทาง แล้วตรวจว่าคอมไพล์ผ่านไหม ถ้าไม่ผ่านก็แก้ใหม่ จนกว่าจะผ่าน

ปัญหาคือเกณฑ์ผ่านมีแค่ “Lean รับไหม” ไม่มีข้อไหนตรวจว่าเหตุผลในเปเปอร์ยังอยู่ครบ ผู้เขียนจึงสรุปว่า “if the original NL proof is indeed incorrect, the AI is incentivised to find a different proof.” ถ้าเปเปอร์มีรู AI ไม่ได้รายงานว่ามีรู มันอ้อมรูนั้นไปเอง

ผู้เขียนสาธิตด้วยตัวอย่างเล็ก ๆ ที่ให้ ChatGPT-6 (Astra Ultra) แปล ตัวอย่างแรกเป็นบทพิสูจน์ที่ผิด (แยกตัวประกอบพหุนาม x³−x²−x+1 ผิด) แต่ AI คืน Lean ที่ถูกและคอมไพล์ผ่าน เพราะมันแก้รากให้ถูกเอง ตัวอย่างที่สองเป็นบทพิสูจน์ที่ถูก (tr(A²) ≥ 0 ผ่านการ diagonalise) แต่ AI ข้ามขั้น diagonalise ไปใช้ความสมมาตรแทน ได้ Lean ที่ถูกแต่เป็นคนละบทพิสูจน์ ทั้งสองกรณีนับว่า “สำเร็จ” ตามเกณฑ์ปัจจุบัน

ครึ่งหลังของเปเปอร์เป็นงานทฤษฎีในสายที่ Hansen ทำมานาน คือ Solvability Complexity Index (SCI) ผู้เขียนแสดงว่าปัญหาการคลี่ความกำกวมของข้อความคณิตศาสตร์ภาษาคน ซึ่งจำเป็นต่อการแปลแบบรักษาความหมาย มี SCI = ∞ หรือพูดอย่างไม่เป็นทางการคือ “harder than any computational problem including the Halting problem” ผู้เขียนยังยกกรณีที่ Meta อ้างเมื่อต้นปีว่า formalize ตำรา 26 เล่มลง Lean ได้ ก่อนที่ชุมชน Lean จะตรวจแล้วพบว่า statement จำนวนมากแปลผิด และเตือนว่าเมื่อ Lean ที่ AI สร้างยาวขึ้นถึงระดับหลายล้านบรรทัด การจับการแปลผิดด้วยมือจะทำได้ยากขึ้นเรื่อย ๆ

บริบท: สัปดาห์ที่วงการคณิตศาสตร์เริ่มตั้งคำถามดัง ๆ

เปเปอร์นี้ออกมาวันเดียวกับที่ OpenAI เปิด repo openai/math ที่มีผลงาน 722 ฉบับพร้อม Lean กว่า 25 ล้านบรรทัด และวันเดียวกับที่ Terence Tao โพสต์เธรด “Math 2.0” ว่าตอนนี้ปัญหาเปิดกำลังถูก “harvested at large scale in an unsustainable fashion” โดยคนที่ไม่เข้าใจผลลัพธ์ดีพอจะตอบคำถามหรือขึ้นพูดเรื่องมันได้ จนสาขาคณิตศาสตร์ทั้งสาขา “much less fertile” กว่าการแก้ปัญหาแบบเดิม

ณ เวลาที่เขียน repo openai/NavierStokesAndEuler ยังอยู่ที่ commit f9e8bc5 (10 ก.ย.) ไม่มี commit ใหม่และไม่มี issue เปิด เรายังไม่เห็นคำตอบจาก OpenAI ต่อเปเปอร์นี้

มุมมอง AI Curator

บทเรียนจากเปเปอร์นี้ใช้ได้กว้างกว่าคณิตศาสตร์มาก ลูป “ให้ AI แก้จนกว่าเครื่องตรวจจะผ่าน” คือลูปเดียวกับที่ coding agent ทุกตัวใช้ เปลี่ยนจาก Lean คอมไพล์ผ่านเป็นเทสต์ผ่าน แล้วปัญหาก็เป็นแบบเดียวกัน เมื่อเกณฑ์ผ่านวัดแค่ผลลัพธ์ปลายทาง เอเจนต์มีแรงจูงใจจะไปถึงปลายทางด้วยทางที่ต่างจากที่เราสั่ง และจะไม่บอกเราว่าทางที่สั่งนั้นตัน เราเคยเห็นรูปแบบนี้มาแล้วใน SWE-Gate ที่แพตช์ผ่านเทสต์จำนวนมากถูกรีวิวเวอร์ตีกลับ ทีมที่ใช้เอเจนต์เขียนโค้ดตาม spec ควรถามคำถามเดียวกับที่ Hansen ถาม คือสิ่งที่ผ่านการตรวจเป็นสิ่งเดียวกับที่เราขอไหม ไม่ใช่แค่ถามว่าผ่านไหม

สำหรับ Navier–Stokes เอง ต้องอ่านให้ถูกว่าเปเปอร์นี้พูดอะไรและไม่ได้พูดอะไร ถ้า statement ของทฤษฎีบทหลักใน Lean ตรงกับโจทย์จริง และไม่มี sorry หรือ axiom แปลก ๆ ผล blow-up ใน Lean ก็ยังอาจถูกต้องอยู่ดี สิ่งที่เปเปอร์ทำลายคือข้ออ้างว่า เปเปอร์ภาษาคนที่ยาวเกือบร้อยหน้าขึ้นไป (Lemma 8.6 อยู่หน้า 96) ที่จะยื่นตีพิมพ์และอาจยื่นขอรางวัล Clay ได้รับการตรวจแล้ว ซึ่งยังไม่ได้ตรวจ ทั้งที่กติกาของ Clay ต้องการบทความที่ตีพิมพ์และวงการยอมรับ ไม่ใช่ไฟล์ Lean ที่ไม่มีใครอ่าน

สำหรับนักวิจัยและอาจารย์ในไทยที่เริ่มใช้ AI ช่วยเขียนบทพิสูจน์หรือเขียน Lean เปเปอร์นี้ให้เครื่องมือเชิงปฏิบัติที่ดี อย่าถือว่า “Lean ผ่าน” เท่ากับ “เปเปอร์ถูก” ให้เทียบ statement ทีละ lemma ว่าเงื่อนไขในโค้ดตรงกับที่เขียนไว้ไหม เหมือนที่ผู้เขียนทำกับ m+4/m+5 งานแบบนี้ต้องใช้คนที่เข้าใจทั้งคณิตศาสตร์และ Lean ซึ่งยังมีน้อยมากในภูมิภาค และอาจกลายเป็นทักษะที่หายากที่สุดในยุคที่ AI ผลิตบทพิสูจน์ได้เร็วกว่าที่คนตรวจทัน

แหล่งข่าว

• arXiv 2610.08144 — Navier–Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs (6 ต.ค. 2026)
• GitHub — openai/NavierStokesAndEuler (commit f9e8bc5)
• Terence Tao บน Mathstodon — เธรด “Math 2.0” (6 ต.ค. 2026)