คณิตศาสตร์ก็มีผี

• Lean คือภาษาโปรแกรมที่ออกแบบมาเพื่อให้สามารถทำให้คณิตศาสตร์เป็นทางการได้ และทำให้นักคณิตศาสตร์สามารถจัดการกับทฤษฎีคณิตศาสตร์ในลักษณะเหมือนโค้ดได้
• ผู้ใช้จะเขียน ทฤษฎี, การพิสูจน์, อสมมติฐาน ในรูปแบบโค้ด และกระบวนการพิสูจน์ดำเนินผ่านชุดคำสั่งที่เรียกว่า tactic
• แม้การพิสูจน์ยังไม่สมบูรณ์ ก็สามารถปิดชั่วคราวด้วย sorry ได้ แต่สิ่งนี้เป็น การพิสูจน์เทียม ที่เปรียบได้กับ any ใน TypeScript
• หากเพิ่มอสมมติฐานที่ไม่ถูกต้อง (เช่น 2 = 3) จะก่อให้เกิดความเสี่ยงเรื่องความขัดแย้งทางตรรกะ และความเป็นไปได้ในการพิสูจน์ ข้อกล่าวทุกข้อ
• Lean จะสรุปผลได้เฉพาะจากอสมมติฐานที่เลือกแบบมีเหตุผลและโครงสร้างการพิสูจน์ จึงมีความสำคัญอย่างยิ่งในการรักษาความถูกต้องทางคณิตศาสตร์

---

Lean: ภาษาสำหรับจัดการคณิตศาสตร์เป็นโค้ด

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

ก้าวแรกของการพิสูจน์ด้วย Lean

• ใน Lean สามารถประกาศทฤษฎีอย่างง่ายได้ด้วยรูปแบบ theorem two_eq_two : 2 = 2 := by sorry
• เมื่อการพิสูจน์ยังไม่เสร็จ สามารถใส่ sorry เพื่อแก้ปัญหาชั่วคราว แต่ไม่ใช่การพิสูจน์จริง
  • sorry ทำให้ผ่านการตรวจสอบการพิสูจน์ของ Lean แต่ในเชิงตรรกะไม่สามารถเชื่อถือได้
• เพื่อให้ได้การพิสูจน์ที่สมบูรณ์ ให้ใช้ tactic อย่าง rfl (reflexivity) เพื่อพิสูจน์สมการที่เป็นเรื่องง่าย อย่างเช่น 2 = 2
• เนื้อหาที่พิสูจน์แล้วสามารถนำไปใช้ซ้ำในทฤษฎีอื่นผ่าน exact ฯลฯ จึงเน้นย้ำเรื่อง โมดูลาร์

อสมมติฐานและความขัดแย้ง: เมื่อคณิตศาสตร์ถูกทำให้หลอกหลอน

• หากเพิ่มอสมมติฐานเช่น axiom math_is_haunted : 2 = 3 ลงไป, Lean จะถือว่าเป็นเรื่องจริง
• อสมมติฐานนี้สามารถนำไปใช้ในขั้นตอนการพิสูจน์ถัดไป ทำให้สามารถพิสูจน์ผลลัพธ์ที่ไม่สมเหตุสมผลทางคณิตศาสตร์ได้ด้วย (เช่น 2 + 2 = 6)
• เป็นไปได้ที่จะใช้ tactic rewrite เพื่อแทนที่ 2 ด้วย 3 และปิดขั้นตอนการพิสูจน์สมการด้วย rfl
• หากอสมมติฐานที่ไม่เหมาะสมก่อให้เกิดความขัดแย้ง, ใน Lean ก็จะเกิดสถานะที่สามารถพิสูจน์ ทุกข้อเสนอ ได้ (ระบบตรรกะพัง)
• ในความเป็นจริง, ในช่วงต้นศตวรรษที่ 20 ความขัดแย้งในระบบอสมมติฐาน เช่น พาราโดกซ์ของ Russell ได้นำไปสู่การพิจารณาเชิงรากฐานของคณิตศาสตร์
• อย่างไรก็ตาม, Lean แสดงให้เห็นอย่างชัดเจนว่าการเลือกอสมมติฐานเป็นเรื่องสำคัญในการคงไว้ซึ่งความชอบธรรมของระบบตรรกะ

Lean ในฐานะ Proof Checker

• หากคัดเลือกอสมมติฐานอย่างเหมาะสมและ Lean ถูกต้องตามตรรกะ จะให้ข้อสรุปที่น่าเชื่อถือในทางทฤษฎี
• จากสมการง่ายไปจนถึงทฤษฎีที่ซับซ้อนมาก (เช่น Fermat’s Last Theorem) ก็ตรวจสอบได้ตามหลักการเดียวกันทั้งหมด
• ทฤษฎีขนาดใหญ่มีลักษณะเป็นต้นไม้ที่เสร็จสมบูรณ์ผ่านการสะสมการพิสูจน์ทฤษฎีย่อยและทฤษฎีย่อยต่อเนื่องแบบซ้ำๆ
• ตัวอย่างเช่น มีโครงการขนาดใหญ่ที่กำลัง formalize Fermat's Last Theorem ใน Lean และมีแผนจะมีระบบการพิสูจน์อย่างเป็นทางการโดยไม่มีการใช้ sorry ชั่วคราวในที่สุด

ความสนุกของการเรียนรู้ Lean

• การพิสูจน์ด้วย Lean คือการผสมผสานที่สร้างสรรค์ระหว่างการเขียนโค้ดและคณิตศาสตร์
• ตั้งแต่การพิสูจน์ข้อเสนอง่าย ๆ ในขั้นแรก ค่อย ๆ สะสมการก่อสร้างคณิตศาสตร์ที่ซับซ้อนและลึกซึ้งอย่างเคร่งครัด ซึ่งเป็นความสนุกสำคัญ
• คู่มือทางการและทรัพยากรชุมชน (เช่น Natural Numbers Game, Mathematics in Lean ฯลฯ) เหมาะสมสำหรับผู้เริ่มต้น
• การใช้ Lean ทำให้คุณ formalize ตรรกะด้วยตัวเอง และทำให้ได้ค้นพบเสน่ห์ของไอเดียแยบยลกับความงดงามของการโต้แย้งอีกครั้ง
• บทความสรุปว่าบางกลุ่มคนแม้ไม่มีเหตุผลชัดเจน ก็ยังรู้สึกว่า Lean ให้ความสนุกที่เป็นพิเศษ

[GN⁺]

ความเห็นจาก Hacker News

• ช่วงนี้กำลังคิดไอเดียว่าจะใช้ระบบแบบ Lean หรืออาจจะใช้ Lean เอง มาเขียนข่าวหรือบทความ non-fiction ใหม่ โดยมองแต่ละข้อความเป็นทฤษฎีบทที่ต้องพิสูจน์ และให้การพิสูจน์รวมถึงการอ้างอิงด้วย เช่นอาจจัดการเป็นการพิสูจน์แบบประกอบว่า “ถ้า 3 แหล่งที่ฉันอนุมัติอ้างว่าเป็นข้อเท็จจริง งั้นนี่ก็เป็นข้อเท็จจริง” และคิดว่าน่าจะสามารถมาร์กอัปทั้งเอกสารเพื่อให้ดูได้ว่าข้ออ้างไหน “พิสูจน์แล้ว” แม้จะไม่สมบูรณ์แบบ แต่ก็เป็นความพยายามจะใช้เทคโนโลยีกู้ความเข้มงวดแบบที่สื่อเคยมีขึ้นมาอีกครั้ง
  • การทำให้ข้อความภาษาธรรมชาติกลายเป็นรูปแบบเชิงฟอร์มัลเป็นพื้นที่ที่มีอุปสรรคมหาศาล ด้วยเหตุผลคล้ายกับที่เขียนโค้ดให้โต้ตอบกับโลกจริงได้ยาก เราต้องจัดการแนวคิดที่เรามองว่าเป็นเรื่องปกติทั้งหมดอย่างละเอียดภายในระบบฟอร์มัล ไม่ว่าจะเป็นอัตลักษณ์ เวลา เหตุและผล ฯลฯ ถึงจะเชื่อมโยงหรือแทนข้อเท็จจริงต่าง ๆ ได้ ถึงอย่างนั้นปัญหานี้ก็น่าสนใจมาก OpenCog เป็นโปรเจ็กต์ที่ผลักดันเรื่องนี้ไปไกลมาก และก็มีสาขาวิจัย Knowledge Representation and Reasoning (KRR) อยู่ในวงวิชาการโดยเฉพาะด้วย วารสาร IJCAI ก็เต็มไปด้วยงานแนวนี้ อีกทั้งนักปรัชญายังสร้างตรรกะจำนวนมากเพื่อทำให้การให้เหตุผลเรื่องเวลา/ภาวะ/ความน่าจะเป็น ฯลฯ เป็นฟอร์มัลได้ แต่น่าเสียดายที่สิ่งเหล่านี้ไม่ค่อยรวมเข้าหากันได้ง่ายนัก (เว้นแต่ระยะหลังจะมีคนแก้ไปแล้ว)
  • คิดว่าความเชื่อสำคัญที่สุดที่เราควรมีต่อข่าวนั้น ส่วนใหญ่ไม่ใช่สิ่งที่พิสูจน์ได้ด้วยชุดของข้อความสัมบูรณ์ แต่เครื่องมือแบบความน่าจะเป็นเชิงเบย์น่าจะเหมาะกว่าสำหรับคำนวณสายโซ่ของการอนุมาน เคยเห็นเครื่องมือสำหรับการประเมินเชิงตัวเลขลักษณะนี้อยู่บ้าง
  • หลังจากเรียนคณิตศาสตร์ในมหาวิทยาลัย รู้สึกว่าการเขียน non-fiction ของตัวเองดีขึ้นมาก เคยอ่านเรียงความที่ SO(แฟน) กับน้องสาวเขียน แล้วใช้ความเข้มงวดแบบอ่านการพิสูจน์เชิงตรรกะ เช่น “ตรงนี้บอกว่า C มาจาก B แต่เหตุผลที่ B มาจาก A กลับหายไป ดังนั้นจะบอกว่า C มาจาก A ไม่ได้” เครื่องมืออย่าง LLM ดูเหมือนจะพอทำให้สิ่งนี้กลายเป็นโปรแกรมได้ แต่ก็มีข้อจำกัดชัดเจนเพราะมีอาการหลอน สร้างข้ออ้างที่ไม่มีอยู่จริงได้
  • ต้องระวัง เพราะแนวทางแบบนี้อาจมอบภาพลักษณ์ของความเป็นกลางทางตรรกะให้กับข้ออ้างที่จริง ๆ แล้วสุดโต่งหรือไร้สาระอย่างมากได้ง่าย ๆ มุมมองทางการเมืองของ Gottlob Frege หนึ่งในบิดาแห่งตรรกะสมัยใหม่ อาจเป็นคำเตือนได้ ลิงก์ที่เกี่ยวข้อง
  • น่าจะน่าสนใจกว่าถ้าทำวิธีวาดโครงสร้างการโต้แย้งทั้งหมดของหัวข้อหนึ่งออกมาเป็นแผนที่ เช่นเริ่มจากคำถามใหญ่อย่าง “พระเจ้ามีอยู่จริงหรือไม่?” แล้วคลี่เหตุผลฝ่ายสนับสนุน ฝ่ายคัดค้าน คำโต้กลับ และคำโต้แย้งต่อคำโต้กลับออกมาเป็นลำดับชั้นทั้งหมด โดยในแต่ละข้ออ้าง การอ้างอิงอย่าง “เพลโตเคยเสนอข้อโต้แย้งแบบนี้” จะมีไว้เพื่อให้บริบททางประวัติศาสตร์มากกว่าจะเป็นหลักฐาน แก่นสำคัญไม่ใช่การตัดสินแพ้ชนะ แต่คือการสร้างแผนที่การโต้แย้งเพื่อไม่ให้วนอยู่กับประเด็นเดิม
• สงสัยว่าเรากำลังสร้างพจนานุกรมของการพิสูจน์ที่เริ่มจากความจริงที่ประจักษ์ชัดไม่กี่ข้อ แล้วค่อยซ้อนการพิสูจน์ต่าง ๆ ขึ้นไปอย่างมีตรรกะใช่ไหม ถ้าอย่างนั้นการพิสูจน์เพิ่มเติมก็เป็นแค่การจัดองค์ประกอบเชิงตรรกะของการพิสูจน์ที่มีอยู่แล้ว อยากให้มีคนเอาไปทำเป็นเกมสไตล์ Zachtronics! มีเกมชื่อ Euclidea ที่ให้ความรู้สึกแบบนี้ในสายตรีโกณมิติอยู่บ้าง และคอนเซปต์การสร้างหอคอยแห่งตรรกะแบบนี้มีเสน่ห์มาก สงสัยว่าคณิตศาสตร์บริสุทธิ์ก็คือสิ่งนี้เองหรือเปล่า และอาจารย์คณิตศาสตร์บริสุทธิ์รู้สึกตื่นเต้นกับการขยายพจนานุกรมตรรกะนี้หรือไม่ อีกอย่างจำได้ลาง ๆ ว่าเคยมีนักคณิตศาสตร์ชื่อดังสร้างรายการการพิสูจน์พื้นฐานไว้ ถ้ามีใครบอกได้ว่าเป็นใคร (หรืออะไร) และเรียกว่าอะไรจะดีมาก คิดว่าน่าจะคือสัจพจน์ (axioms)
  • มีเกมที่เกี่ยวข้องอยู่แล้ว แต่ก็อาจจะยังไม่ตรงกับที่คุณต้องการทั้งหมด (และไม่ใช่เกมสร้างคณิตศาสตร์ทั้งระบบ) ฉันเคยเล่นจริงแล้วสนุกพอสมควร ตัวอย่างก็คือ leanprover-community/nng4 ที่บทความนี้พูดถึง
  • ถ้าจะตอบคำว่า “ช่วยทำสิ่งนี้เป็นเกมสไตล์ Zachtronics ที” ก็อาจพูดได้ว่าคณิตศาสตร์นั่นแหละคือเกมนั้นเอง (พูดเล่นนิดหน่อย) แต่เวอร์ชันเกมจริงก็น่าจะสนุกมาก คณิตศาสตร์บริสุทธิ์ก็คือระบบแบบนั้น ตอนเรียนปริญญาตรีความรู้สึกจะประมาณนั้น แต่พอขึ้นไปถึงงานวิจัยระดับเปเปอร์จะต่างออกไปนิดหน่อย ถ้าอยากได้อารมณ์แบบเกม แนะนำลองดูตำรา abstract algebra อย่าง Dummit and Foote การพิสูจน์มันมีความสนุกแบบเกมอยู่ หนังสือดัง ๆ ถ้าติดขัดก็มักมีคำอธิบายออนไลน์
  • คุณอาจกำลังหมายถึงสัจพจน์ของ Euclid ซึ่งเป็นระบบที่นิยามแนวคิดอย่างจุด เส้น ระนาบ เส้นขนาน ฯลฯ แต่ถ้าอยู่บนทรงกลมแทนระนาบ ระบบนี้ก็ใช้ไม่ได้ หรืออาจกำลังพูดถึงทฤษฎีเซต Zermelo-Fraenkel (ZF/ZFC) ซึ่งคณิตศาสตร์สมัยใหม่ทั้งหมดสร้างอยู่บนสิ่งนี้
  • ยังมีเกมชื่อ Bombe ด้วย เป็นเกมดัดแปลงจาก Minesweeper แทนที่จะเปิดช่องด้วยตัวเอง คุณจะสร้างกฎว่า “เมื่อไรถึงจะปักธงได้” ยิ่งเลเวลสูงขึ้น กฎก็จะเชื่อมต่อกันเหมือน lemma และเมื่อผู้เล่นเก่งขึ้น ก็สามารถคลายข้อจำกัดของชุดเครื่องมือเพื่อทำให้เป็นนามธรรมมากขึ้นได้ ลิงก์เกม
  • คณิตศาสตร์โดยแก่นแท้คือกระบวนการเริ่มจากสัจพจน์แล้วอนุมานไปสู่ข้อสรุป แน่นอนว่าอาจไม่ได้มีแค่นั้น แต่ในระดับของฉันตอนนี้เข้าใจแบบนั้น
• ขอจับผิดนิดหน่อย การบอกว่าทฤษฎีบท two_eq_two ดูเหมือนฟังก์ชันนั้นฟังแปลก เพราะมันไม่มีอาร์กิวเมนต์ จึงใกล้เคียงค่าคงที่มากกว่า (แน่นอนว่าค่าคงที่ก็เป็นฟังก์ชันที่ไม่มีอาร์กิวเมนต์ได้เหมือนกัน) น่าจะน่าเชื่อกว่าถ้าใช้ x_eq_x แบบด้านล่าง แล้วค่อยนำไปใช้กับ 2_eq_2 แบบฟังก์ชัน

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  ตรงนี้ x_eq_x ดูเหมือนฟังก์ชัน และใน 2_eq_2 ก็ถูกใช้แบบนั้นจริง ๆ
  • ทักได้ถูกต้องเลย! ที่ฉันไม่ได้ทำแบบนั้น เพราะการจัดการอาร์กิวเมนต์ของ Lean (โดยเฉพาะแนวคิดอย่าง dependent types — เมื่อให้ x แล้วจะคืน proof ของ x = x) ยังแปลกใหม่สำหรับฉันพอสมควร และเป็นหัวข้อที่ควรแยกอธิบายต่างหาก วางแผนว่าจะพูดถึงในบทความถัดไป
• สิ่งที่ยากตอนเรียน Lean คือ tactics (อย่าง rfl) ดูครอบจักรวาลเกินไป และแม้แต่ในบทสอนก็ยากจะเข้าใจความหมายที่แน่ชัด เช่น C สามารถตามการเปลี่ยนสถานะได้ละเอียดถึงระดับบิต แต่ Lean ให้ความรู้สึกคลุมเครือกว่า และไวยากรณ์ของ tactic rewrite (rw) ก็รู้สึกไม่เป็นธรรมชาติ
  • ใน Coq (ตอนนี้คือ Rocq) การปรับตัวกับ tactics ก็ยากเสมอเหมือนกัน เช่นเคยมีกรณีที่มี “A = B” และ “P(A,A)” แล้วพยายามเปลี่ยนเป็น “P(A,B)” แต่ rewrite กลับใช้ไม่ได้ด้วยเหตุผลที่อธิบายยากมาก (น่าจะเป็นปัญหาเรื่องนิยามของโครงสร้างกลาง) ในทางกลับกัน Metamath กับฐานข้อมูล set.mm ให้พิสูจน์ด้วยการอนุมานที่เป็นรูปธรรมล้วน ๆ โดยไม่มี tactic เลย (ใช้แต่กฎอนุมานอย่าง ax-mp) แต่แบบนี้ก็ต้องจำ utility lemma ที่ใช้ได้จริงจำนวนมาก จึงไม่ง่ายเหมือนกัน
  • นี่เป็นเหตุผลหนึ่งที่ฉันชอบ Agda มากกว่า Agda แทบไม่มี tactic เลย และใช้ Curry-Howard correspondence เพื่อเขียน proof term โดยตรงในภาษา functional programming แต่ในทางกลับกัน ถ้าขี้เกียจสร้าง abstraction และฟังก์ชัน แม้เรื่องเล็กน้อยก็จะกลายเป็นงานที่น่ารำคาญเกินเหตุ จึงต้องมีวินัยมาก
  • อย่างน้อยใน Lean ก็ยังมีข้อดีตรงที่สามารถ “go to definition” เข้าไปดูการทำงานภายในของ tactics ได้ ตอนเรียนอาจจะหนักเพราะมีของให้ดูเยอะ แต่สุดท้ายก็สามารถไล่ดูได้ทั้งหมด (แม้พอถึง type theory ระดับพื้นฐานจะเริ่มจับทางยากอยู่บ้าง) และคุณบอกว่าไวยากรณ์ rewrite ไม่เป็นธรรมชาติ ถ้าอย่างนั้นก็อยากรู้เหมือนกันว่ารูปแบบ rewrite ที่เป็นธรรมชาติสำหรับคุณหน้าตาเป็นอย่างไร
  • สิ่งที่น่าสนใจคือ tactics ทั้งหมดอยู่ในโค้ดระดับ “ผู้ใช้” และอยู่นอก kernel ของตัวพิสูจน์ ซึ่งก็สมเหตุสมผล เพราะเราอยากรักษา kernel ที่เล็กและผ่านการตรวจสอบแล้วไว้โดยไม่เปลี่ยนแปลง แต่ก็แปลว่าเมื่อ tactics ถูกอัปเดตหรือแก้ไข การพิสูจน์เดิมอาจพังได้ เลยสงสัยว่าในโลกจริงสิ่งนี้เป็นปัญหามากน้อยแค่ไหน
  • ต่างจากที่ฉันคาดไว้ ฉันนึกว่าใน Lean เรื่อง reflection กับ rewrite จะเป็นพื้นฐานกว่าการบวก แต่ Lean กลับมี addition มาให้เลย ขณะที่ rfl หรือ rewrite ต้องเรียกใช้เองทุกครั้ง บางที Lean อาจมีอะไรคล้าย prelude ที่ช่วยทำสิ่งนี้ให้อัตโนมัติได้ก็ได้
• อยากรู้ว่าใน Lean มีวิธีอ่าน proof แบบ noninteractive หรือไม่ ตอนเล่น natural number game รู้สึกว่า proof มีแต่รายการคำสั่งอย่าง rw [x] ทำให้อ่านยากมาก แม้ใน editor จะดูสถานะของแต่ละบรรทัดได้ แต่ต้องคลิกตลอดจนเสียจังหวะ ถ้าภาษา Python ไม่มีการเยื้องและต้องคลิกดูแค่โครงสร้างบล็อกเพื่อเข้าใจลำดับการทำงาน ก็คงแย่พอกัน มุมมองของฉันอาจเกิดจากข้อจำกัดของคำสั่งช่วงต้นเกมก็ได้ เลยสงสัยว่าในสภาพแวดล้อม Lean แบบเต็ม ๆ การไหลของการพิสูจน์จะอ่านง่ายขึ้นไหม

  • ใน Lean มีวิธีอ่าน proof แบบ noninteractive ไหม?
    ฉันก็เพิ่งสงสัยเรื่องนี้เมื่อไม่นานและลองหาดู พบว่า บล็อก lean-in-latex มีวิธีทำให้ตามการไหลของ proof ได้จากนอก editor โดยไม่ต้องคลิก และยังเห็นด้วยว่าคอมมูนิตี้ Lean มองเรื่องนี้อย่างไร

  • Rocq เมื่อก่อนเคยมีสิ่งที่เรียกว่า “ภาษาพิสูจน์เชิงคณิตศาสตร์” อยู่ แม้จะหาตัวอย่างใช้งานจริงได้ยาก แต่หน้าตาประมาณนี้

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    แนวทางนี้ทำให้มันอ่านเหมือน “proof เขียนมือ” ในงานวิชาการ แต่แทบไม่มีใครใช้จึงหายไป ส่วนภาษา proof ของ Isar ใน Isabelle ก็คล้ายกัน และจริง ๆ แล้วใกล้เคียงแนวมาตรฐานกว่า ตัวอย่างเช่น

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    มันเขียนโครงสร้างตรรกะทั้งหมดและผลลัพธ์ระหว่างทางไว้อย่างชัดเจน แล้วค่อยย่อรายละเอียดด้วย by ... เฉพาะจุดที่ tactic เหมาะกว่า ฉันไม่แน่ใจว่า Lean มีอะไรคล้ายแบบนี้หรือไม่ แต่อย่างน้อยก็น่าจะใช้เป็นคีย์เวิร์ดค้นหาหรือประเด็นไปถามในฟอรัม Lean ได้
  • เป็นคำถามที่ดีมาก! ฉันยังเป็นมือใหม่จึงไม่กล้าบอกว่าเชื่อถือได้เต็มที่ แต่ขอแชร์ความรู้สึกจากที่ใช้ Lean มาสองสามเดือน การอ่าน proof code ต่างจากการอ่านโค้ดโปรแกรม และใกล้กับการ “สแกน” มากกว่า เราจะโฟกัสที่โครงสร้างการโต้แย้งโดยรวม ใช้ tactic อะไร ใช้ lemma อะไร สไตล์โค้ด Lean จริง ๆ จะเยื้องเมื่อมี goal ใหม่ และคืนระดับเยื้องเมื่อ goal นั้นจบ เพราะฉะนั้นรูปร่างหรือ “shape” ของ argument จึงสำคัญมาก ลองดู ตัวอย่าง PR ของฉัน ถ้าคุ้นกับ tactics แล้ว พอเห็น intro ก็จะรู้ว่าเป็นการเข้าสู่ quantifier เห็น constructor ก็รู้ว่าเป็นการแยก goal ออกเป็นหลายส่วน สุดท้าย tactics ก็คือแมโคร/DSL ที่สร้าง proof tree (term tree) ขึ้นมา สำหรับฉัน เวลาดู proof code มันให้ความรู้สึกเหมือนกำลังจัดการต้นไม้ แยกชิ้นส่วน เติมลำดับ ฯลฯ ถึงอย่างนั้น ถ้าต้องการรู้ assertion กลางทางอย่างแม่นยำก็ยังต้องคลิกอยู่ดี proof ที่มีไอเดียดีจะอ่านได้ชัดเหมือนการดำเนินตรรกะในงานเขียนวิชาการ ดังนั้นคนที่อยากสื่อเจตนาจึงมักตั้งชื่อให้อ่านง่าย เขียนลำดับให้ชัด แยก lemma ย่อยออกมา และเขียนโดยใส่สมมติฐานก่อนแล้วปิดด้วย proof code สั้น ๆ ส่วนสิ่งที่เครื่องมองว่ายุ่งยากแต่ในสายตานักคณิตศาสตร์ชัดอยู่แล้ว ก็มักถูกเขียนแบบ “golfing” คือย่อให้สั้นที่สุด ซึ่งทำให้โค้ดสั้นลงแต่พึ่งพาส่วนที่มนุษย์เข้าใจโดยสัญชาตญาณมากขึ้น สรุปคือโครงสร้างเวลาจะอ่าน Lean นั้นค่อนข้างแฝงอยู่ แต่ก็มีวิธีทำให้ชัดขึ้นได้ และเมื่อชำนาญ tactic มากขึ้นก็จะเข้าใจโครงสร้างได้ดีขึ้นแม้ไม่ต้องคลิก แค่ไล่ชื่อ lemma ก็พอมองเห็นภาพรวมได้ และลำดับก็ประกอบกลับได้ไม่ยาก
• เนื้อหาดีมากจริง ๆ คิดว่าคนที่อธิบายเรื่องแบบนี้ให้ย่อยง่ายได้มีน้อยมาก เคล็ดลับคือการโชว์ขั้นตอนเล็ก ๆ ทุกขั้นที่ผู้เชี่ยวชาญมักข้ามไปเฉย ๆ
  • ขอบคุณ!
• อยากฟังความเห็นในเธรดนี้หน่อยว่าอนาคตของ Lean เทียบกับ idris/coq/agda จะเป็นอย่างไร ฉันสนใจเรียน Knowledge Representation แต่กังวลเรื่องขนาดคอมมูนิตี้และความเสี่ยงระยะยาวก่อนจะทุ่มเวลาไป เพราะเมื่อก่อนเคยลงทุนกับ clojure core.logic แล้วเจอปัญหาความสนใจต่ำและชุมชนเล็ก เลยเริ่มอะไรใหม่ยาก
  • จากประสบการณ์ตรงของฉัน Lean กับ Coq/Rocq ถูกใช้งานมากกว่า Idris และ Agda อย่างเห็นได้ชัด ทั้งในแง่ไลบรารีและคอมมูนิตี้ Rocq ถูกใช้ในงานตรวจพิสูจน์โปรแกรมเยอะกว่าเป็นหลัก ซึ่งฉันคิดว่าเป็นเพราะมีประวัตินานกว่า และก็มีลักษณะเฉพาะหลายอย่างจน Lean อาจตามทันได้ในอนาคต Lean พบได้บ่อยที่สุดในงานพิสูจน์ทฤษฎีบททางคณิตศาสตร์ โปรเจ็กต์ดังของ Rocq ก็มีอย่าง CompCert, CertiCoq, sel4 และกรณีใช้งานตรวจพิสูจน์ซอฟต์แวร์อากาศยานจริงด้วย (ดู รายการโปรเจ็กต์ ที่รวบรวมไว้) ฝั่ง Lean ก็มี mathlib (คลัง proof คณิตศาสตร์), โครงการพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มาต์ (โครงการพิสูจน์ FLT), PFR และโปรเจ็กต์ขนาดใหญ่อื่น ๆ ส่วน Idris กับ Agda เท่าที่รู้ยังไม่มีโปรเจ็กต์ “โลกจริง” มากนัก แต่อาจจำผิดได้ ทั้งหมดนี้ยังเล็กมากเมื่อเทียบกับภาษาอย่าง C++ หรือ JavaScript และในทางปฏิบัติ การตรวจพิสูจน์โปรแกรมนั้นช้าและน่าเบื่อมาก แม้ดูเหมือนว่าสุดท้ายจะมีการเปลี่ยนแปลงระดับรากฐานจาก AI หรือสิ่งอื่น ๆ เข้ามา แต่ทักษะที่เรียนไปก็น่าจะยังใช้ได้
  • ฉันคิดว่าจริง ๆ แล้วไม่ควร “เดิมพัน” กับสาขานี้ในความหมายนั้น เพราะนักคณิตศาสตร์ส่วนใหญ่ไม่ได้สนใจ formalization มากนัก ช่องว่างระหว่าง proof เขียนมือกับไวยากรณ์เคร่งครัดที่คอมพิวเตอร์ต้องการมันกว้างเกินไป ควรเข้าหามันในฐานะสิ่งที่น่าเรียนและน่าลองมากกว่า ถ้าพูดเรื่องอนาคต Lean ช่วงหลังดูคึกคักที่สุดก็จริง แต่แต่ละระบบก็มีฐานผู้ใช้สะสมมานานอยู่แล้ว จึงเดายากว่าจะไปทางไหน
• อยากรู้ว่าถ้าโยนอะไรสุ่ม ๆ ให้ Lean แบบไม่มีเทคนิคหรือเล่ห์เหลี่ยมใด ๆ แล้วดูว่า Lean ยอมรับผ่านไหม จะพอนำไปสู่การค้นพบที่น่าสนใจได้หรือเปล่า หรือจะเอาแนวคิดนี้ไปทำเป็นระบบอัตโนมัติหรือใช้ llm ให้ลองพิสูจน์/ทฤษฎียาก ๆ ไปเรื่อย ๆ แล้วดูว่าอันไหนสำเร็จได้ไหม? คำถามอาจแปลกหน่อย ฉันยังเข้าใจ Prolog แบบผิวเผินมาก
  • ในฐานะคนที่ทำ certified programming เป็นอาชีพ ฉันคิดว่า generative AI กับ formal methods เข้ากันได้ดีที่สุด และการที่ LLM จะมาแทนโปรแกรมเมอร์ได้หรือไม่ ในอนาคตก็อาจขึ้นกับว่ามันทำ certified programming และ combinatorial reasoning ได้ดีแค่ไหน

    ถ้าโยนอะไรสุ่ม ๆ ไป จะมีการค้นพบที่น่าสนใจไหม?
    AI แบบเดิมทำได้ดีในปัญหาที่จำนวนกรณีไม่มากนักอย่างหมากฮอส หมากรุกยากขึ้นอีกระดับ ส่วนโกะนั้นถ้าไม่มี machine learning ก็แทบเป็นไปไม่ได้สำหรับ AI แบบดั้งเดิม ภาษาฟอร์มัลมีจำนวนกรณีและจำนวนสถานะที่ค้นหาได้มากมหาศาลเกินจินตนาการ ถ้าธรรมชาติของปัญหาชัดเจน ก็ brute force ได้ด้วย SMT solver เดิมที SMT solver กับ proof assistant อยู่กันคนละแขนงของ formal methods แต่ตอนนี้เริ่มเป็นโลกที่เสริมกันและกันแล้ว (ดู Sledgehammer, Lean-SMT)
    แล้วถ้าให้ llm หรือระบบอัตโนมัติลองพิสูจน์/ทฤษฎีแบบสุ่มล่ะ?
    เรื่องนี้ยังไม่ใช่งานวิจัยกระแสหลักเต็มตัว แต่ก็มีการทดลองกันมาก ก่อนยุค LLM จะบูมก็มีผู้สนับสนุนรายใหญ่ลงทุนมาหลายปีแล้ว เช่นงานเก่าอย่าง “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies” และงานล่าสุดอย่าง DeepSeek-Prover ทุกอย่างยังเปิดกว้างมาก ทั้งในแง่วิธีฝึกและขอบเขตความเป็นไปได้ในอนาคต
    LLM ในโลกจริงทุกวันนี้ยังอ่อนในภาษา Rocq และ Lean และถ้าตอบผิดขึ้นมา การแก้ให้ถูกนั้นทรมานมาก ถึงอย่างนั้นก็ยังคาดว่าคุณภาพของเครื่องมือ AI จะดีขึ้นมากเมื่อเวลาผ่านไป

  • นี่เป็นสาขาที่มีงานวิจัยและการทดลองกันอย่างคึกคักจริง ๆ!
    ชุมชน Lean รวมตัวกันมากบน Zulip และคุณสามารถดูเธรดอ้างอิงหลากหลายได้ในช่อง Machine-Learning-for-Theorem-Proving
• ในฐานะคนที่เพิ่งสนใจ Lean ครั้งแรกเพราะ alphaproof บทความแนะนำนี้ดีมาก อยากรู้ว่าตอนนี้คุณกำลังทำอะไรกับ Lean อยู่บ้าง?
  • ตอนนี้ยังแค่เรียนคณิตศาสตร์ด้วย Lean อยู่ โดยตาม ตำรา Lean ของ Tao และเติมส่วน sorry ที่เว้นไว้ในแบบฝึกหัดด้วยตัวเอง (คำตอบของฉันอยู่ที่นี่)
• อยากรู้ว่าใน Lean มีโหมดตรวจสอบที่ป้องกันการใช้ proof ที่ไม่น่าเชื่อถือ (proof with "sorry") หรือการเติมสัจพจน์เพิ่มเองแบบอัตโนมัติไหม เช่นตรวจได้หรือไม่ว่า “proof นี้ไม่ได้ใช้ sorry ไม่ว่าทางตรงหรือทางอ้อม” และ “พึ่งพาเฉพาะพลังการพิสูจน์จากชุดสัจพจน์ที่กำหนดไว้เท่านั้น”
  • ตัวอย่าง #print axioms some_theorem ที่กล่าวถึงช่วงท้ายบทความน่าจะตอบคำถามนี้ได้ มันทำให้เห็นว่าการพิสูจน์นั้นพึ่งพา sorry หรือสัจพจน์ที่ยังไม่ได้ตรวจสอบ ไม่ว่าโดยตรงหรือโดยอ้อมหรือไม่
  • ใช้ print axioms เพื่อตรวจว่ามีการเพิ่มสัจพจน์หรือไม่ และดูด้วยว่าคอมไพล์ผ่านโดยไม่มี warning หรือ error หรือเปล่า ส่วน utility ชื่อ SafeVerify ก็จับทริกบางอย่างที่ระบบ RL ค้นพบได้ด้วย
  • มีประเด็นว่าทำแบบนี้ผ่านแมโครได้ด้วย ที่นี่