แท็ก

#Lean

11 บทความ

Axiom ใช้ฝูง AI agent formalize การจำแนกกรุปเชิงเดียวจำกัด (CFSG) ลง Lean ครบใน 24 วัน — 43.1 ล้านบรรทัด ไม่มี sorry และระหว่างทางเจอจุดผิดในบทพิสูจน์ที่ตีพิมพ์ตั้งแต่ปี 1986
งานวิจัย

Axiom ใช้ฝูง AI agent formalize การจำแนกกรุปเชิงเดียวจำกัด (CFSG) ลง Lean ครบใน 24 วัน — 43.1 ล้านบรรทัด ไม่มี sorry และระหว่างทางเจอจุดผิดในบทพิสูจน์ที่ตีพิมพ์ตั้งแต่ปี 1986

Axiom Math ประกาศเมื่อ 26 ต.ค. 2026 ว่าใช้ฝูง AI agent หลายสิบตัว ภายใต้การกำกับของวิศวกรและนักคณิตศาสตร์ formalize บทพิสูจน์รุ่นแรกของ Classification of Finite Simple Groups ลง Lean 4 ได้ครบใน 24 วัน ได้โค้ด 43.1 ล้านบรรทัด ไม่มี sorry ใช้แค่ axiom มาตรฐาน 3 ตัว และใช้ statement จากโปรเจกต์ TauCeti ภายนอก ระหว่างทางพบ 34 จุดที่เบี่ยงจากเอกสารที่ตีพิมพ์ รวมถึง counterexample ต่อข้ออ้างในบทพิสูจน์ Unbalanced Group Theorem ปี 1986 รีโปเปิดภายใต้ Apache-2.0

· อ่าน 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 นาที
Claude ออกแบบวงจรควอนตัมที่ดีกว่างานตีพิมพ์ 7 ใน 8 โจทย์ — ตัว decoder ของ DQI ใช้เกตน้อยลง 12 เท่า และสร้าง modular inversion แบบ reversible ใหม่บนเส้นโค้ง secp256k1 ใน 53 ชั่วโมง แต่วงจรบวกจุดยังไม่ชนะ Schrottenloher ทุกด้าน
งานวิจัย

Claude ออกแบบวงจรควอนตัมที่ดีกว่างานตีพิมพ์ 7 ใน 8 โจทย์ — ตัว decoder ของ DQI ใช้เกตน้อยลง 12 เท่า และสร้าง modular inversion แบบ reversible ใหม่บนเส้นโค้ง secp256k1 ใน 53 ชั่วโมง แต่วงจรบวกจุดยังไม่ชนะ Schrottenloher ทุกด้าน

Anthropic เผยงานวิจัยเมื่อ 16 ต.ค. ที่ให้ Claude Mythos 5 ออกแบบวงจรควอนตัม 8 โจทย์ผ่านลูป OpenEvolve กับตัวตรวจอัตโนมัติ ผลคือ 7 โจทย์ใช้ทั้ง Toffoli และ qubit น้อยกว่างานที่ดีที่สุดที่ตีพิมพ์ (ดีขึ้น 4.1–39 เท่าตามค่า T×Q) และโจทย์ที่ 8 ได้วงจร modular inversion แบบ divsteps ที่ไม่ต้องเก็บประวัติ ซึ่งเป็นครั้งแรกบน prime field แต่เปเปอร์เองแสดงว่าวงจรบวกจุดของ Claude ยังมีค่า T×Q สูงกว่างานของ Schrottenloher

· อ่าน 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 ถอนเปเปอร์คณิตศาสตร์ 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 นาที
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 นาที
Bend 2 มาแล้ว: ภาษาที่ให้คุณเขียน 'กฎ' แล้วบังคับให้ AI พิสูจน์ว่าโค้ดไม่ละเมิด — type checker เร็วกว่า Rocq 20 เท่า แต่ตัวเลขบนหน้าเว็บมีข้อควรอ่าน
เครื่องมือนักพัฒนา

Bend 2 มาแล้ว: ภาษาที่ให้คุณเขียน 'กฎ' แล้วบังคับให้ AI พิสูจน์ว่าโค้ดไม่ละเมิด — type checker เร็วกว่า Rocq 20 เท่า แต่ตัวเลขบนหน้าเว็บมีข้อควรอ่าน

16-17 ก.ย. ทีม HigherOrderCO ปล่อย Bend 2 ภายใต้ Apache-2.0 พร้อมแนวคิด LAWS.bend — ไฟล์ที่คุณประกาศกฎที่แอปห้ามละเมิด แล้ว compiler จะไม่ยอมให้ AI merge โค้ดจนกว่าจะพิสูจน์ได้ว่ากฎยังอยู่ ตัวเลข benchmark ในรีโปยืนยันว่า checker เร็วจริง (0.295 วิ เทียบ Rocq 5.985 วิ, Lean 36.177 วิ) แต่คำโฆษณา 'เร็วเท่า C บนคอร์เดียว' อ่านจาก pin ของเขาเองแล้วยังช้ากว่า C ใน 15 จาก 16 เบนช์

· อ่าน 8 นาที
นักคณิตศาสตร์ NYU เปิดบันทึกการคุยกับ OpenAI เรื่อง Navier-Stokes — โจทย์รางวัลล้านดอลลาร์ที่กลายเป็นข้อพิพาทเรื่องเครดิต
งานวิจัย

นักคณิตศาสตร์ NYU เปิดบันทึกการคุยกับ OpenAI เรื่อง Navier-Stokes — โจทย์รางวัลล้านดอลลาร์ที่กลายเป็นข้อพิพาทเรื่องเครดิต

8 ก.ย. Tristan Buckmaster ศาสตราจารย์ Courant เผยแพร่แถลงการณ์ 4 หน้าเล่าลำดับเหตุการณ์ที่ OpenAI ติดต่อเขาก่อนประกาศว่าโมเดลภายในพิสูจน์ blowup ของ Navier-Stokes แบบมีแรงกระทำได้ — พร้อมกับที่เขาและ Levent Alpöge ปล่อยผลของตัวเองสามชิ้นที่ผ่านการตรวจด้วย Lean แล้ว OpenAI ปฏิเสธข้อกล่าวหา และ Terence Tao ออกมาเตือนเรื่องการ 'ขุด' โจทย์เปิดจนหมด

· อ่าน 9 นาที
"พิสูจน์" 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 นาที