Lean4 ช่วยค้นพบบั๊กเล็ก ๆ ในงานวิจัยล่าสุดของเทอเรนซ์ เต๋า

 (mathstodon.xyz)
3 คะแนน โดย GN⁺ 2023-10-28 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • โพสต์ของ Terence Tao บน mathstodon.xyz
  • พบข้อผิดพลาดเล็กน้อยแต่สำคัญในงานวิจัยล่าสุดของ Terence Tao จากโครงการทำให้เป็นแบบรูปนัยด้วย Lean4
  • พบข้อผิดพลาดระหว่างกระบวนการทำให้เป็นแบบรูปนัยในหน้าที่ 6 ของงานวิจัย โดยดูตัวบทความได้ที่ https://arxiv.org/pdf/2310.05328.pdf
  • ในงานวิจัยของ Tao พบว่านิพจน์ 12log⁡n−1n−k−1 มีการลู่ออกเมื่อ n=3, k=2
  • ปัญหานี้มีอยู่เฉพาะกับค่า n ที่เล็ก และแก้ได้ด้วยการเปลี่ยนค่าคงที่เชิงตัวเลขบางส่วนในหน้าเอกสาร
  • สำหรับกรณี n≥8 ตรรกะยังคงใช้ได้ และกรณี n ที่เล็กกว่านั้นสามารถจัดการได้ด้วยวิธีที่ง่ายกว่า
  • Lean4 ขอให้ Tao พิสูจน์ว่า 0<n−3 แต่เขามีเพียงสมมติฐานว่า n>2 จึงเกิดความขัดแย้งขึ้น
  • Tao วางแผนจะเพิ่มเชิงอรรถในงานวิจัยฉบับใหม่เพื่อยอมรับข้อผิดพลาดเล็กน้อยที่พบหลังจากลองทำให้เป็นแบบรูปนัยใน Lean4
  • โพสต์นี้กระตุ้นความสนใจและเสียงตอบรับเชิงบวกจากชุมชน พร้อมตอกย้ำความสำคัญของเครื่องมือช่วยพิสูจน์ในการสร้างรากฐานที่มั่นคงสำหรับงานในอนาคต

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2023-10-28
ความคิดเห็นจาก Hacker News
  • นักคณิตศาสตร์ชื่อดัง Terence Tao ใช้ Lean4 และ GPT4 เพื่อค้นพบบั๊กเล็ก ๆ ในงานวิจัยล่าสุดของเขา
  • กระบวนการเรียนรู้ Lean4 ของ Tao ถูกบันทึกไว้ในโพสต์บน Mastodon ของเขา กลายเป็นกรณีศึกษาที่น่าสนใจเกี่ยวกับวิธีที่ Lean4 ช่วยเร่งงานได้
  • สำหรับผู้เริ่มต้น มีการแนะนำ Natural Number Game ว่าเป็นจุดเริ่มต้นที่เข้าใจง่ายสำหรับ Lean4
  • ผู้ใช้รายหนึ่งแบ่งปันประสบการณ์การใช้ TLA+ ของ Lamport เพื่อสร้าง formal specification และลดความผิดพลาดในการเขียนโปรแกรม
  • แม้จะมีความซับซ้อนในการนำไปใช้ในคอมไพเลอร์ แต่ก็ยังมีความสนใจใน dependent types
  • การผสาน Lean4 เข้ากับ automated theorem proving ดูเป็นชุดเทคโนโลยีที่มีอนาคตสดใส และอาจช่วยกระตุ้นการค้นพบใหม่ ๆ
  • การที่ Tao ใช้ Copilot เพื่อเรียนรู้ Lean ถูกยกเป็นตัวอย่างของวิธีที่ Lean4 อาจช่วยลดแรงเสียดทานในการรับเอาเครื่องมือใหม่มาใช้
  • ความคืบหน้าของ Tao กับ Lean4 สามารถติดตามได้บน GitHub ของเขา
  • ผู้ใช้รายหนึ่งเสนอแนวคิดในการผสาน formal proof checker เข้ากับ language model เพื่อสร้างคู่ conjecture-proof แบบสังเคราะห์ ซึ่งอาจต่อยอดไปสู่ความสามารถเหนือมนุษย์ในการสร้างบทพิสูจน์
  • คำว่า "บั๊ก" ถูกใช้เพื่ออธิบายข้อผิดพลาดทางคณิตศาสตร์ ซึ่งผู้ใช้บางคนมองว่าแปลกดี