นักคณิตศาสตร์มนุษย์ถูก AI แซงหน้าในการหาตัวอย่างโต้แย้ง

 (xenaproject.wordpress.com)
2 คะแนน โดย GN⁺ 5 시간 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • โมเดลตระกูล ChatGPT และ Claude ได้สร้างตัวอย่างโต้แย้งให้กับข้อคาดการณ์ระยะหน่วยของ Erdős, คำถามเรื่องกรุปสคีมของ Grothendieck และ Jacobian Conjecture ภายในเวลาเพียงไม่กี่สัปดาห์ และบางส่วนได้รับการตรวจสอบด้วย Lean แล้ว
  • Sol ของ OpenAI ได้ทำการจัดรูปแบบเชิงพิสูจน์ของตัวอย่างโต้แย้งของ Erdős และผลลัพธ์ทฤษฎีสนามจำกัดเชิงโกลบอลที่จำเป็นทั้งหมดเป็นเวลา 3 สัปดาห์ ด้วยโค้ด Lean 1.2 ล้านบรรทัด ซึ่งมีขนาดมากกว่าครึ่งหนึ่งของ mathlib ที่เขียนมา 9 ปีซึ่งมี 2.3 ล้านบรรทัด
  • สำหรับคำถามอายุ 60 ปีของ Grothendieck นั้น Sol พบตัวอย่างโต้แย้งยาว 12 หน้า และ Fable จัดรูปแบบเชิงพิสูจน์ให้เป็น 1,076 บรรทัดภายใน 4 ชั่วโมง ยืนยันการมีอยู่ของ กรุปสคีมอันดับ 4 แต่ไม่ถูกทำลายด้วย 4
  • การจัดรูปแบบเชิงพิสูจน์อัตโนมัติยังเพิ่มความเร็วการวิจัยอย่างมาก โดย Andrew Yang เขียน โค้ด Lean 250,000 บรรทัด ในราว 2 สัปดาห์ ทำให้โครงการทฤษฎียกโมดูลาร์ที่จำเป็นต่อทฤษฎีบทสุดท้ายของแฟร์มาต์แทบเสร็จสมบูรณ์
  • แม้จะยังไม่อาจเชื่อคณิตศาสตร์แบบไม่เป็นทางการที่ AI สร้างขึ้นได้ตรง ๆ แต่หากเปลี่ยนข้อคาดการณ์ให้เป็นประพจน์ Lean ที่แม่นยำ ก็สามารถตรวจสอบการพิสูจน์และการหักล้างด้วยเครื่องได้ และมนุษย์ต้องดึงเอา อินไซต์ทางคณิตศาสตร์ ที่ลึกกว่าจากตัวอย่างโต้แย้งเหล่านั้น

ข้อคาดการณ์ระยะหน่วยของ Erdős และทฤษฎีสนามจำกัดเชิงโกลบอล

  • วันที่ 20 พฤษภาคม 2026 ChatGPT ได้หักล้าง ข้อคาดการณ์ระยะหน่วยของ Erdős ในเรขาคณิตเชิงไม่ต่อเนื่อง
    • สร้างตัวอย่างโต้แย้งโดยใช้ทฤษฎีจำนวนเชิงลึกของ Golod และ Shafarevich จากทศวรรษ 1960
    • นักคณิตศาสตร์หลายคนตรวจทานเหตุผลล่วงหน้าและเห็นว่าน่าเชื่อถือ แต่ตอนประกาศยังไม่มีการจัดรูปแบบเชิงพิสูจน์ด้วย Lean
  • วันที่ 26 พฤษภาคม Mike Freedman ผู้ได้รับเหรียญ Fields และประธานเจ้าหน้าที่วิทยาศาสตร์ของ Logical Intelligence แจ้งว่าระบบของบริษัทสามารถจัดรูปแบบเชิงพิสูจน์บทความของ ChatGPT ทั้งฉบับเป็น Lean โดยอัตโนมัติได้
    • ขอบเขตที่จัดรูปแบบเชิงพิสูจน์คือประพจน์ที่ว่า ทฤษฎีบท Golod–Shafarevich นำไปสู่ตัวอย่างโต้แย้งของ Erdős
    • ส่วนทฤษฎีจำนวนพื้นฐานที่รองรับตัวมันเองต้องใช้มากกว่า 100 หน้า และพึ่งพาส่วนขนาดใหญ่ของ ทฤษฎีสนามจำกัดเชิงโกลบอล
  • ตลอด 1 ปีหลัง โรงเรียนฤดูร้อนว่าด้วยการจัดรูปแบบเชิงพิสูจน์ของทฤษฎีสนามจำกัด ในปี 2025 กรณีโลคัลเกือบเสร็จสมบูรณ์แล้ว แต่กรณีโกลบอลยังคงค้างอยู่

การจัดรูปแบบเชิงพิสูจน์แบบสมบูรณ์ 1.2 ล้านบรรทัดที่ Sol สร้างขึ้น

  • วันที่ 26 มิถุนายน Boris Alexeev ของ OpenAI โพสต์ใน Lean Zulip ว่าเขาได้ชี้นำโมเดลใหม่ Sol ให้สร้างการจัดรูปแบบเชิงพิสูจน์แบบสมบูรณ์ของตัวอย่างโต้แย้ง Erdős ที่ไม่สมมติอะไรนอกจากสัจพจน์คณิตศาสตร์
  • Sol สร้าง โค้ด Lean 1.2 ล้านบรรทัด ตลอด 3 สัปดาห์
    • mathlib ที่เขียนมานาน 9 ปีมี 2.3 ล้านบรรทัด
    • คุณภาพโค้ดไม่สม่ำเสมอ แต่ได้พิสูจน์ผลลัพธ์ยาก ๆ ของทฤษฎีสนามจำกัดเชิงโกลบอลและทฤษฎีบทที่ไม่เป็นสามัญเกี่ยวกับโคโฮโมโลยีของ number field ได้จริง
  • Lean เป็นภาษาโปรแกรมที่สามารถรันคำสั่งใด ๆ ก็ได้ ดังนั้นเพื่อคำนึงถึงความเป็นไปได้ของโค้ดอันตราย จึงรันโค้ดที่สร้างขึ้นในแซนด์บ็อกซ์
  • ขนาดและความเร็วระดับนี้นำไปสู่ข้อสรุปว่าการพัฒนาคณิตศาสตร์ขนาดใหญ่ที่ AI สร้างขึ้น เป็นสิ่งที่หลีกเลี่ยงไม่ได้

เวิร์กช็อป Formalizing Fermat และการเข้าถึงเครื่องมือ

  • ใน เวิร์กช็อป Formalizing Fermat วันที่ 6–10 กรกฎาคม มีผู้เข้าร่วม 25 คน แต่ระบบจัดรูปแบบเชิงพิสูจน์อัตโนมัติของผู้สนับสนุน Logos Research รองรับการใช้งานพร้อมกันได้เพียง 5 คน
  • มีการมอบสิทธิ์สมัคร Claude Max 1 เดือนให้ผู้เข้าร่วมทุกคนเพื่อใช้ Claude Fable และ OpenAI ก็ให้สิทธิ์เข้าถึง ChatGPT Pro ฟรี 1 เดือนเช่นกัน
    • Sol มีกำหนดเปิดตัววันที่ 9 กรกฎาคม
    • Fable เดิมมีกำหนดสิ้นสุดวันที่ 7 กรกฎาคม แต่การเข้าถึงจริงยังคงอยู่
    • ผู้เข้าร่วมสามารถใช้ Sol และ Fable ได้ 4 ใน 5 วันของเวิร์กช็อป และใช้เครื่องมือของ Logos ได้ตลอดช่วงงาน
  • เพื่อพัฒนาทฤษฎีกรุปสคีมแฟลตจำกัดที่จำเป็นต่อการจัดรูปแบบเชิงพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ จึงป้อนบทความคลาสสิกให้ Fable และ ChatGPT แล้วให้เขียนคำอธิบายภาษาธรรมชาติ
    • Logos พบว่ามีประพจน์หนึ่งในคำอธิบายนั้นเป็นเท็จ และยกตัวอย่างโต้แย้งที่ชัดเจนออกมา
    • เมื่อตรวจสอบพบว่าเอกสารที่ LLM สร้างขึ้นซึ่งอธิบายโครงสร้างมาตรฐานนั้นผิด และมนุษย์ก็พลาดข้อผิดพลาดนี้ระหว่างการอ่าน
    • ความต่างคือ มันไม่ได้ตอบเพียงว่าไม่เข้าใจเหตุผล แต่ให้ ข้อพิสูจน์ว่าเหตุผลนั้นผิด

คำถามเรื่องกรุปสคีมของ Grothendieck

  • Akhil Mathew ศาสตราจารย์จาก UChicago เสนอ คำถามเก่าแก่ของ Grothendieck ให้ AI พิจารณา โดยถามว่ากรุปสคีมอิสระจำกัดทุกตัวที่มีอันดับ (n) จะถูกทำลายด้วย (n) หรือไม่
    • Deligne พิสูจน์กรณีสับเปลี่ยนได้
    • Grothendieck พิสูจน์กรณีที่ฐานเป็น reduced
    • Rene Schoof ศึกษาอีกหลายกรณี และ Emiliano Torti ก็พิสูจน์กรณีทั่วไปยิ่งขึ้นในบทความของปีก่อนหน้า
  • วันถัดจากเวิร์กช็อป คือ 11 กรกฎาคม Sol พบตัวอย่างโต้แย้งและสร้าง PDF ยาว 12 หน้า
    • เมื่อขอไม่ใช่ผลลัพธ์แบบไม่เป็นทางการแต่เป็นการจัดรูปแบบเชิงพิสูจน์ Lean ทั้งหมด Fable ก็จัดรูปแบบเชิงพิสูจน์อัตโนมัติเป็น 1,076 บรรทัดใน 4 ชั่วโมง
  • ก่อนคอมไพล์บนโน้ตบุ๊ก ได้ตรวจสอบก่อนว่าไฟล์ Lean มีแต่ทฤษฎีบท ไม่มีคำสั่งอย่างการลบไฟล์
    • ตรวจสอบว่าประพจน์ใช้เฉพาะแนวคิดจาก mathlib
    • ตรวจสอบว่าประพจน์นั้นแสดงการมีอยู่ของตัวอย่างโต้แย้งจริง
    • ตรวจสอบว่าบทพิสูจน์คอมไพล์ผ่านตามปกติ
    • การตรวจสอบทั้งหมดใช้เวลาไม่ถึง 5 นาที
  • ผลการตรวจสอบยืนยันว่ามี กรุปสคีมอันดับ 4 แต่ไม่ถูกทำลายด้วย 4
  • Akhil Mathew ส่งตัวอย่างโต้แย้งนี้เป็น mathlib PR
  • แม้ตัวอย่างโต้แย้งของ Erdős จะยาวราว 1 ล้านบรรทัด ขณะที่ของ Grothendieck มีเพียงราว 1,000 บรรทัดและเรียบง่ายกว่ามาก แต่นี่ก็เป็นกรณีที่เครื่องแก้คำถามพีชคณิตเรขาคณิตอายุ 60 ปีได้สำเร็จ

ปฏิกิริยาจากผู้เชี่ยวชาญและทฤษฎียกโมดูลาร์

  • วันที่ 14 กรกฎาคม ศาสตราจารย์คนหนึ่งจาก Imperial College ประเมินว่าการที่พบตัวอย่างโต้แย้งของ Grothendieck ได้ง่าย แสดงเพียงว่ามนุษย์ยังคิดกับปัญหานี้ไม่นานพอ
  • Andrew Yang นักศึกษาปริญญาเอก ใช้ Sol และ Fable ในการจัดรูปแบบเชิงพิสูจน์ ทฤษฎียกโมดูลาร์ ซึ่งสำคัญต่อทฤษฎีบทสุดท้ายของแฟร์มาต์ด้วย Lean
    • เขียนโค้ด Lean ราว 250,000 บรรทัดในเวลาประมาณ 2 สัปดาห์
    • ทำให้โครงการนี้แทบเสร็จสมบูรณ์
  • ศาสตราจารย์อีกคนจาก Imperial มองว่าเข้าใจได้ยากที่นักศึกษาปริญญาโทเอกจะจ่าย 200 ดอลลาร์ต่อเดือนให้ Sol และ Fable แต่หลังยืนยันผลงานเหล่านี้แล้วกลับเห็นว่า นักศึกษาปริญญาเอกที่ไม่ยอมจ่าย 200 ดอลลาร์ต่อเดือนเพื่อใช้เครื่องมือเช่นนี้ต่างหากที่ไม่สมเหตุสมผล
  • Harvard ได้มอบ สิทธิ์เข้าถึง Fable ฟรี ให้กับนักศึกษาปริญญาเอก นักวิจัยหลังปริญญาเอก และคณาจารย์ทุกคนอยู่แล้ว

ตัวอย่างโต้แย้งของ Jacobian Conjecture

  • Akhil Mathew และ Levent Alpöge พูดคุยกันถึงวิธีหาตัวอย่างโต้แย้งเพิ่มเติมในพีชคณิตเรขาคณิต และ Fable ก็พบตัวอย่างโต้แย้งของ Jacobian Conjecture ซึ่งเป็นปัญหาชื่อดังที่เปิดค้างมาราว 100 ปี
  • Levent Alpöge โพสต์บน X ว่าผลลัพธ์ที่ดูเหมือนจะแก้ปัญหาได้นั้นเกิดขึ้นระหว่างนัดชิงชนะเลิศฟุตบอลโลกปี 2026
  • เมื่อ Akhil Mathew เสนอ mathlib PR ใหม่ Paul Lezeau ก็ได้จัดรูปแบบเชิงพิสูจน์ตัวอย่างโต้แย้งนั้นด้วยมือไว้แล้ว และส่ง PR ไปยังคลัง Formal Conjectures ของ DeepMind
  • แม้ mathlib จะไม่มีรายการใหญ่ของข้อคาดการณ์ทางคณิตศาสตร์ แต่ คลัง Formal Conjectures มีสิ่งนั้นอยู่
  • หากมนุษย์ตกลงกันได้ในประพจน์ Lean ที่ถ่ายทอดความหมายของข้อคาดการณ์ได้อย่างซื่อตรง งานตรวจสอบว่าโค้ดที่ AI สร้างขึ้นพิสูจน์หรือหักล้างข้อคาดการณ์นั้นหรือไม่ ก็จะกลายเป็นเรื่องง่าย

งานที่ยังเหลือสำหรับมนุษย์หลังการพิสูจน์เชิงรูปนัย

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

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

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

 
GN⁺ 5 시간 전
ความคิดเห็นจาก Hacker News

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

    • นี่น่าจะเป็นเหตุผลว่าทำไมเครื่องจักรถึงเก่งในการหาตัวอย่างโต้แย้ง มันไม่มี ความยึดติดด้านสุนทรียะ กับข้อคาดเดา และไม่อายที่จะให้ผลลัพธ์ที่น่าเกลียด
    • ในฐานะนักคณิตศาสตร์ ความรู้สึกของผมกลับตรงกันข้าม การพิสูจน์มักดัดแปลงจากบทพิสูจน์ที่รู้อยู่แล้วได้เล็กน้อย แต่การสร้างตัวอย่างโต้แย้งต้องเข้าใจโครงสร้างของวัตถุอย่างลึกซึ้ง จึงมักเกินความสามารถของผม
      อย่างไรก็ดี นี่อาจเป็นเพราะผมทำงานกับวัตถุนามธรรมที่เข้าใจยากเป็นหลัก และสำหรับจำนวนหรือพหุนามก็อาจตรงกันข้าม
    • ศาสตราจารย์·นักวิจัย·ครู ที่เปิดเผยปัญหาที่ยังแก้ไม่ได้ให้นักเรียนรู้และชวนให้เข้ามามีส่วนร่วม สมควรได้รับการยกย่องมากกว่านี้ ในชั้นเรียนวิศวกรรมวิชาแรกของมหาวิทยาลัย ผู้สอนเคยบอกนักศึกษาปีหนึ่งว่า “นี่คือปัญหาที่เรายังแก้ไม่ได้ ถ้ามีไอเดียก็บอกเราได้” ตอนนั้นผมรู้สึกว่าตัวเองได้รับการต้อนรับและเป็นส่วนหนึ่งของชุมชนมากกว่าครั้งไหน ๆ และมันเป็นแรงบันดาลใจอย่างมากในช่วงต้นของการเรียนที่อาจกลายเป็นเรื่องน่าเบื่อได้ง่าย
    • ใน 《How to Solve It》 ก็มีเรื่องที่แทบเหมือนกันอยู่
    • มีเกร็ดของ Zeeman ที่สุดโต่งกว่าและไปในทิศตรงข้าม เขาใช้เวลาหลายปีพยายามหาทรงกลมที่ผูกปมได้ในปริภูมิห้ามิติ ก่อนจะตระหนักว่ามันเป็นไปไม่ได้ และพิสูจน์ได้ภายในไม่กี่ชั่วโมง
      https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

  • Yitang Zhang ผู้มีชื่อเสียงจากข้อคาดเดาจำนวนเฉพาะคู่แฝด เคยทำวิจัยเรื่องข้อคาดเดายาโคเบียนอยู่ 7 ปีที่ Purdue ภายใต้การดูแลของ Tzuong-Tsieng Moh ต่อมาพบว่าขั้นตอนสำคัญในวิทยานิพนธ์ของเขาพึ่งพาบทตามที่ผิดพลาดของ Moh และ Moh ก็ปฏิเสธเขียนจดหมายแนะนำให้ Zhang จึงหางานสอนหรืองานวิจัยไม่ได้ และต้องไปทำงานที่ Subway อยู่หลายปี
    ชวนให้สงสัยว่าถ้าตอนเริ่มงานวิจัยในปี 1986 มี ChatGPT อยู่แล้ว จะเป็นอย่างไร ทุกวันนี้มันกลายเป็นเรื่องราวความสำเร็จที่น่าประทับใจ แต่ก็ชวนให้เกิดความรู้สึกซับซ้อน แบบที่วรรคกวี “庾信平生最萧瑟，暮年诗赋动江关” สื่อไว้

    • เคยมีครั้งหนึ่งในระหว่างการสอบปากเปล่าปริญญาเอกคณิตศาสตร์ กรรมการสอบคนหนึ่งพบข้อบกพร่องในบทพิสูจน์ พอนักศึกษาเข้าใจแล้วก็ถามว่า “แล้วตอนนี้จะทำอย่างไรดี?” กรรมการคนนั้นก็แค่ยักไหล่
    • ภายหลังเขาประสบความสำเร็จกับข้อคาดเดาจำนวนเฉพาะคู่แฝด จึงเรียกว่าเป็นเรื่องน่าประทับใจก็ได้ แต่ผมเหนื่อยกับเรื่องแบบนี้ในวงการวิชาการแล้ว การเมืองและการจัดการชื่อเสียง มีมากเกินไป และ Zhang ไม่ควรต้องเจ็บปวดแบบนั้น
      เมื่อขยายงานวิจัยไปทางคณิตศาสตร์ ผมตกใจที่พบว่าข้อความอ้างในวรรณกรรมจำนวนมากเป็นเท็จ และยังแพร่กระจายกว้างไปถึงวรรณกรรมเชิงประยุกต์ด้วย ต่อให้แจ้งปัญหาให้รู้ ก็มักเจอการปกป้องตัวเองและการปฏิเสธแบบในเรื่องของ Zhang LLM มีประโยชน์กับการพิสูจน์ แต่ก็ผิดอย่างหนักได้เช่นกัน และคล้ายกับมีอีกคนหนึ่งที่มีสัญชาตญาณคนละแบบคอยเสนอทิศทางการสำรวจ ดังนั้นแม้ในปี 1986 ผลลัพธ์ก็คงเหมือนเดิม
    • ความหมายของบทกวีที่ ChatGPT แปลคือประมาณว่า “ชีวิตของ Yu Xin เงียบเหงาและอ้างว้างอย่างยิ่ง แต่บทกวีและร้อยแก้วในบั้นปลายชีวิตของเขาสะเทือนถึง Jiangguan”

  • ในคณิตศาสตร์ ตัวอย่างโต้แย้ง มีความสำคัญมากต่อการขัดเกลาคำนิยามและทำให้บทพิสูจน์คมชัดขึ้น ขอแนะนำหนังสือปี 1976 ของ Imre Lakatos ชื่อ 《Proofs and Refutations》 และในสาขาอย่างโทโพโลยี ทฤษฎีความน่าจะเป็น และการวิเคราะห์ ก็มีหนังสือจำนวนไม่น้อยที่ว่าด้วยตัวอย่างโต้แย้งโดยเฉพาะ
    https://en.wikipedia.org/wiki/Proofs_and_Refutations
    https://www.amazon.com/s?k=counterexamples

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

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

  • ดูเหมือนว่า AI จะได้เป็นผู้เขียน 《The Ballad of John Henry》 ฉบับวงการคณิตศาสตร์ด้วย น่าสงสัยว่า แชมป์มนุษย์ คนสุดท้ายที่ยังสามารถสร้างบทพิสูจน์ระดับ “คู่ควรแก่ THE BOOK” ได้ แม้เครื่องจักรก็ยังเทียบไม่ติด จะเป็นใคร
    https://en.wikipedia.org/wiki/John_Henry_(folklore)
    https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

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

  • หากการลงทุน 2,400 ดอลลาร์ต่อปีต่อนักศึกษา ช่วยเร่งให้ผลงานที่มีความหมายของนักศึกษาปริญญาโทหรือเอกเกิดขึ้นได้มาก ก็ไม่มีเหตุผลที่จะไม่ลงทุน เมื่อเทียบกับค่าใช้จ่ายทั้งหมดแล้วแทบเป็นเงินเล็กน้อย

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

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

    • เห็นด้วยกับข้อแรกได้ยาก แม้เส้นโค้งการเรียนรู้จะชัน แต่ การฟอร์แมต Lean·Agda·Rocq ที่เขียนดีนั้นยอดเยี่ยมมากสำหรับการทำความเข้าใจบทพิสูจน์ การฟอร์แมตที่ดีจะแสดงภาพรวมและแกนหลักของเหตุผลเชิงโครงสร้าง และต่างจากบทพิสูจน์บนกระดาษตรงที่สามารถตรวจรายละเอียดของทุกขั้นตอนได้ลึกเท่าที่ต้องการ
      ที่เก็บ TypeTopology Agda ของ Martín Escardó เป็นตัวอย่างที่ดี ตรงกันข้าม การฟอร์แมตที่ LLM สร้างในปัจจุบันอาจรกมาก แม้จะรับรองทฤษฎีบทและมีเหตุผลที่น่าสนใจอยู่ข้างใน ก็ยังต้องใช้แรงมากในการเกลาจนอยู่ในรูปแบบที่ช่วยเพิ่มความเข้าใจทางคณิตศาสตร์ บทเรียน Agda แบบโต้ตอบมีอยู่ที่ lets-play-agda.quasicoherent.io
    • การฟอร์แมตยังใช้กับ แนวทางแบบ Leibniz เพื่อยุติข้อโต้แย้งและขจัดความสงสัยได้อย่างสิ้นเชิง

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

    • ตัวอย่างโต้แย้งช่วยทำให้บทบาทของเงื่อนไขต่าง ๆ ชัดเจนขึ้น หากมีตัวอย่างโต้แย้งที่ง่ายที่สุดและจำง่ายที่สุด ซึ่งแสดงให้เห็นว่าอะไรล้มเหลวเมื่อฝ่าฝืนเงื่อนไขแต่ละข้อของบทพิสูจน์ ก็จะมีประโยชน์มาก
      นักคณิตศาสตร์มักพกพา สวนสัตว์ของตัวอย่างโต้แย้ง ไว้ในหัว เวลาฟื้นคืนทฤษฎีบทขึ้นมาใหม่ ก็สามารถนึกถึงตัวอย่างโต้แย้งที่คมชัดและน่าจดจำ แล้วค่อยจำกัดโดเมนและเงื่อนไขเพื่อกันสิ่งเหล่านั้นออกไป
    • มีหนังสือสอนอย่าง 《Counterexamples in Topology》 และ 《Counterexamples in Analysis》 ที่ใช้ตัวอย่างโต้แย้งเพื่อสอนความละเอียดอ่อนของแต่ละสาขา หนังสือเหล่านี้ได้รับความนิยมมาก เพราะการเรียนรู้รายละเอียดจาก ตัวอย่างผิดปกติหรือเสื่อมสภาพ มักง่ายกว่าการเรียนเฉพาะวัตถุปกติที่ตั้งใจไว้

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

    • มีความเป็นไปได้ Compressed sensing อาจถือเป็นตัวอย่างของคณิตศาสตร์ใหม่ที่นำไปใช้ในชีวการแพทย์ได้ และสามารถลดเวลาการถ่าย MRI ได้มาก ช่วยให้ประสบการณ์ของผู้ป่วยดีขึ้นและทำให้ผู้ป่วยเข้ารับการตรวจได้มากขึ้น
      https://en.wikipedia.org/wiki/Compressed_sensing
    • แม้จะนำไปใช้ในวิศวกรรมและชีวการแพทย์ได้ ก็คงเป็นเรื่องระยะยาว แต่การพัฒนาวิธีการทางคณิตศาสตร์แบบใหม่อาจมีความสำคัญต่อ การวิจัยฟิสิกส์พื้นฐาน ได้เร็วกว่า เพราะบ่อยครั้งที่แบบจำลองดีขึ้นอย่างมากหลังมีเครื่องมือทางคณิตศาสตร์ที่ทำให้สามารถแสดงหรือทดสอบแบบจำลองของจักรวาลได้
    • ต่อให้เป็นไปได้ ก็คงใช้เวลานานมาก เพราะในสาขาประยุกต์ส่วนใหญ่ เรายังเพิ่งเริ่มใช้คณิตศาสตร์เมื่อหลายร้อยปีก่อนได้อย่างเหมาะสมเท่านั้น

  • สักวันหนึ่งนักคณิตศาสตร์อาจจมอยู่กับบทพิสูจน์ที่ต้องตรวจทาน จนทำให้ข้อความเท็จที่ได้รับความเชื่อมั่นเกินจริงเล็ดลอดเข้าสู่วงการคณิตศาสตร์ได้ นักคณิตศาสตร์ในอนาคตอาจต้องตรวจ บทพิสูจน์ที่ AI สร้างยาวนับพันบรรทัด เพื่อหาข้อผิดพลาดที่ละเอียดอ่อน เหมือนวิศวกรซอฟต์แวร์ที่ใช้ AI

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