เว็บไซต์ปัญหาเออร์ดิชกำลังทำให้การใช้ AI กลายเป็นเรื่องปกติในชีวิตประจำวัน

 (mathstodon.xyz)
1 คะแนน โดย GN⁺ 2025-11-25 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ในกระบวนการแก้ ปัญหาเออร์ดิช #367 มีรายงานว่า เครื่องมือ AI มีบทบาทสำคัญ และทำงานร่วมกับนักคณิตศาสตร์มนุษย์
  • Wouter van Doorn ได้นำเสนอ ตัวอย่างหักล้างที่มนุษย์สร้างขึ้น สำหรับส่วนที่สองของปัญหา จากนั้น Gemini Deepthink ได้สร้างบทพิสูจน์สมบูรณ์ของคองกรูเอนซ์ที่เกี่ยวข้อง
  • Terence Tao ได้นำ บทพิสูจน์ที่อาศัยทฤษฎีจำนวนเชิงพี-แอดิกเชิงพีชคณิต ของ Gemini มาแปลงและเผยแพร่ในรูปแบบที่ง่ายกว่า และต่อมาได้กล่าวถึง ความเป็นไปได้ในการทำ formalization ด้วย Lean
  • Boris Alexeev ใช้ เครื่องมือ Aristotle ของ Harmonic เพื่อทำ Lean formalization จนเสร็จสมบูรณ์ และเพื่อป้องกันการใช้ AI ในทางที่ผิด จึงตรวจสอบข้อความสุดท้ายด้วยตนเองแบบแมนนวล
  • ลำดับเหตุการณ์นี้แสดงให้เห็นว่า การใช้ AI เป็นผู้ช่วยในงานวิจัยคณิตศาสตร์กำลังค่อย ๆ กลายเป็นขั้นตอนมาตรฐาน

กรณีศึกษาความร่วมมือกับ AI ในปัญหาเออร์ดิช #367

  • วันที่ 20 พฤศจิกายน Wouter van Doorn ได้นำเสนอตัวอย่างหักล้างสำหรับส่วนที่สองของปัญหา ซึ่งอาศัยสมมติฐานว่าคองกรูเอนซ์หนึ่งเป็นจริง
    • เขาขอให้ผู้เข้าร่วมคนอื่นช่วยตรวจสอบความถูกต้องของคองกรูเอนซ์ดังกล่าว
  • ไม่กี่ชั่วโมงต่อมา Terence Tao ได้นำปัญหานี้ไปให้ Gemini Deepthink และภายในเวลาประมาณ 10 นาที ก็ได้ทั้งบทพิสูจน์สมบูรณ์ของคองกรูเอนซ์และการยืนยันตรรกะทั้งหมด
    • บทพิสูจน์ของ Gemini ใช้ ทฤษฎีจำนวนเชิงพี-แอดิกเชิงพีชคณิต และ Tao ได้นำมันมาแปลงเป็นบทพิสูจน์เชิงมูลฐานที่ง่ายกว่าแล้วโพสต์ลงเว็บไซต์
    • Tao กล่าวว่าบทพิสูจน์นี้น่าจะสามารถทำ ‘vibe formalizing’ ใน Lean ได้

Lean formalization และการตรวจสอบ

  • สองวันถัดมา Boris Alexeev ได้ใช้ เครื่องมือ Aristotle ของ Harmonic เพื่อทำ Lean formalization จนเสร็จ
    • เพื่อป้องกันการใช้ AI ในทางที่ผิด ข้อความสุดท้ายจึงถูก formalize ด้วยมือโดยตรง
    • กระบวนการทั้งหมดใช้เวลาประมาณ 2–3 ชั่วโมง และผลลัพธ์ถูกเผยแพร่ออนไลน์
  • หลังจากนั้น Tao ได้ใช้ AI เพื่อทำ การค้นหาวรรณกรรม แต่แม้จะพบงานวิจัยที่เกี่ยวข้องอยู่บ้าง ก็ไม่พบสิ่งใดที่เกี่ยวข้องโดยตรงกับปัญหา #367

ปฏิกิริยาและการถกเถียงในชุมชน

  • ผู้ใช้บางคนติดตามสถานการณ์ การใช้ AI ในคณิตศาสตร์เชิงวิชาการ ผ่านอัปเดตของ Tao อย่างสนใจ
  • ผู้ใช้อีกบางคนแสดงมุมมองเชิงวิพากษ์ต่อ แนวทางแบบพิธีการของ Lean โดยชี้ว่าความเข้าใจทางคณิตศาสตร์คือการบีบอัด (compression) แต่ Lean กลับทำให้สิ่งนั้น แตกออกเป็นรายละเอียดระดับต่ำ (decompression)
    • เอกสารที่เกี่ยวข้อง “Against Lean: Why Proof Assistants Formalize the Wrong Thing” โต้แย้งว่า Lean และผู้ช่วยพิสูจน์ที่คล้ายกันจับแก่นแท้ของคณิตศาสตร์ได้อย่างไม่ถูกต้อง
  • ผู้ใช้อีกคนกล่าวถึงปัญหาความแม่นยำของการสนทนากับ AI โดยประเมินว่า ยังต้องปรับจูนอย่างละเอียด แต่ก็ใช้งานได้อย่างเพลิดเพลิน

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

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

 
GN⁺ 2025-11-25
ความเห็นจาก Hacker News

  • เป็นประสบการณ์ที่น่าทึ่งมากที่สามารถโยนบทความวิจัย MLที่เน้นคณิตศาสตร์ให้ AI assistant แล้วรับคำอธิบายแบบง่ายหรือ pseudocode กลับมาได้
    สำหรับคนอย่างฉันที่ไม่เคยได้ใช้สิ่งที่เรียนในมหาวิทยาลัยมาเกิน 25 ปี นี่ช่วยได้มากจริง ๆ

    • สงสัยว่าตรวจสอบความถูกต้องของคำอธิบายพวกนั้นอย่างไร เพราะนิยามทางคณิตศาสตร์มีรายละเอียดที่ละเอียดอ่อนมาก
    • ผมคิดว่านี่แหละคือจุดที่ LLM เปล่งประกายในเรื่องการเรียนรู้
      สามารถใส่งานวิจัยเข้าไปใน Claude แล้วรับภาพรวมก่อน จากนั้นค่อยถามต่อได้
      แม้แต่ในสาขาอย่างชีววิทยาที่ผมไม่เคยเรียนตอนปริญญาตรีหรือโท ก็ยังขุดลึกได้เหมือนกำลังคุยกับติวเตอร์ที่มีความรู้
    • สัญลักษณ์ทางคณิตศาสตร์มีการพึ่งพาบริบทสูงมาก ดังนั้นถ้าขอให้ LLM แปลงเป็นภาษาที่ใช้บริบทต่ำอย่าง Lisp ก็จะเข้าใจโครงสร้างได้เร็วขึ้นมาก

  • หวังว่านักวิจัยและบริษัทต่าง ๆ จะได้ประสิทธิภาพการทำงานที่ดีขึ้นจากงานวิจัยทางวิทยาศาสตร์
    ต่อให้เป็น assistant ที่ยังไม่สมบูรณ์ ก็ยังเพิ่มแรงทดได้มากพอ

    • มีแอปformalization เวอร์ชันเบต้าบน iOS ที่ Tao พูดถึง → Aristotle
      ว่ากันว่าเป็นสตาร์ตอัปที่ก่อตั้งโดย CEO ของ Robin Hood

  • “Vibe formalizing” ให้ความรู้สึกเหมือนเป็นส่วนขยายเชิงตรรกะของ “vibe engineering” และ “vibe coding”
    เวลาที่ชิ้นส่วนของปัญหาต่อกันไม่ลงตัว แนวทางแบบ “Move 37 as a Service” ที่ผสมวิธีไม่เป็นทางการเข้ากับความเข้มงวดทางคณิตศาสตร์ก็น่าสนใจ

    • ก่อนหน้านี้ผมเคยติดอยู่กับบางช่วงตอนอ่านงานวิจัยเรื่องpolyhedral compilation แล้ว ChatGPT ก็ช่วยพา reasoning ไปได้ดี
      แน่นอนว่ามีส่วนที่ผิดอยู่บ้าง แต่เพราะมันสะท้อนความสับสนของผมและคุยต่อยอดได้ จึงช่วยให้เข้าใจลึกขึ้น
      AI เก่งเป็นพิเศษในการจับจุดที่ผู้ใช้กำลังสับสน

  • เคยได้ยินเรื่องการออกเสียงชื่อนักคณิตศาสตร์ชาวฮังการี Erdős
    ภาษาฮังการีโดยทั่วไปสะกดกับออกเสียงแทบจะตรงกัน แต่ในชื่อคนมีข้อยกเว้นอยู่
    ถ้าออกเสียงแบบอังกฤษจะฟังคล้าย ๆ “airdish”

    • Ő ก็เป็นแค่เสียง œ(oe) เท่านั้น ส่วน -y ในชื่อฮังการีเป็นร่องรอยของปัจจัยลงท้าย -iที่เคยสื่อถึงเชื้อสายขุนนาง
      เช่น Görgey, Széchényi, Lánczos
      ลำดับชื่อของฮังการีก็เหมือนญี่ปุ่น คือเรียงแบบนามสกุล-ชื่อ (big endian) เช่น “Erdős Pál”, “Neumann János”
    • เคยเห็นบทกลอนตลกบนบอร์ดภาคคณิตศาสตร์ราวปี 1960 — เป็นมุกว่าบทความที่ Erdos เขียนได้หักล้างทฤษฎีบท ‘วงกลมนั้นกลม’
    • เพราะเครื่องหมายกำกับการออกเสียง (accent marks) มีความหมายต่างกันไปในแต่ละภาษา ผมเลยคิดว่าการใช้เครื่องหมายแบบฮังการีตรง ๆ ในประโยคภาษาอังกฤษดูแปลก
    • ตอนแรกการออกเสียง “airdish” ฟังประหลาด แต่พอลองทำให้ท้ายเสียง ‘os’ เป็น palatalize ก็ฟังสมเหตุสมผลขึ้น
    • อาจเพราะผมไม่ใช่คนอเมริกัน เลยรู้สึกว่าไม่มีใครสนใจปัญหาเรื่องการออกเสียงแบบนี้เท่าไร

  • น่าสนใจที่ในคอมเมนต์มีปฏิกิริยาแนวanti-Lean อยู่ด้วย

    • ผมไม่ใช่นักคณิตศาสตร์ แต่อยากรู้ว่าเนื้อหาฝั่งต่อต้าน Lean พวกนั้นน่าเชื่อถือไหม
      มันเป็นแค่การโปรโมตแนวทางอื่น หรือเป็นการคัดค้าน Lean ในเชิงปรัชญากันแน่
    • คนดังอย่าง Tao มักดึงดูดความสนใจจากพวกคนประหลาดหรือทฤษฎีสมคบคิดอยู่แล้ว

  • ผลลัพธ์จากการใช้ AI ในคณิตศาสตร์เชิงวิจัยออกมาแบบคละกันไป
    บางทีก็เติมข้อโต้แย้งที่ไม่ trivial ให้เองได้ แต่ในบางเรื่องก็หลงทางไปเลย
    ตอนนี้ผมยังคิดว่า AI มีประโยชน์ในฐานะเครื่องมือช่วยมากกว่าจะมาแทนนักคณิตศาสตร์

    • ผมก็มีประสบการณ์คล้ายกัน เคยให้มันช่วยปัญหาการคำนวณ permutationง่าย ๆ ในงานวิจัย แต่กลับใช้เวลามากกว่าลงมือทำเอง
      ในงานเขียนโค้ดมันก็เคยจับบั๊กเล็ก ๆ ไม่ได้เหมือนกัน แต่พอเป็นงานซับซ้อนกลับช่วยได้มาก
      สุดท้ายแล้วเครื่องมือพวกนี้ยังห่างไกลจากการแทนผู้เชี่ยวชาญ และการโฆษณาเกินจริงยิ่งอาจทำลายความน่าเชื่อถือ
      เหมือนคำที่ว่า “ถ้าสัญญาว่าจะให้ดวงจันทร์ ก็ต้องให้ดวงจันทร์” ดังนั้นการตั้งความคาดหวังที่สมจริงจึงสำคัญ

  • ไม่น่าเชื่อว่าในช่วงชีวิตของผมจะได้เห็นยุคแบบในStar Trek ที่เราพูดว่า “Computer, ช่วยวาด proof ของโจทย์คณิตข้อนี้ให้หน่อย” ได้
    อยากให้ “Beam me up Scotty” เป็นจริงได้ด้วยเหมือนกัน

    • แต่ถ้าเป็นแบบนั้นแล้วตายทุกครั้งก็คงลำบากน่าดู

  • คืนนี้ระหว่างขับรถ ผมคุยกับ ChatGPT เรื่องรายละเอียดโครงสร้างของLLVM และ GCC pipeline scheduler
    มันช่วยเพิ่มประสิทธิภาพการทำงานของผมมาก และยังจัดระเบียบบันทึกเกี่ยวกับคอมไพเลอร์ที่กำลังทดลองอยู่ให้โดยอัตโนมัติ
    เป็นเรื่องที่เมื่อก่อนนึกไม่ถึงเลย

    • จากประสบการณ์ของผม LLM น่าจะมีบางรายละเอียดที่ตอบผิดอยู่พอสมควร
      แน่นอนว่าผลลัพธ์ของแต่ละคนอาจต่างกัน

  • ถ้าตั้งชื่อ AI ว่า Erdos ก็ดูเหมือน Erdos number ของพวกเราทุกคนจะกลายเป็น 1

    • หรือไม่ก็ดูเหมือนภาคต่อของ DR-DOS
    • จริง ๆ แล้วก็มีผลิตภัณฑ์ชื่อ Erdos ที่เป็นAI integrated IDE อยู่แล้ว

  • น่าประทับใจที่เขาใช้เครื่องมือ frontierที่มีอยู่ได้ดีและสร้างสภาพแวดล้อมการวิจัยคณิตศาสตร์แบบร่วมมือกันขึ้นมา

    • โชคดีที่คณิตศาสตร์เป็นสาขาที่การบูชาตัวบุคคลหรือการแข่งขันความนิยมไม่ได้เป็นตัวตัดสินว่าผลลัพธ์จริงหรือเท็จ
      ด้วยเหตุนี้ผมจึงคิดว่าคณิตศาสตร์ยังคงเป็นศาสตร์หายากที่ค่อนข้างปลอดจากอิทธิพลแบบลวงโลก