OpenAI เปิดผลงานคณิตศาสตร์ 719 ฉบับจาก AI ภายใน ด้าน Terence Tao เตือนผลต่อวงการ
OpenAI เผยแพร่ต้นฉบับคณิตศาสตร์ 719 ฉบับจากแบบจำลองภายในเมื่อ 6 ต.ค. 2026 มีบทพิสูจน์ Lean รองรับราว 42% ขณะที่สมาคมนักคณิตศาสตร์ AHM ขอให้เลิกทำงานกับบริษัท
โดย กองบรรณาธิการ THAI DATA อ่าน 9 นาที ผู้เข้าชม 1
สรุปประเด็นสำคัญ
- OpenAI เผยแพร่ผลงานคณิตศาสตร์จากแบบจำลองภายในที่ยังไม่เปิดให้ใช้ เมื่อ 6 ตุลาคม 2026 ผ่านคลัง GitHub
openai/mathรวม 719 ต้นฉบับใน 372 กลุ่มผลงาน จากโจทย์ที่ป้อนให้ราว 4,000 ข้อ - ผลงานที่ OpenAI อ้างรวมถึงปัญหาที่ค้างมานาน เช่น quasi-Riemann hypothesis, ค่า irrationality exponent ของ π และการหักล้าง Hadwiger's conjecture โดยผลงานเฉลี่ยใช้กำลังประมวลผลเทียบเท่า ChatGPT Pro คิดราว 3 ชั่วโมง
- ณ 7 ตุลาคม ผลหลักมีบทพิสูจน์ใน Lean แล้ว 300 จาก 719 ฉบับ (ราว 42%) และ OpenAI ถอนต้นฉบับ 3 ฉบับ หลังพบข้อผิดพลาดเรื่องเครื่องหมาย พร้อมแก้ไขอีก 14 ฉบับ
- คณะที่ปรึกษา AGMAI ที่ Institute for Advanced Study ย้ำเมื่อ 6 ตุลาคมว่าบทบาทของตน ไม่ใช่การรับรอง ผลงาน ส่วน Association for Human Mathematics (AHM) ออกแถลงการณ์เมื่อ 7 ตุลาคมว่าการปล่อยไฟล์กว่า 700 ไฟล์พร้อมกันคือการแสดงอำนาจ และเรียกร้องให้นักคณิตศาสตร์ เลิกทำงานกับ OpenAI
- Terence Tao โพสต์ 4 ตอนในวันเดียวกันว่าการไล่แก้ปัญหาเปิดด้วย AI กำลังทำให้หลายสาขา "อุดมสมบูรณ์น้อยลง" และเสนอแนวคิด "Math 2.0" ที่ให้น้ำหนักกับการอธิบายและการสร้างชุมชน
OpenAI เผยแพร่ผลงานคณิตศาสตร์ชุดใหญ่ที่สร้างโดยแบบจำลองภายในซึ่งยังไม่เปิดให้ใช้ เมื่อวันที่ 6 ตุลาคม 2026 รวม 719 ต้นฉบับใน 372 กลุ่มผลงาน บริษัทอ้างว่าครอบคลุมปัญหาเปิดหลายร้อยข้อ แต่ ณ วันถัดมามีบทพิสูจน์ที่คอมพิวเตอร์ตรวจได้ใน Lean รองรับเพียงราว 42% และถอนไปแล้ว 3 ฉบับ
ในวันเดียวกันตามเวลาสากล (ตรงกับเช้ามืด 7 ตุลาคมตามเวลาไทย) Terence Tao นักคณิตศาสตร์ที่ติดตามเรื่อง AI กับคณิตศาสตร์อย่างใกล้ชิด โพสต์เธรด 4 ตอนบน Mathstodon ว่าการไล่แก้ปัญหาเปิดด้วย AI ในรูปแบบปัจจุบันไม่ยั่งยืน และทำให้หลายสาขาของคณิตศาสตร์อุดมสมบูรณ์น้อยลง เธรดนี้ไม่ได้เอ่ยชื่อ OpenAI โดยตรง แต่โพสต์หลังประกาศเพียงไม่กี่ชั่วโมง
ปรับปรุงเมื่อ 8 ตุลาคม 2026 เวลา 14:07 น.: เพิ่มหัวข้อแถลงการณ์ของ Association for Human Mathematics (AHM) ที่เรียกร้องให้นักคณิตศาสตร์เลิกทำงานกับ OpenAI และตรวจตัวเลขในคลัง openai/math ซ้ำ ซึ่ง ณ 8 ตุลาคมยังเท่าเดิม (มี Lean 300 จาก 719 ฉบับ ถอน 3 ฉบับ แก้ไข 14 ฉบับ)
OpenAI เผยแพร่อะไรในคลัง openai/math
ประกาศของ OpenAI สั้นและไม่ได้ระบุชื่อปัญหาแม้แต่ข้อเดียว รายละเอียดทั้งหมดอยู่ในคลัง GitHub openai/math ที่เปิดเป็นสัญญาอนุญาต Apache-2.0 ข้อมูลหลักจาก README และประกาศมีดังนี้
- ขนาด 719 ต้นฉบับใน 372 กลุ่มผลงาน (family) แต่ละกลุ่มรวมผลหลัก ผลข้างเคียง และบทพิสูจน์ทางเลือกไว้ด้วยกัน แบ่งตามสาขา 17 สาขา ตั้งแต่ทฤษฎีจำนวนไปจนถึงสมการเชิงอนุพันธ์ย่อย
- ที่มา ผลงานเกือบทั้งหมดได้จากขั้นตอนเดียวกันบนแบบจำลองภายในที่ยังไม่เปิดตัว ตลอดการประเมินแบบจำลองได้รับโจทย์ราว 4,000 ข้อ แล้วคัดเฉพาะผลที่มีนัยสำคัญพอ
- ต้นทุน ผลงานแต่ละชิ้นใช้กำลังประมวลผลเฉลี่ยเทียบเท่า ChatGPT Pro คิดราว 3 ชั่วโมง
- ข้อยกเว้น งานเรื่องบริเวณที่ไม่มีศูนย์ของฟังก์ชันซีตาของรีมันน์ และ Hodge conjecture สำหรับ CM abelian varieties ไม่ได้ใช้ขั้นตอนมาตรฐานนี้ และบทความเรื่องบริเวณ Re(s) > 11/12 มีคนช่วยเรียบเรียงให้อ่านง่ายขึ้น
- ความโปร่งใส มีสรุปการให้เหตุผลของแบบจำลอง 10 เรื่อง สถิติจำนวนโจทย์ที่ลอง และไลบรารี Lean
OpenAI บอกว่าปรึกษาคณะที่ปรึกษา AGMAI ก่อนเผยแพร่ ใช้ GitHub เป็นที่เก็บรอบนี้ และยังมองหาคลังที่ชุมชนดูแลซึ่งตรงตามแนวทางของคณะที่ปรึกษา บริษัทยังจะให้ทุนจัดเวิร์กช็อปและการประชุมเพื่อทำความเข้าใจผลงานที่ AI สร้าง
ตัวอย่างปัญหาที่ OpenAI อ้างว่าแก้ได้
ในเอกสารภาพรวมของคลัง OpenAI ใช้คำว่า "พิสูจน์" (proves) หรือ "หักล้าง" (disproves) กับปัญหาที่นักคณิตศาสตร์รู้จักกันดีหลายข้อ ตารางนี้สรุปตามข้อความของ OpenAI เอง ไม่ได้แปลว่าผลเหล่านี้ได้รับการยอมรับแล้ว
| ปัญหา | สิ่งที่ OpenAI อ้าง | มีบทพิสูจน์ Lean ของผลหลักหรือยัง |
|---|---|---|
| Quasi-Riemann hypothesis | ฟังก์ชัน Dirichlet L ทุกตัว รวมถึง ζ(s) ไม่มีศูนย์ในบริเวณ Re s > 7/8 | มี |
| Irrationality exponent ของ π | มีค่าเท่ากับ 2 พอดี | ยังไม่มี (มีสรุปการให้เหตุผล) |
| Hilbert's tenth problem บนจำนวนตรรกยะ | ไม่มีอัลกอริทึมใดตัดสินได้ว่าพหุนามสัมประสิทธิ์จำนวนเต็มมีรากที่เป็นจำนวนตรรกยะหรือไม่ | ยังไม่มี |
| Hadwiger's conjecture (ทฤษฎีกราฟ) | หักล้างด้วยตัวอย่างค้าน | มี |
| Kaplansky's zero-divisor conjecture | สร้างกลุ่มไร้ทอร์ชันที่ group algebra เหนือ F₂ มีตัวหารศูนย์ | มี |
| Free group factor isomorphism | L(F₂) กับ L(F₃) สมสัณฐานกัน | ยังไม่มี (มีสรุปการให้เหตุผล) |
สถานะ Lean ในตารางอ้างอิงแค็ตตาล็อก formalization ในคลังเมื่อ 8 ตุลาคม 2026 ซึ่งระบุวิธีสร้างว่าเป็น agent และสถานะการรีวิวว่า unchecked
ใครตรวจแล้วบ้าง: Lean การถอนบทความ และกรณี Navier–Stokes
Lean เป็นภาษาโปรแกรมที่ให้คอมพิวเตอร์ตรวจบทพิสูจน์ทีละขั้น OpenAI แนบบทพิสูจน์ Lean มากับผลงานส่วนหนึ่ง และ README ยอมรับเองว่าผลที่ยังไม่มี Lean "อาจมีปัญหา" ภายในวันเดียวก็มีการแก้ไขครั้งใหญ่ บันทึกประวัติของคลังวันที่ 7 ตุลาคมระบุว่าพบข้อผิดพลาดเรื่องเครื่องหมายในต้นฉบับเรื่อง Weil classes ซึ่งทำให้ต้องถอนต้นฉบับ 3 ฉบับ รวมถึงฉบับที่อ้างพิสูจน์ rational Hodge conjecture สำหรับผลคูณของ K3 surfaces และแก้ไขอีก 14 ฉบับ พร้อมเพิ่ม formalization จนครบ 300 จาก 719 ฉบับ
แต่ Lean ก็ไม่ได้ปิดคำถามทั้งหมด งานวิจัยบน arXiv ที่ส่งเมื่อ 6 ตุลาคม โดย Alexander Bastounis (King's College London) Fabian Circelli และ Anders C. Hansen (University of Cambridge) โต้แย้งว่าการให้ AI แปลบทความภาษาคนเป็น Lean แล้วตรวจผ่าน อาจไม่ได้ยืนยันอะไรเกี่ยวกับบทความต้นฉบับเลย ถ้าการแปลไม่ตรงความหมาย ทีมนี้ยกตัวอย่างผลงาน Navier–Stokes ที่ OpenAI ประกาศเมื่อ 8 กันยายน 2026 (ประกาศวันที่ 6 ตุลาคมลิงก์คำว่าแบบจำลองภายในไปยังหน้านั้น) และแสดงว่าบทพิสูจน์ Lean ไม่ตรงกับบทพิสูจน์ภาษาคน เช่น ในขั้นตอนหนึ่งบทความใช้อนุพันธ์เพิ่ม 4 อันดับ แต่โค้ด Lean ใช้ 5 อันดับ จึงพิสูจน์ข้อความที่อ่อนกว่าที่บทความเขียนไว้ ผู้เขียนย้ำว่าไม่ได้ตัดสินว่าบทพิสูจน์ของ OpenAI ผิด แต่เห็นว่าบทพิสูจน์แบบนี้ควรผ่านการตรวจโดยผู้ทรงคุณวุฒิ (peer review) เหมือนบทพิสูจน์อื่น
Terence Tao: จาก "Math 1.0" สู่ "Math 2.0"
Tao อธิบายว่าในคณิตศาสตร์แบบดั้งเดิม ซึ่งเขาเรียกว่า "Math 1.0" การพิสูจน์ปัญหาใหญ่ได้จะตามมาด้วยการบรรยาย เวิร์กช็อป ความร่วมมือ และคนรุ่นใหม่ที่เข้ามาในสาขา จนบทพิสูจน์ถูกย่อยและเข้าไปอยู่ในตำรา แต่ตอนนี้บ่อยครั้งปัญหาถูกแก้โดยผู้สั่งงาน AI ที่ไม่สนใจสาขานั้นต่อ และไม่เข้าใจผลลัพธ์พอจะตอบคำถามหรือขึ้นบรรยายได้ ผลคือมีสัมมนาและความร่วมมือน้อยลง และทิศทางวิจัยที่น่าสนใจถูกเก็บไว้ไม่เปิดเผยเพราะกลัวถูกชิงผลงานไปก่อน
เขาชี้ว่าปัญหาที่แก้แล้วย้อนกลับไปเป็นปัญหาที่ยังไม่แก้ไม่ได้ และการรู้ว่ามีคำตอบอยู่แล้วก็ทำให้การหาเส้นทางอื่นที่ให้ความเข้าใจใหม่ยากขึ้น Tao เขียนว่าคำตอบของปัญหาเปิด "กำลังถูกเก็บเกี่ยวในปริมาณมหาศาลอย่างไม่ยั่งยืน" ทำให้ทั้งสาขาของคณิตศาสตร์อุดมสมบูรณ์น้อยกว่าตอนที่ปัญหาถูกแก้แบบ Math 1.0 มาก
ทางออกที่เขาเสนอคือ "Math 2.0" ที่ลดความสำคัญของการแก้โจทย์อย่างเดียว แล้วให้คุณค่ากับการอธิบาย การสร้างชุมชน และการเปิดทิศทางวิจัยใหม่ Tao เชื่อว่า AI ช่วยได้ในทุกด้าน แต่ต้องใช้จินตนาการมากกว่าแค่ชี้ AI agent ไปที่รายการปัญหาเปิด และวงการต้องทบทวนเกณฑ์ด้านการศึกษา การตีพิมพ์ และความก้าวหน้าในอาชีพ
ทำไมเรื่องนี้สำคัญ
เดือนกันยายน OpenAI ประกาศผลงาน Navier–Stokes เพียงชิ้นเดียว โดยบอกว่ากลุ่ม agent ที่หาคำตอบได้มีราว 10,000 ตัวทำงานพร้อมกัน และบริษัทไม่ได้ตั้งใจขอรับรางวัล Millennium Prize รอบนี้ผลงานมีหลายร้อยชิ้นในคราวเดียว คำถามสำคัญจึงไม่ใช่ว่า AI ทำคณิตศาสตร์ได้หรือไม่ แต่เป็นว่าใครจะตรวจผลงานปริมาณขนาดนี้ และใช้เวลานานเท่าไร
AGMAI ซึ่งมีสมาชิก 9 คน เช่น Timothy Gowers, Martin Hairer และ Edward Witten เรียกการเผยแพร่นี้ว่าเป็นเหตุการณ์สำคัญของคณิตศาสตร์ แต่ย้ำว่าเป็นแค่จุดเริ่มต้นของกระบวนการทำความเข้าใจของมนุษย์ และอนาคตของงานวิจัยจะเป็นแค่การทำความเข้าใจผลงานจากห้องแล็บ AI ไม่ได้ นักคณิตศาสตร์ต้องตั้งคำถามและเลือกทิศทางวิจัยเองได้ คณะนี้ยังเน้นว่าการเข้าถึงเครื่องมือวิจัยและกำลังประมวลผลอย่างเท่าเทียมเป็นเรื่องจำเป็น
ส่วนการทยอยเปิด GPT-6 ให้ผู้ใช้ ChatGPT ทั่วโลกเมื่อ 7 ตุลาคมเป็นอีกข่าวหนึ่ง ณ 8 ตุลาคม README ของคลังยังเรียกแบบจำลองที่สร้างผลงานชุดนี้ว่าแบบจำลองภายในที่ยังไม่เปิดตัว
Association for Human Mathematics เรียกร้องให้เลิกทำงานกับ OpenAI
ขณะที่ AGMAI เลือกวางตัวเป็นผู้ให้คำปรึกษา อีกกลุ่มหนึ่งค้านตรง ๆ Association for Human Mathematics (AHM) ลงแถลงการณ์บนเว็บไซต์ของสมาคมเมื่อ 7 ตุลาคม 2026 (ตัวแถลงการณ์เขียนว่า OpenAI เผยแพร่ผลงาน "เมื่อวานนี้" คือ 6 ตุลาคม) ในนามคณะทำงานด้านการสื่อสารของสมาคม
AHM อธิบายตัวเองว่าเป็นองค์กรวิชาชีพที่สมาชิกบริหารร่วมกัน มีเป้าหมายปกป้องคณิตศาสตร์ในฐานะงานของมนุษย์จากภัยของ AI และรักษาความเป็นอิสระของวงการจากผลประโยชน์ของบริษัท สมาชิกเป็นคนในวงการวิจัยคณิตศาสตร์ระดับบัณฑิตศึกษาขึ้นไป ซึ่งให้คำมั่นว่าจะไม่ช่วยงานบริษัท AI เชิงพาณิชย์และไม่เผยแพร่งานเขียนที่ AI สร้าง ณ 8 ตุลาคม หน้าสมาชิกระบุว่ามี 808 คน ในจำนวนนี้ 532 คนไม่ใช้ AI ในงานวิจัย
สาระหลักของแถลงการณ์มี 3 ส่วน
- ปฏิเสธข้ออ้างของ OpenAI ว่าการเผยแพร่ครั้งนี้ทำให้คณิตศาสตร์ก้าวหน้า และขอให้ทั้งนักคณิตศาสตร์และสาธารณชนประเมินคุณค่าของการเผยแพร่แบบนี้อย่างระมัดระวัง AHM เขียนว่า "การปล่อยไฟล์กว่า 700 ไฟล์ในคราวเดียวไม่ใช่การแสดงผลงานวิชาการ แต่เป็นการแสดงอำนาจ"
- ขอให้เลิกทำงานกับ OpenAI และกลับไปยึดวิทยาศาสตร์ที่มีความเข้าใจของมนุษย์เป็นศูนย์กลาง
- ชี้ว่า OpenAI ข้ามหลักของ AGMAI ซึ่ง AHM ระบุว่าเป็นคณะที่บริษัทใช้อ้างความชอบธรรม แนวทางของ AGMAI ลงวันที่ 29 กันยายน เปิดด้วยการขอให้ห้องแล็บ AI หยุดทดสอบโจทย์คณิตศาสตร์ขั้นสูงบนแบบจำลองที่คนนอกเข้าถึงไม่ได้ ตรงตามที่ AHM อ้าง
ผลต่อองค์กรไทย
- ถือว่าผลลัพธ์จาก AI เป็นข้ออ้างจนกว่าจะตรวจ แม้แต่ OpenAI ยังถอนงานภายในวันเดียว องค์กรที่ใช้ AI วิเคราะห์ข้อมูล เขียนรายงาน หรือออกแบบระบบ ควรมีขั้นตอนให้ผู้เชี่ยวชาญตรวจก่อนนำไปใช้ตัดสินใจ
- ตรวจผ่านไม่ได้แปลว่าตรงโจทย์ บทเรียนจาก Lean ใช้กับงานซอฟต์แวร์ได้ตรง ๆ โค้ดที่ AI เขียนแล้วผ่านชุดทดสอบที่ AI สร้างเอง อาจทดสอบคนละเรื่องกับที่ธุรกิจต้องการ ทีมควรเขียนหรือทบทวนข้อกำหนดและเกณฑ์ทดสอบเอง
- ขอข้อมูลแบบเดียวกับที่นักคณิตศาสตร์ขอ เมื่อผู้ขายอวดผลลัพธ์ของ AI ให้ถามว่าลองไปกี่ครั้ง ล้มเหลวกี่ครั้ง ใช้กำลังประมวลผลเท่าไร และใครตรวจ ตัวเลขอย่างโจทย์ 4,000 ข้อต่อผลงาน 719 ฉบับช่วยให้เห็นภาพจริงมากกว่าตัวอย่างที่คัดมาแล้ว
- เผื่องบสำหรับงานที่ต้องให้ AI คิดนาน ผลงานแต่ละชิ้นใช้กำลังประมวลผลเทียบเท่า ChatGPT Pro คิดราว 3 ชั่วโมง งานวิจัยและพัฒนาที่จะใช้ reasoning model ควรประเมินต้นทุนต่องานก่อนขยายผล
- มหาวิทยาลัยและหน่วยงานวิจัยควรมีนโยบาย ข้อเสนอของ Tao เรื่องทบทวนเกณฑ์การตีพิมพ์และความก้าวหน้าในอาชีพใช้กับไทยได้เช่นกัน โดยเฉพาะการระบุว่าส่วนใดของงานมาจาก AI และจุดยืนเรื่องความร่วมมือกับบริษัท AI ซึ่งวงการคณิตศาสตร์เองยังเห็นต่างกันตั้งแต่การให้คำปรึกษาแบบ AGMAI ไปจนถึงการเลิกทำงานด้วยแบบที่ AHM เรียกร้อง ติดตามข่าว AI อื่น ๆ ได้ที่หมวด AI
คำถามที่พบบ่อย
OpenAI อ้างว่าแก้ปัญหาคณิตศาสตร์อะไรได้บ้าง?
OpenAI เผยแพร่ต้นฉบับ 719 ฉบับใน 372 กลุ่มผลงานเมื่อ 6 ตุลาคม 2026 ตัวอย่างที่บริษัทอ้างได้แก่ quasi-Riemann hypothesis (ฟังก์ชัน Dirichlet L ไม่มีศูนย์ในบริเวณ Re s > 7/8), ค่า irrationality exponent ของ π เท่ากับ 2, Hilbert's tenth problem บนจำนวนตรรกยะ และตัวอย่างค้านของ Hadwiger's conjecture ทั้งหมดนี้เป็นข้ออ้างที่ยังรอการตรวจจากนักคณิตศาสตร์
ผลงานคณิตศาสตร์ของ OpenAI ได้รับการตรวจสอบแล้วหรือยัง?
ยังไม่ครบ OpenAI ระบุเองว่าผลงานอยู่ในขั้นการตรวจสอบต่างกัน ณ 7 ตุลาคม 2026 ผลหลักมีบทพิสูจน์ใน Lean ราว 42% (300 จาก 719 ฉบับ) และถอนต้นฉบับไปแล้ว 3 ฉบับ ส่วนคณะที่ปรึกษา AGMAI ย้ำว่าตนไม่ได้รับรองผลงาน และการประเมินเป็นหน้าที่ของวงการคณิตศาสตร์
บทพิสูจน์ใน Lean รับประกันว่าผลงานถูกต้องหรือไม่?
ไม่เสมอไป Lean ตรวจได้ว่าบทพิสูจน์ที่เขียนเป็นภาษาทางการถูกต้อง แต่ไม่ได้ยืนยันว่าข้อความทางการนั้นตรงกับบทความภาษาคน งานวิจัยบน arXiv ของนักวิจัยจาก King's College London และ Cambridge แสดงว่าบทพิสูจน์ Lean ของผลงาน Navier–Stokes ที่ OpenAI ประกาศไม่ตรงกับบทพิสูจน์ในบทความ
Terence Tao พูดถึงการใช้ AI แก้ปัญหาคณิตศาสตร์ว่าอย่างไร?
Tao เขียนเธรด 4 ตอนเมื่อ 6 ตุลาคม 2026 ว่าการแก้ปัญหาเปิดด้วย AI แบบที่ผู้สั่งงานไม่สนใจสาขานั้นต่อ ทำให้เกิดสัมมนาและความร่วมมือน้อยลง และเสนอให้วงการเปลี่ยนเกณฑ์ไปสู่ "Math 2.0" ที่ให้คุณค่ากับการอธิบายและการสร้างชุมชน เธรดนี้ไม่ได้เอ่ยชื่อ OpenAI โดยตรง
Association for Human Mathematics เรียกร้องอะไรหลัง OpenAI เผยแพร่ผลงานคณิตศาสตร์?
Association for Human Mathematics (AHM) สมาคมวิชาชีพของนักคณิตศาสตร์ที่ประกาศตัวว่าปกป้องคณิตศาสตร์ในฐานะงานของมนุษย์จากภัยของ AI ออกแถลงการณ์เมื่อ 7 ตุลาคม 2026 ปฏิเสธข้ออ้างของ OpenAI ว่าการเผยแพร่ผลงานคณิตศาสตร์ 719 ฉบับทำให้วงการก้าวหน้า เรียกการปล่อยไฟล์กว่า 700 ไฟล์พร้อมกันว่าเป็นการแสดงอำนาจ และเรียกร้องให้นักคณิตศาสตร์เลิกทำงานกับ OpenAI
แหล่งอ้างอิง
- Sharing AI progress in mathematics — OpenAI
- openai/math (README, history, Lean formalization catalogue) — OpenAI (GitHub)
- On OpenAI's Release of Mathematical Results — Advisory Group on Mathematics and Artificial Intelligence (IAS)
- AHM Statement on OpenAI’s October 6 Release of Mathematical Documents — Association for Human Mathematics
- "Math 1.0" placed a premium on being the first to solve an open problem… (4/4) — Terence Tao (Mathstodon)
- Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs — arXiv
พบข้อมูลคลาดเคลื่อน? แจ้งกองบรรณาธิการ