ทำไมไม่ใช้แค่ Lean ไปเลย?

 (lawrencecpaulson.github.io)
1 คะแนน โดย GN⁺ 2026-04-29 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ประวัติศาสตร์ของการทำคณิตศาสตร์ให้เป็นแบบรูปนัย ไม่ได้เริ่มต้นจาก Lean และตลอดเกือบ 60 ปีที่ผ่านมา ระบบหลายสายได้สั่งสมเทคนิคหลักและผลงานสำคัญไว้แล้ว
  • เครื่องมืออย่าง AUTOMATH ในปี 1968, สาย LCF, HOL, Rocq, ACL2 และ Mizar ต่างสร้างงาน formalization ได้กว้างขวาง ตั้งแต่การวิเคราะห์จริงไปจนถึงทฤษฎีจำนวนเฉพาะ, ทฤษฎีบทสี่สี, และข้อคาดการณ์ของ Kepler
  • Lean สร้างนิยามคณิตศาสตร์สมัยใหม่ขึ้นมาได้อย่างรวดเร็วด้วยคลังไลบรารีขนาดใหญ่และชุมชนที่คึกคัก แต่ propositions as types และ dependent types ก็ไม่ใช่หนทางเดียวของ proof assistant
  • Isabelle ชูจุดเด่นเรื่อง automation ที่ทรงพลัง, ความอ่านง่ายสูง, และการหลีกเลี่ยง dependent types พร้อมสืบทอดขนบ LCF ที่จัดการการตรวจสอบบทพิสูจน์ผ่าน abstraction barrier ของ kernel ได้แม้ไม่มี proof object
  • เมื่อ AI เริ่มช่วยจัดระเบียบบทพิสูจน์แบบมีโครงสร้างและ แปล ข้ามระบบต่าง ๆ ภาระในการมองว่าเครื่องมือเดียวคือมาตรฐานสูงสุดก็อาจลดลงอีกในอนาคต

ระบบยุคแรกและสายพัฒนาการอื่น ๆ

  • AUTOMATH

    • AUTOMATH มีองค์ประกอบเกือบทั้งหมดที่จำเป็นต่อการทำคณิตศาสตร์แบบรูปนัยตั้งแต่ปี 1968 แล้ว
    • ในปี 1977 Jutting ใช้ AUTOMATH ทำ formalization ของ Foundations of Analysis ของ Landau โดยครอบคลุมตั้งแต่ตรรกะล้วนไปจนถึง การสร้างจำนวนเชิงซ้อน
    • ใช้ ชั้นสมมูล และเซตของจำนวนตรรกยะ และยังพิสูจน์เชิงรูปนัยถึง Dedekind completeness ของเส้นจำนวนจริงด้วย
    • ผลงานนี้ไม่ได้เกิดขึ้นซ้ำอีกตลอด 20 ปี และต้องรอถึงกลางทศวรรษ 1990 จึงมี formalization ของจำนวนจริงอีกครั้งใน HOL Light ของ John Harrison และ Isabelle/HOL ของ Jacques Fleuriot
    • สัญกรณ์ใช้งานยากมากและไม่มี automation เลย ทำให้บทพิสูจน์ยาวและอ่านยาก
    • ถึงอย่างนั้น ผู้เขียนเห็นว่าในการจัดการกับชั้นสมมูลนั้นดีกว่า Rocq และต่างจาก setoid hell ที่ผู้ใช้ Rocq มักเจอ Jutting สามารถทำ formalization ของชั้นสมมูลได้อย่างสุขุมเป็นระบบ

  • Boyer และ Moore

    • สาย computational logic ของ Robert Boyer, J Moore เริ่มต้นขึ้นเพื่อการพิสูจน์ความถูกต้องของโค้ด ไม่ใช่เพื่อคณิตศาสตร์
    • ทิศทางนี้ปรากฏชัดครั้งแรกในบทความปี 1973 Proving theorems about LISP functions
    • แม้จะมีข้อจำกัดชัดเจนสำหรับคณิตศาสตร์ทั่วไป แต่ก็ถูกใช้ในการทำ formalization ของผลลัพธ์ลึกซึ้งอย่าง ทฤษฎีบทความไม่สมบูรณ์ของ Gödel, quadratic reciprocity, และ ทฤษฎีบท Banach–Tarski
    • ปัจจุบันสายนี้ในชื่อ ACL2 ถูกนำไปใช้หลัก ๆ กับ การตรวจพิสูจน์ฮาร์ดแวร์

กระแสหลัง LCF

  • Edinburgh LCF มุ่งเน้นทฤษฎีภาษาโปรแกรม แต่แนวคิดที่ใช้ ภาษาฟังก์ชันเป็น metalanguage ของ proof assistant แพร่หลายออกไปมาก
  • หลายกลุ่ม เช่น Cambridge, INRIA และ Cornell ใช้ ML สร้างเครื่องมือยุคแรกอย่าง HOL, Coq (ปัจจุบันคือ Rocq) และ Nuprl
  • กลุ่ม HOL มุ่งที่การพิสูจน์ฮาร์ดแวร์ แต่การพิสูจน์ฮาร์ดแวร์เลขจุดลอยตัวทำให้ต้องใช้ การวิเคราะห์จริง
  • John Harrison ใช้สูตรอินทิกรัลของ Cauchy เพื่อพิสูจน์ผลคณิตศาสตร์จริงจังอย่าง ทฤษฎีจำนวนเฉพาะ ในสาย HOL
  • ภายใต้เป้าหมายที่จะตรวจพิสูจน์ 100 theorems ให้ได้มากที่สุด HOL Light มักอยู่ในกลุ่มผู้นำ
  • จนถึงปี 2014 ระบบสายนี้ได้ทำ formalization ของทฤษฎีบทขั้นสูงหลายรายการ
  • โดยมากทฤษฎีบทเหล่านี้มีบทพิสูจน์ยาวและซับซ้อน งาน formalization ก็มีขนาดใหญ่มาก และมีบทบาทสำคัญในการลดข้อกังขาที่ค้างอยู่ในตัวทฤษฎีบทเอง
โฆษณา

การผงาดขึ้นของชุมชน Lean

  • นักคณิตศาสตร์มองว่าความสำเร็จด้าน formalization ก่อนหน้านี้ยังไม่ครอบคลุมโครงสร้างอันประณีตของคณิตศาสตร์ร่วมสมัยกระแสหลักอย่าง Grothendieck schemes หรือ perfectoid spaces
  • Tom Hales จึงเลือกแนวทางสะสมสิ่งนิยามเหล่านี้เป็นไลบรารี และเลือก Lean โดยเน้น การสั่งสมนิยาม มากกว่าตัวบทพิสูจน์
  • เขานำเสนอแนวทางนี้ในโครงการ Big Proof และมีการหารือแนวคิดคล้ายกันไปพร้อมกัน
  • Kevin Buzzard ได้ฟังเรื่องนี้แล้วตัดสินใจลองใช้ Lean ในการสอน ทำให้การแพร่กระจายหลังจากนั้นเร็วขึ้น
  • จุดเปลี่ยนสำคัญของชุมชน Lean ถูกเสนอว่าเป็นการหลุดพ้นจาก ความยึดติดกับบทพิสูจน์เชิงสรรค์ ที่ครอบงำ Rocq มายาวนาน
  • สัญชาตญาณนิยม เกิดขึ้นหลังปริทรรศน์ของ Russell และมีนัยเฉพาะต่อแนวคิดเรื่องจำนวนจริงด้วย
  • Martin-Löf type theory เป็นรูปแบบพิธีการนิยมเชิงสัญชาตญาณอย่างชัดเจน แต่ผู้เขียนระบุว่า Rocq ไม่อาจมองอย่างเรียบง่ายเช่นนั้นได้
  • ถึงอย่างนั้น ในงานเขียนเกี่ยวกับ Rocq บทพิสูจน์เชิงสรรค์ก็ยังถูกหยิบยกซ้ำ ๆ แม้ในบริบทที่ไม่เกี่ยวหรือไม่มีความหมาย และผู้เขียนมองว่าแนวโน้มนี้ขัดขวางการใช้ Rocq กับคณิตศาสตร์ จนพื้นที่นั้นถูก Lean เข้ามาแทน

propositions as types กับความต่างของ LCF

  • Propositions as types คือความเป็นคู่กันระหว่างสัญลักษณ์ตรรกะ ∀, ∃, →, ∧, ∨ กับตัวสร้างชนิด Π, Σ, →, ×, +
  • กรอบนี้สวยงามและให้ผลเชิงทฤษฎีอย่างมาก แต่ ไม่ใช่หนทางเดียว
  • หากจำกัดความหมายของ proof assistant ว่าเป็นซอฟต์แวร์ที่ตรวจสอบบทพิสูจน์ตามหลัก propositions as types งานวิจัยเกือบทั้งหมดในช่วงครึ่งศตวรรษที่ผ่านมาจะถูกกันออกไปจากคำนิยาม
  • เมื่อนั้นก็จะเหลือเพียง Rocq, Lean และ Agda
  • แม้แต่ AUTOMATH เองก็ไม่ใช่ตัวอย่างของ propositions as types แม้จะมีองค์ประกอบคล้าย Π และ → แต่ในด้านตรรกะกลับตั้งอยู่บน สัจพจน์ แบบเดียวกับตำราตรรกะทั่วไป
  • de Bruijn มองไว้ตั้งแต่ 50 ปีก่อนแล้วว่าจำเป็นต้อง แยกชนิดออกจากพจน์
  • ตัวอย่างเด่นคือการหารต้องรับอาร์กิวเมนต์สามตัว และค่าของ (x/y) ต้องขึ้นกับบทพิสูจน์ของ (y \ne 0) จึงต้องอาศัย proof irrelevance
  • ผู้เขียนยืนยันชัดว่า ความเข้าใจว่าแนวทาง LCF เท่ากับ propositions as types นั้นไม่ตรงกับข้อเท็จจริง
  • ใน Rocq และ Lean มี sort ของพจน์คือ Prop ซึ่งภายในนั้น proof object ทั้งหมดของพจน์เดียวกันจะถูกประเมินเป็นค่าเดียวกัน จึงให้ proof irrelevance
  • แต่นั่นไม่ได้หมายความว่า proof object ขนาดมหึมาจะหายไป เพราะในระบบจริงมันยังคงอยู่
  • การค้นพบสำคัญของ Robin Milner คือใน LCF ไม่จำเป็นต้องมี proof object เลย
  • หากวาง kernel ของบทพิสูจน์ไว้ใน abstract data type ของ ML และใช้นิยามกฎอนุมานเป็น constructor ก็สามารถตรวจสอบบทพิสูจน์แบบไดนามิกได้
  • ผู้เขียนมองว่า abstraction barrier ของ ML ทำให้การโกงเป็นไปไม่ได้
  • การที่เทอมขนาดใหญ่ซึ่งไม่ได้บ่งชี้อะไรเลยแต่กลับกินพื้นที่หลายสิบ MB ดูไร้เหตุผลเป็นพิเศษในยุค RAMmageddon
  • และยังวิจารณ์ต่อว่ามีงานวิจัยที่พยายามทำให้เทอมอันไม่จำเป็นเหล่านั้นดูสง่างามขึ้นอีกด้วย

เหตุผลที่จะเลือก Isabelle

  • หากเพื่อนร่วมงานใช้ Lean อยู่แล้ว ทีมก็มีความเชี่ยวชาญด้าน Lean และไลบรารีตั้งต้นที่จำเป็นก็อยู่ใน Lean การใช้ Lean ย่อมเป็นทางเลือกที่เป็นธรรมชาติ
  • แต่หากเลือกได้อย่างอิสระ ก็มีเหตุผลชัดเจนที่จะพิจารณา Isabelle

  • Automation

    • ผู้เขียนยก automation ที่ทรงพลังที่สุด เป็นข้อได้เปรียบ และมองว่าแม้เทียบกับ “hammer” ทั่วไปแล้วก็ยังไม่มีอะไรสู้ sledgehammer ได้
    • และระบุว่าด้านพีชคณิตเชิงคำนวณก็ควรถูกพิจารณาแยกต่างหากด้วย

  • ความอ่านง่าย

    โฆษณา

  • การหลีกเลี่ยง dependent types

    • เพราะ ไม่มี dependent types จึงหลีกเลี่ยง universe level และความประหลาดอีกหลายอย่างที่มักทำให้ผู้เริ่มต้นลำบาก
    • ผู้เขียนระบุว่าแม้ใน mathlib ของ Lean และ SSReflect, Mathematical Components ของ Rocq ก็ไม่ได้สนับสนุนให้ใช้ dependent types
    • ปัญหาหลักของ dependent types คือหากนำไปใช้อย่างเต็มรูปแบบ การตรวจชนิดจะกลายเป็นปัญหาที่ตัดสินใจไม่ได้
    • นั่นเป็นเพราะการตัดสินความเท่ากันทำไม่ได้แบบตัดสินแน่ชัด และในช่วงแรกเรื่องนี้เคยถูกยอมรับว่าเป็นเรื่องปกติ
    • ตั้งแต่ราวปี 1990 เป็นต้นมา ฉันทามติค่อย ๆ ขยับไปสู่การทำให้การตรวจชนิดตัดสินได้ โดยลดความเท่ากันให้เหลือ definitional/intensional equality
    • ผลคือ (T(N+1)) และ (T(1+N)) กลายเป็นชนิดคนละตัวกัน
    • ข้อจำกัดนี้ส่งผลกับบทพิสูจน์จริงด้วย และแม้แต่การตรวจ definitional equality เองก็ยังมี ภาระการคำนวณ สูง

คณิตศาสตร์สมัยใหม่ที่ทำได้แม้ไม่มี dependent types

  • ผู้เขียนระบุว่า ณ ปี 2017 ยังมองอย่างระมัดระวังกว่านี้มากว่า Isabelle จะรองรับคณิตศาสตร์ได้ไกลแค่ไหน
  • ในเวลานั้นดูเหมือนง่ายที่จะคิดว่าหัวข้ออย่างต่อไปนี้จำเป็นต้องใช้ dependent types
  • แต่ผ่าน งานวิจัย Alexandria ก็ได้เรียนรู้อะไรมากมาย และสรุปแก่นสำคัญว่า อย่าพยายามยัดทุกอย่างให้กลายเป็นชนิด

ทิศทางข้างหน้าและ AI

  • Lean ทำหลายอย่างได้ถูกต้องและรองรับแม้กระทั่ง บล็อกบทพิสูจน์แบบซ้อน จึงมีศักยภาพที่จะเป็นภาษาบทพิสูจน์ที่อ่านง่ายได้อย่างเพียงพอ
  • ตอนนี้ชุมชน Lean ต้องนำความสามารถนั้นมาใช้จริง และผู้ใช้ Isabelle นั้นโดยมากได้ทำเช่นนั้นอยู่แล้ว
  • ความสำคัญอยู่ที่ ความโปร่งใสของข้อความบทพิสูจน์ ที่มนุษย์อ่านได้จริง มากกว่าการมี proof object ที่เครื่องคอมพิวเตอร์ตรวจได้
  • การมาของ AI ทำให้ความต่างนี้ยิ่งชัดขึ้น
  • บทพิสูจน์ที่ AI สร้างมักจะรก แต่ก็จัดระเบียบด้วย sledgehammer ได้ง่าย และถ้าโครงสร้างดี แม้รายละเอียดจะมากเกินไปก็ยังอ่านได้
  • เมื่อเป็นเช่นนั้นก็จะมองเห็นลำดับการดำเนินเรื่องได้ง่ายขึ้น และย่อให้อยู่ในรูปที่เรียบง่ายกว่าได้ง่ายขึ้นด้วย
  • ระยะหลังยังมี งานวิจัย ที่ให้ language model เรียก sledgehammer โดยตรงด้วย
  • AI ยังสามารถ แปล บทพิสูจน์แบบมีโครงสร้างและอ่านง่ายจาก proof assistant หนึ่งไปสู่อีกระบบหนึ่งได้ไม่ยาก
  • เมื่อเป็นเช่นนั้น ภาระในการต้องเลือกระบบใดระบบหนึ่งก็จะลดลงไปเอง

เติมช่องว่างเรื่อง Mizar

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

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

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

 
GN⁺ 2026-04-29
ความคิดเห็นจาก Hacker News

  • ผู้อ่าน HN ส่วนใหญ่น่าจะใกล้เคียงกับการเป็น โปรแกรมเมอร์ มากกว่านักคณิตศาสตร์ ดังนั้นการมอง Lean จากมุมของการเขียนโปรแกรมจึงดูใช้งานได้จริงกว่าการมองจากมุมพิสูจน์ทางคณิตศาสตร์
    หนังสือที่อธิบาย Lean จากมุมมองการเขียนโปรแกรมเชิงฟังก์ชันอย่าง https://leanprover.github.io/functional_programming_in_lean/ ค่อนข้างดี
    ตัวฉันเองก็กำลังเรียน Lean อยู่เหมือนกัน เลยอาจยังมี มุมมองแบบโลกสวยของมือใหม่ อยู่บ้าง แต่เป้าหมายคืออยากเขียนและพิสูจน์โค้ดแบบที่โปรแกรมเมอร์ทั่วไปใช้จริง เช่นอัลกอริทึมบีบอัด/คลายบีบอัด ตามตัวอย่าง lean-zip ล่าสุด
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • ระหว่างอ่านหนังสือเล่มนี้ ฉันลองทำ ตัวทำให้นิพจน์พีชคณิตคอมพิวเตอร์เรียบง่าย พื้นฐานด้วย Lean เอง
      https://github.com/dharmatech/symbolism.lean
      เป็นงานพอร์ตจากโค้ด C# มา และ พลังในการแสดงออก ของ Lean น่าทึ่งมาก
    • ถ้าเป็นงานลักษณะนั้น Dafny ก็อาจเป็นตัวเลือกคล้ายกันไม่ใช่หรือ
      เคยเห็นมันถูกพูดถึงอยู่พักหนึ่งเมื่อก่อน แต่ช่วงหลังไม่ได้ตามสายนี้ละเอียดนัก
    • จำได้ว่าในยุค 1990s มีการทดลองเรื่อง การพิสูจน์ความถูกต้องของซอฟต์แวร์ อยู่กรณีหนึ่ง และเท่าที่จำได้ ความผิดพลาดฝั่งคำอธิบายประกอบของตัวพิสูจน์สุดท้ายกลับมีมากกว่าซอฟต์แวร์จริงเสียอีก
      และยังเห็นอุปสรรคอีกสองอย่าง อย่างแรกคือการรู้ให้ได้ว่าซอฟต์แวร์ ควรทำอะไร นั้นยากในตัวมันเอง และสิ่งที่ผู้ใช้อยากทำก็ไม่จำเป็นต้องตรงกับสิ่งที่ลูกค้ายอมจ่ายเงินเสมอไป
      อย่างที่สองคือคุณภาพงานของนักพัฒนาจำนวนมากต่ำมากอยู่แล้ว จึงยากจะคาดหวังว่าพวกเขาจะใช้ ภาษาแห่งความจริง ได้ดีกว่าภาษาอย่าง Java
      แต่ข้อที่สองอาจหายไปได้ถ้าถูกแทนที่ด้วยระบบ AI ที่ใส่ใจในรายละเอียดตามต้องการ ซึ่งถ้าเป็นแบบนั้นสถานการณ์ก็อาจเปลี่ยน
    • แล้ว การเขียนโปรแกรมที่ไม่ใช่เชิงฟังก์ชัน ล่ะ
      ฉันมองว่าการเขียนโปรแกรมเชิงฟังก์ชันเองก็แทบไม่เกี่ยวข้องกับโปรแกรมเมอร์ส่วนใหญ่พอ ๆ กับคณิตศาสตร์ที่ถูกละไว้แล้ว

  • ดูเหมือนผู้เขียนจะเข้าใจ Lean ผิดไปมากพอสมควร และยิ่งน่าแปลกเพราะเขาดูเหมือนเป็นคนที่รู้เรื่องสายนี้ดี
    เหมือนเขาจะมองว่า Lean เก็บวัตถุพิสูจน์ไว้แบบครบถ้วน และสุดท้ายก็ตรวจวัตถุพิสูจน์ขนาดมหึมาเพียงชิ้นเดียวที่คลี่ทุกนิยามออกหมดแล้ว ซึ่งห่างไกลจากความเป็นจริง
    Lean ใช้การปรับแต่งแบบเดียวกับที่ผู้เขียนยกย่องว่าเป็นข้อดีของ LCF แทบทั้งหมด เปรียบได้กับการลบกระดานไปเรื่อย ๆ ระหว่างพิสูจน์
    ใน Lean4 ถ้าเขียนด้วย theorem แทน def วัตถุพิสูจน์นั้นจะไม่ถูกใช้อีกต่อไป และนี่ไม่ใช่แค่ optimization ธรรมดา แต่เป็นคุณสมบัติแกนกลางของภาษาเลย theorem เป็น opaque
    ต่อให้มี proof term หลงเหลืออยู่ ก็มีไว้เพียงเพื่อให้ผู้ใช้ดูได้ในโหมดโต้ตอบเท่านั้น และ kernel เองก็ไม่สามารถสนใจได้ด้วยซ้ำว่าวัตถุพิสูจน์นั้นคืออะไร

    • นี่ใกล้เคียงกับ ความต่างเชิงแนวคิด มากกว่าความต่างด้าน implementation
      ใน LCF การพิสูจน์กับ term เป็นคนละอย่างกัน และฉันคิดว่าโดยพื้นฐานมันก็ควรเป็นแบบนั้น ความสับสนแบบ Curry-Howard นี้ไม่จำเป็นเลย แต่หลายคนกลับคิดว่านี่คือวิธีเดียวในการทำคณิตศาสตร์ด้วยคอมพิวเตอร์
      ถ้าต้องการ ใน LCF ก็สามารถเก็บและใช้ประโยชน์จาก proof ได้ และใน Lean ถ้าต้องการก็แค่ลบมันออกด้วย optimization เท่านั้น
    • ใน dependent type theory นั้น วัตถุพิสูจน์ ก็คือ term ที่เติมเต็ม type บางตัวเฉย ๆ ดังนั้นเลยสงสัยว่าหมายความว่า implementation ของ Lean สามารถสร้างการพิสูจน์ได้โดยไม่ต้องสร้าง term แบบนั้นจริงหรือไม่
    • ฟังดูถูกต้อง
      แนวทางแบบ abstract type อาจช่วยประหยัดหน่วยความจำได้บ้าง แต่ก็เป็นแค่ความต่างระดับค่าคงที่ ไม่ใช่การปรับปรุงเชิงเส้นกำลัง
      ข้อบ่นว่า Lean เปลืองไปเป็น หลายสิบ MB อาจสำคัญมากในยุค 1980s–90s แต่ทุกวันนี้อาจไม่ใช่ข้อได้เปรียบที่ชี้ขาดขนาดนั้นแล้ว

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

    • สุดท้ายก็คือเรื่องของ network effects
      แต่ผลแบบนี้แม้ในขณะนั้นจะดูเหมือนถาวร ทว่าในความจริงมักอยู่ได้ไม่นานอย่างที่คิด ถ้ามีแค่นั้นที่สำคัญจริง Perl ก็ควรยังเป็นยักษ์ใหญ่อยู่จนถึงตอนนี้
      สำหรับ Lean นั้นการมี ไลบรารีขนาดใหญ่ ก่อนถือว่าสำคัญมาก คล้ายกับที่ CPAN เคยเป็นสำหรับ Perl
      แต่ถ้ามองจากกฎการสเกล คุณค่าของไลบรารีใหญ่สำหรับผู้ใช้ส่วนมากอาจเพิ่มขึ้นเพียงระดับลอการิทึมตามขนาดเท่านั้น
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      ช่วงแรกความห่างนี้อาจดูเหมือนไล่ไม่ทัน แต่ถึงไม่ต้องตามทันด้านขนาด พอถึงจุดหนึ่งความใช้งานง่ายก็จะสำคัญกว่า
      ยิ่งไปกว่านั้น การพอร์ตไลบรารีคณิตศาสตร์ เป็นงานที่เหมาะกับ LLM มากด้วย ต้นทางถูกตรวจสอบแล้ว เป้าหมายก็ตรวจสอบได้ และเส้นทางการให้เหตุผลส่วนใหญ่ก็ย้ายตามได้
      ถ้ามองอีกด้าน LLM ยังทำให้อุปสรรคของการทำงานบนแพลตฟอร์มเล็กต่ำลงกว่าที่คาด ถ้าฉันย้ายไลบรารีฝั่งนั้นมาที่แพลตฟอร์มของฉันได้ ก็มีโอกาสสูงว่าฉันจะย้าย proof ของฉันไปฝั่งนั้นได้ด้วย
    • กลับกัน มันดูเหมือนเป็นสัญญาณว่าชุมชนเติบโตเต็มที่พอจะเริ่มทำ งานจริง แล้วมากกว่า
      ประเด็นสำคัญไม่ใช่เครื่องมือที่สมบูรณ์แบบ แต่คือการทำงานให้สำเร็จด้วยเครื่องมือที่ดีพอ
    • Agda อาจดีกว่าในฐานะ proof checker แต่ไม่น่าใช่ตัวเลือกเชิงปฏิบัติสำหรับการสร้างซอฟต์แวร์
      Lean ดูมีพื้นที่ให้เติบโตเป็นภาษาฟังก์ชันสำหรับพัฒนาซอฟต์แวร์ได้จริง ถึงขั้นอาจเป็น ผู้สืบทอดของ Haskell ได้เลย
    • ฉันเคยใช้ Agda มาบ้าง และใช้ Lean มากกว่านั้นอีกหน่อย การเขียน โปรแกรมฟังก์ชันทั่วไปมากกว่าพิสูจน์คณิตศาสตร์ ใน Lean ง่ายกว่ามาก
      ความต่างหลักน่าจะมาจาก การรองรับด้านเครื่องมือ เอกสารของ Agda ค่อนข้างอ่อน การติดตั้งให้ระบบใช้งานได้ก็ยุ่งยาก และแทบจะบังคับกลาย ๆ ให้ใช้ Emacs
      ส่วน Lean มีแม้กระทั่งวิธีเขียน utility cat อยู่ในเอกสารของตัวเอง และโดยรวมให้ประสบการณ์ tooling ที่ทันสมัยกว่ามาก
    • อยากรู้ว่าในการเขียนโปรแกรมเชิงฟังก์ชัน Agda ดีกว่าตรงไหนกันแน่
      ปกติคำชมมักไปอยู่ที่ dependent pattern matching และในจุดนั้น Lean ก็ดูอ่อนอยู่พอควร
      แต่ถ้ารู้สึกว่า Agda เป็นมิตรกับ FP ทั่วไปมากกว่าด้วย ก็อยากฟังว่าเพราะอะไร

  • Isabelle/HOL ตัวภาษาเองก็โอเค แต่ฝั่ง tooling มีข้อบกพร่องลึก ๆ ที่มากกว่าแค่แนวคิดแบบเดสก์ท็อปเป็นศูนย์กลาง
    ภาษาไม่ได้ดีกว่า Lean อย่างชัดเจน เพียงแต่ต่างกัน และฉันก็เห็นด้วยกับคำวิจารณ์บางส่วนเรื่อง dependent types
    ท้ายที่สุด ทั้งสองภาษาเลือก trade-off คนละแบบ และการเลือกนั้นก็ดูทำให้แต่ละตัวเป็นเครื่องมือที่มีประสิทธิภาพพอตัวในขอบเขตของมัน เพราะโลกของ proof กว้างมาก แต่ละกระบวนทัศน์จึงมีจุดแข็งจุดอ่อนต่างกัน และ Lean ก็แค่เชี่ยวชาญกับอีกส่วนหนึ่งของพื้นที่นั้น
    Sledgehammer นั้นดี แต่ดูเหมือน Lean เองก็คงจะมีของคล้ายกันในไม่ช้า
    ในช่วงสำรวจโจทย์มันอาจมีประโยชน์ แต่ก็ใช้ทรัพยากรมาก และแม้จะช่วยให้ proof สั้นลง ฉันก็ยังชอบให้ ทุกขั้นของ proof ปรากฏออกมาเองในโค้ดสาธารณะ มากกว่าประโยคกึ่งเวทมนตร์อย่าง by sledgehammer
    ตรงกันข้าม งานพัฒนา Isabelle เองกลับเจ็บปวดกว่า Lean มาก โดยเฉพาะเวลาต้องสื่อสารกับนักพัฒนา
    ท่าทีบน mailing list แบบ ไม่มีบั๊ก มีแต่พฤติกรรมที่คุณไม่คาดคิด ดูเด็กและไม่เป็นมืออาชีพ
    และการล้อเลียนการใช้ RAM ของระบบคล้าย Lean ก็ดูตลกดี เมื่อมองจาก ความตะกละหน่วยความจำ ของฝั่ง Isabelle เอง

    • ปัญหาตรงนี้คือการทำ ใบรับรอง UNSAT ให้อยู่ในรูปแบบที่ตรวจได้เร็ว ไม่ใช่เรื่องเล็กน้อยเลย
      ในทางปฏิบัติมันยากพอ ๆ กับการใช้ formal proof เองนั่นแหละ
    • เท่าที่จำได้ตอนเช็กล่าสุด Isabelle/HOL ใช้ custom Emacs mode เป็นอินเทอร์เฟซ
      หรือฉันอาจจำสลับกับ HOL ตัวอื่นก็ได้
    • ฉันไม่รู้ว่า Sledgehammer คืออะไร แต่จากคำอธิบายมันฟังดูแทบเหมือนกับ grind ของ Mathlib เลย
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • สิ่งที่น่าสนใจใน Lean คือ Lean เป็นภาษา แต่สิ่งที่คนพูดถึงกันเป็นหลักจริง ๆ กลับเป็นไลบรารีชื่อ Mathlib
    คนทำ Mathlib ดูค่อนข้างปฏิบัตินิยม เลยเหมือนพวกเขาใส่ classical logic ลงไปใน type ของ Lean และใช้ intuitionistic logic แค่บางส่วน

    • ตัวอย่างที่ยกมาเพื่ออธิบาย กฎตัดสินเป็นกลาง นั้นผิด
      ประโยคว่า “สิ่งใดสิ่งหนึ่งไม่อาจทั้งจริงและเท็จพร้อมกันได้” ไม่ใช่กฎตัดสินเป็นกลาง แต่คือ กฎไม่ขัดแย้งกันเอง
      กฎตัดสินเป็นกลางหมายถึง p เป็นจริง หรือ not p เป็นจริง
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • ฝั่งวิทยาการคอมพิวเตอร์ตอนนี้กำลังสร้าง CSLib ของตัวเองแล้ว
      https://www.cslib.io https://www.github.com/leanprover/cslib
      intuitionistic logic มีความหมายโดยเนื้อแท้ตรงที่พยายามเปลี่ยนข้อโต้แย้งทางคณิตศาสตร์ให้เป็น สิ่งประกอบที่คำนวณได้ จึงน่าสนใจว่าจะจัดการประเด็นนี้อย่างไร
      ที่จริง พอเขียนอัลกอริทึมด้วย Lean คุณก็เข้าสู่ข้อจำกัดเชิงโครงสร้างแบบหนึ่งอยู่แล้วไม่ทางใดก็ทางหนึ่ง และสำหรับเป้าหมายนั้น ตรรกะแค่นั้นก็อาจเพียงพอ
    • ทำให้นึกถึงมุก 5 ขั้นของการยอมรับคณิตศาสตร์เชิงโครงสร้าง
      ปฏิเสธ โกรธ ต่อรอง ซึมเศร้า ยอมรับ
      บรรยายและบทความที่เกี่ยวข้องของ Andrej Bauer ก็น่าดูเช่นกัน
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • สิ่งที่พูดถึงตรงนี้ไม่ใช่ intuitive logic แต่ควรเป็น intuitionistic logic
    • ทั้งที่มีข้อจำกัดและทางตันเยอะขนาดนั้น ก็ยังสงสัยอยู่ดีว่าเมื่อไรและเพราะอะไรคนถึงจะเลือก intuitionistic logic

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

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

  • การถกเถียงแบบนี้ให้ความรู้สึกคล้ายบทความที่ชี้ ข้อจำกัดของ Python ในงานวิทยาศาสตร์คำนวณ
    เมื่อชุมชนก่อตัวรอบเครื่องมือที่ดีพอในระดับหนึ่งจนถึงจุดมวลวิกฤต มันก็จะกลบปัจจัยอื่นแทบทั้งหมด
    แรงส่งจะเกิดขึ้น แล้ว tutorial บทอธิบาย และเอกสารที่ดีขึ้นก็จะสะสมจนแทบถึง ความเร็วหลุดพ้น
    Lean ดูเหมือนอยู่ตรงจุดนั้นพอดี โดยมีผู้สนับสนุนทรงอิทธิพลอย่าง Terrance Tao ด้วย
    ดังนั้นคำพูดว่า “ภาษา X ดีกว่า” อาจไม่ผิดเสียทีเดียว แต่ก็ทำให้พลาดคำถามที่สำคัญจริงได้ง่าย
    แก่นคือมัน ดีกว่าจริงหรือไม่ เมื่อเทียบกับเครื่องมือที่ทุกคนรู้จัก ใช้ได้ทันที และมีเวลาจำนวนมากเทลงไปเพื่อพัฒนา
    สุดท้ายมันดูคล้ายสถานการณ์แบบ worse is better หรือไม่ก็ถ้าดีและนิยมมากพอ แค่นั้นก็เพียงพอแล้ว

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

  • ประโยคที่ว่า “เกือบทุกอย่างที่วันนี้ถูก formalize ด้วยระบบสมัยใหม่ น่าจะ formalize ได้ด้วย AUTOMATH เช่นกัน” ก็คล้ายกับการบอกว่าสิ่งที่เราเขียนด้วยภาษาสมัยใหม่ทุกวันนี้ เมื่อ 50 ปีก่อนก็เขียนด้วย assembly ได้ทั้งหมด
    ในเชิงเทคนิคอาจจริง แต่ในเชิงเศรษฐศาสตร์ต่างกันสิ้นเชิง

    • ภาษา assembly โดยทั่วไป Turing-complete แต่ฝั่ง proof engine นั้นยังไม่แน่ใจว่าการเปรียบเทียบที่สมนัยกันจริง ๆ ควรเป็นอะไร

  • เมื่อราว 15 ปีก่อน ฉันเคยพยายามลอง Coq/Rocq และเครื่องมืออื่นอีกบางตัว แต่กลับพบว่ายากจะเข้าใจตัวซอฟต์แวร์เอง มากกว่าจะเป็นเรื่องแนวคิด
    เรื่องแปลกของ proof assistant / interactive theorem prover คือความเป็น interactive ทำให้มันกลายเป็นการผูกกันระหว่างภาษาและ IDE และในทางปฏิบัติก็เกี่ยวพันกันแน่นมาก
    เพราะอย่างนั้นจึงยากจะพูดถึงแค่ภาษาอย่างเดียว และต้องดูด้วยว่าใช้งานในสภาพแวดล้อมแบบไหน
    ฉันเองก็ไม่ใช่แฟนพันธุ์แท้ของ VS Code แต่ก็ชัดเจนว่า IDE แบบขยายได้ ที่มีคนใช้มหาศาล มีเงินมหาศาลลงไป และถูกขัดเกลามาอย่างดีนั้น ล้ำกว่าสภาพแวดล้อมของตัวเลือกอื่นอย่างมาก
    ทางเข้าที่ดีเยี่ยมอย่าง Natural Numbers Game ก็ดูเป็นสิ่งที่เกิดขึ้นได้เพราะความ hack ได้และ ecosystem ของ VS Code
    แต่สิ่งที่กังวลระหว่างเรียน Lean คือ ความสามารถในการขยายไวยากรณ์ นั้นเป็นดาบสองคม
    พอเรียนภาษานั้นได้แล้ว คุณก็ย่อมอยากอ่านโค้ดที่เขียนด้วยภาษานั้น แต่ถ้าแต่ละโปรเจกต์เริ่มสร้าง DSL ของตัวเองกันเต็มไปหมด มันก็อาจควบคุมไม่อยู่
    สุดท้ายเรื่องนี้ขึ้นอยู่กับว่าชุมชนและ ecosystem จะรู้จักยับยั้งชั่งใจแค่ไหน ซึ่งทำให้ฉันมองมันทั้งด้วยความหวังและความกังวล

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