แท็ก

#formal-verification

4 บทความ

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 นาที
Claude พิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์จบครบวงจรใน Lean 4 — 13 ล้านบรรทัดใน 11 วัน แต่ทฤษฎีบทคลาสสิกข้างในถูกพิสูจน์แค่ 'เท่าที่จำเป็น'
งานวิจัย

Claude พิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์จบครบวงจรใน Lean 4 — 13 ล้านบรรทัดใน 11 วัน แต่ทฤษฎีบทคลาสสิกข้างในถูกพิสูจน์แค่ 'เท่าที่จำเป็น'

Anthropic เผยแพร่ 4 ก.ย. 2026 ว่า Claude เขียนพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ที่เครื่องตรวจได้ครบวงจรเป็นครั้งแรก — 13 ล้านบรรทัด Lean, 30,300 ทฤษฎีบทย่อย, 11 วัน, ~6 พันล้านโทเคน แต่ไฟล์ metadata ในรีโปเขียนเองว่าทฤษฎีบทคลาสสิกอย่าง Mazur, Langlands-Tunnell และ Ribet ถูกพิสูจน์เฉพาะรูปแบบที่ข้อโต้แย้งต้องใช้เท่านั้น

· อ่าน 9 นาที
Mistral เปิด Leanstral 1.5 — โมเดลเปิด Apache-2.0 พิสูจน์ทฤษฎีบท Lean 4 ทำ miniF2F เต็ม 100% ปิด PutnamBench 587/672 ที่ ~$4/ข้อ แถมเจอบั๊กจริง 5 ตัว
โมเดลใหม่

Mistral เปิด Leanstral 1.5 — โมเดลเปิด Apache-2.0 พิสูจน์ทฤษฎีบท Lean 4 ทำ miniF2F เต็ม 100% ปิด PutnamBench 587/672 ที่ ~$4/ข้อ แถมเจอบั๊กจริง 5 ตัว

Mistral ปล่อย Leanstral 1.5 (2 ก.ค. 2026) โมเดล MoE เปิดใบอนุญาต Apache-2.0 ขนาด 119B total / 6B active สำหรับพิสูจน์ทฤษฎีบทเชิงรูปนัยบน Lean 4 และตรวจสอบโค้ด — ทำ miniF2F เต็ม 100% ทั้ง val/test, ปิด PutnamBench 587/672 ข้อที่ราว $4/ข้อ (เทียบ Seed-Prover 1.5 ที่ $300+), ครอง SOTA FATE-H 87% และในการทดสอบพบบั๊กที่ไม่เคยรู้มาก่อน 5 ตัวใน 57 repo รวมถึงช่อง overflow วิกฤต.

· อ่าน 6 นาที