แท็ก

#AI-math

2 บทความ

OpenAI ถอนเปเปอร์คณิตศาสตร์ 3 ฉบับจาก repo openai/math — เครื่องหมายผิดตัวเดียวใน Weil classes ทำให้ผลเรื่อง Hodge ที่ต่อยอดกันล้มไปด้วย และแก้อีก 14 ฉบับ
งานวิจัย

OpenAI ถอนเปเปอร์คณิตศาสตร์ 3 ฉบับจาก repo openai/math — เครื่องหมายผิดตัวเดียวใน Weil classes ทำให้ผลเรื่อง Hodge ที่ต่อยอดกันล้มไปด้วย และแก้อีก 14 ฉบับ

สองวันหลังเปิด repo openai/math ที่มีต้นฉบับคณิตศาสตร์ที่ AI สร้าง 722 ฉบับ OpenAI เพิ่มไฟล์ history.md ลงวันที่ 7 ต.ค. 2026 ประกาศถอนเปเปอร์ 3 ฉบับ เพราะพบเครื่องหมายผิดในเปเปอร์ Weil classes บน abelian eightfolds ซึ่งอีกสองฉบับเรื่อง K3 surfaces ใช้ต่อยอด แก้ไขอีก 14 ฉบับ และเพิ่ม Lean จนผลหลักที่ formalize แล้วอยู่ที่ 300 จาก 719 หรือราว 42%

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

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

เปเปอร์ arXiv ลงวันที่ 6 ต.ค. 2026 ของ Bastounis, Circelli และ Anders Hansen (Cambridge) เทียบเปเปอร์ Navier–Stokes ของ OpenAI กับ Lean ใน repo ที่อ้างว่าเป็นการ formalize แล้วพบว่าหลายจุดพิสูจน์คนละอย่าง เช่น Lemma 8.6 ที่เปเปอร์ใช้อนุพันธ์ m+4 แต่ Lean ใช้ m+5 ผู้เขียนไม่ได้บอกว่าบทพิสูจน์ผิด แต่บอกว่า Lean ที่คอมไพล์ผ่านไม่ได้รับรองบทพิสูจน์ภาษาคนที่ OpenAI เผยแพร่

· อ่าน 6 นาที