แท็ก

#formal verification

5 บทความ

OpenAI อ้างโมเดลภายในหักล้าง Exponential Time Hypothesis — นับคำตอบ k-SAT ได้ในเวลา subexponential พร้อม Lean, และอ้างพิสูจน์ local smoothing/Kakeya ทุกมิติกับการมีอยู่ของ Yang–Mills/QCD ด้วย แต่ยังไม่มีใครภายนอกยืนยัน
งานวิจัย

OpenAI อ้างโมเดลภายในหักล้าง Exponential Time Hypothesis — นับคำตอบ k-SAT ได้ในเวลา subexponential พร้อม Lean, และอ้างพิสูจน์ local smoothing/Kakeya ทุกมิติกับการมีอยู่ของ Yang–Mills/QCD ด้วย แต่ยังไม่มีใครภายนอกยืนยัน

เมื่อ 26 ต.ค. 2026 OpenAI ประกาศผลงานใหม่ 3 ชิ้นจากโมเดลภายใน ชิ้นที่ใหญ่ที่สุดคือ preprint "The Exponential Time Hypothesis is False" ซึ่งเสนออัลกอริทึม deterministic ที่นับคำตอบของ k-CNF ได้ในเวลา 2^O(n/√log n) และมี Lean formalization ประกอบ คณะที่นำโดย Impagliazzo, Paturi (ผู้ตั้ง ETH) และ Ryan Williams จะเป็นผู้ตรวจ ส่วนอีกสองชิ้นคือ local smoothing/Kakeya ทุกมิติ และการมีอยู่ของ Yang–Mills/QCD ซึ่งยังไม่ปล่อยเอกสาร ทั้งหมดยังเป็น claim ที่ไม่มีผู้เชี่ยวชาญภายนอกยืนยัน

· อ่าน 6 นาที
AlphaProof Nexus ของ DeepMind ผ่าน peer review ลง Science — เอเจนต์พิสูจน์ด้วย Lean แก้ปัญหา Erdős ที่เปิดอยู่ได้ 9 จาก 353 ข้อ และแค่ 'Ralph loop' + compiler ก็ทำได้เท่ากัน
งานวิจัย

AlphaProof Nexus ของ DeepMind ผ่าน peer review ลง Science — เอเจนต์พิสูจน์ด้วย Lean แก้ปัญหา Erdős ที่เปิดอยู่ได้ 9 จาก 353 ข้อ และแค่ 'Ralph loop' + compiler ก็ทำได้เท่ากัน

งานวิจัย AlphaProof Nexus ของ Google DeepMind ซึ่งเผยแพร่เป็น preprint ตั้งแต่ พ.ค. ได้ลงตีพิมพ์ในวารสาร Science เมื่อ 8 ต.ค. เอเจนต์ที่ให้ Gemini 3.1 Pro เขียนบทพิสูจน์ใน Lean แก้ปัญหา Erdős ที่ยังเปิดอยู่ได้ 9 จาก 353 ข้อ และพิสูจน์ข้อคาดการณ์ OEIS ได้ 44 จาก 492 ข้อ ข้อค้นพบที่สำคัญสำหรับนักพัฒนาคือ เอเจนต์พื้นฐานที่วนสร้างบทพิสูจน์แล้วให้ Lean ตรวจ ก็แก้ปัญหา Erdős ได้ครบทั้ง 9 ข้อเช่นกัน

· อ่าน 5 นาที
OpenAI เปิดรีโป openai/math: ผลงานคณิตศาสตร์ 722 ฉบับจากโมเดลภายในที่ยังไม่เปิดตัว — อ้างพิสูจน์ quasi-Riemann hypothesis และ Unique Games Conjecture พร้อม Lean กว่า 25 ล้านบรรทัด แต่ยังไม่มีนักคณิตศาสตร์ภายนอกตรวจ และ AGMAI ย้ำว่า "ไม่รับรอง"
งานวิจัย

OpenAI เปิดรีโป openai/math: ผลงานคณิตศาสตร์ 722 ฉบับจากโมเดลภายในที่ยังไม่เปิดตัว — อ้างพิสูจน์ quasi-Riemann hypothesis และ Unique Games Conjecture พร้อม Lean กว่า 25 ล้านบรรทัด แต่ยังไม่มีนักคณิตศาสตร์ภายนอกตรวจ และ AGMAI ย้ำว่า "ไม่รับรอง"

6 ต.ค. 2026 OpenAI ปล่อยรีโป openai/math (Apache-2.0) ที่มีต้นฉบับคณิตศาสตร์ 722 ฉบับใน 372 กลุ่มผลลัพธ์ ทั้งหมดสร้างโดยโมเดลภายในที่ยังไม่เปิดตัว ผลเด่นคือ quasi-Riemann hypothesis (ฟังก์ชันซีตาไม่มีศูนย์ใน Re s > 7/8) ซึ่งมีบทพิสูจน์ใน Lean รอให้คนตรวจ แต่ใน catalogue ของรีโปเองยังเขียนสถานะว่า review: unchecked และกลุ่ม AGMAI ออกแถลงการณ์วันเดียวกันว่าการให้คำแนะนำครั้งนี้ไม่ใช่การรับรองผล

· อ่าน 7 นาที
"พิสูจน์" Collatz ที่ AI ช่วยเขียน กลายเป็นบั๊ก soundness ใน Lean kernel — Leo de Moura เผยแพร่ postmortem #14576
เครื่องมือนักพัฒนา

"พิสูจน์" Collatz ที่ AI ช่วยเขียน กลายเป็นบั๊ก soundness ใน Lean kernel — Leo de Moura เผยแพร่ postmortem #14576

1 สิงหาคม 2026 Leonardo de Moura ผู้สร้าง Lean เผยแพร่ postmortem ของบั๊ก soundness ใน kernel — ต้นเรื่องคือ "disproof" ของ Collatz conjecture ที่ AI ช่วยเขียนเมื่อ 25 กรกฎาคม ซึ่งไม่ได้พิสูจน์อะไรเลย แต่ไปเจาะช่องโหว่ใน kernel จนสร้าง proof of False ได้ และมันหลุดผ่านทั้ง kernel ทางการและ nanoda เพราะชนบั๊กคนละตัวพร้อมกัน

· อ่าน 7 นาที
OpenAI ปล่อยงานพิสูจน์คณิตศาสตร์ 10 ข้อพร้อม Lean certificate — ปลดล็อกปัญหาเปิดที่ค้างมาหลายสิบปี รวมถึง non-sofic group
งานวิจัย

OpenAI ปล่อยงานพิสูจน์คณิตศาสตร์ 10 ข้อพร้อม Lean certificate — ปลดล็อกปัญหาเปิดที่ค้างมาหลายสิบปี รวมถึง non-sofic group

1 สิงหาคม 2026 OpenAI เผยแพร่เปเปอร์ 249 หน้าและรีโป openai/ten-proofs (Apache-2.0) รวมผลลัพธ์ 10 ข้อในคณิตศาสตร์และทฤษฎีการคำนวณที่ 'โมเดลภายในของ OpenAI' หาได้เอง — รวมถึงการสร้าง non-sofic group ที่ค้างมาตั้งแต่ปี 1999 และการล้ม Connes's rigidity conjecture — ทุกข้อมาพร้อม formal proof ใน Lean 4 ที่ตรวจซ้ำได้เอง

· อ่าน 7 นาที