ทำไมถึงไม่ใช้แค่ Lean

• ประวัติศาสตร์ของการทำให้คณิตศาสตร์เป็นแบบฟอร์มัล ไม่ได้เริ่มต้นที่ Lean และตลอดเกือบ 60 ปีที่ผ่านมา ระบบหลายสายได้สั่งสมเทคนิคหลักและผลงานสำคัญไว้แล้ว
• เครื่องมืออย่าง AUTOMATH ในปี 1968, สาย LCF, HOL, Rocq, ACL2 และ Mizar ได้สร้างงานฟอร์มัลไลซ์อย่างกว้างขวาง ตั้งแต่การวิเคราะห์จริงไปจนถึงทฤษฎีบทจำนวนเฉพาะ ทฤษฎีบทสี่สี และข้อคาดเดาเคปเลอร์
• Lean สร้างนิยามคณิตศาสตร์สมัยใหม่ได้อย่างรวดเร็วด้วยไลบรารีขนาดใหญ่และชุมชนที่คึกคัก แต่ propositions as types หรือ dependent types ก็ไม่ใช่หนทางเดียวของ proof assistant
• Isabelle ชูจุดเด่นเรื่อง ระบบอัตโนมัติที่แข็งแกร่ง ความอ่านง่ายสูง และการหลีกเลี่ยง dependent types พร้อมสืบทอดธรรมเนียม LCF ที่สร้างการตรวจสอบบทพิสูจน์ผ่านกำแพงนามธรรมของเคอร์เนลได้แม้ไม่มี proof object
• เมื่อ AI เข้ามาช่วยจัดระเบียบบทพิสูจน์ที่มีโครงสร้างและ แปล ไปยังระบบอื่น ๆ ได้ ภาระของการมองว่าเครื่องมือใดเครื่องมือหนึ่งเป็นมาตรฐานสัมบูรณ์ก็อาจลดลงอีกในอนาคต

---

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

• AUTOMATH

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

• Boyer และ Moore

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

กระแสหลัง LCF

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

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

• นักคณิตศาสตร์มองว่าความสำเร็จของการฟอร์มัลไลซ์ก่อนหน้านั้นยังไปไม่ถึงโครงสร้างซับซ้อนของคณิตศาสตร์ร่วมสมัยสายหลัก เช่น Grothendieck schemes หรือ perfectoid spaces
• Tom Hales เลือกแนวทางสะสมนิยามเหล่านี้เป็นไลบรารี โดยเน้น การสะสมนิยาม มากกว่าตัวบทพิสูจน์ และเลือกใช้ Lean
• เขานำเสนอแนวทางนี้ในโครงการ Big Proof และมีการพูดคุยแนวคิดคล้ายกันร่วมด้วย
• Kevin Buzzard ได้ฟังแล้วตัดสินใจลองใช้ Lean ในการสอน ทำให้การแพร่หลายหลังจากนั้นรวดเร็วขึ้น
• จุดเปลี่ยนสำคัญของชุมชน Lean ที่ถูกยกขึ้นมาคือ การหลุดออกจาก ความยึดติดกับบทพิสูจน์เชิงสร้างสรรค์ ซึ่งครอบงำ Rocq มาอย่างยาวนาน
• ลัทธิ intuitionism เกิดขึ้นหลัง Russell’s paradox และมีนัยเฉพาะต่อแนวคิดเรื่องจำนวนจริงด้วย
• Martin-Löf type theory เป็นรูปแบบฟอร์มัลนิยมเชิง intuitionism อย่างชัดเจน แต่ผู้เขียนบอกว่า 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 นั้นไม่ตรงกับข้อเท็จจริง
  • บทความเกี่ยวกับ LCF
• Rocq และ Lean มี Prop ซึ่งเป็น sort ของประพจน์ โดย proof object ทั้งหมดของประพจน์เดียวกันจะถูกประเมินเป็นค่าเดียวกัน จึงให้ proof irrelevance
• แต่นั่นไม่ได้ทำให้ proof object ขนาดมหึมาหายไป เพราะในระบบจริงมันยังคงอยู่
• การค้นพบสำคัญของ Robin Milner คือ ใน LCF ไม่จำเป็นต้องมี proof object เลย
• ถ้าใส่ proof kernel ไว้ใน abstract data type ของ ML และใช้นิยามกฎอนุมานเป็นตัวสร้าง ก็จะตรวจสอบบทพิสูจน์แบบไดนามิกได้
• ผู้เขียนมองว่าด้วย abstraction barrier ของ ML จึงไม่สามารถโกงระบบได้
• การที่เทอมขนาดมหึมาซึ่งไม่ได้บ่งบอกอะไรเลยกลับกินพื้นที่หลายสิบ MB ดูยิ่งไม่สมเหตุสมผลในยุค RAMmageddon
• และยังวิจารณ์ต่อว่ามีงานวิจัยที่มุ่งทำให้เทอมที่ไม่จำเป็นเหล่านั้นดูสง่างามขึ้นอีกด้วย

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

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

• ระบบอัตโนมัติ

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

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

  • ถูกจัดให้เป็น ตัวเลือกที่ดีที่สุดด้านความอ่านง่าย โดยอ้างอิง ตัวอย่างเกี่ยวกับ Isar

• การหลีกเลี่ยง 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
  • field extensions
  • p-adic numbers
  • Grothendieck schemes
• แต่ผ่าน งานวิจัย Alexandria เขาได้เรียนรู้อะไรมากมาย และสรุปว่าแก่นสำคัญคือ อย่าพยายามยัดทุกอย่างลงไปเป็นชนิดทั้งหมด

ทิศทางต่อจากนี้และ AI

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

เติมเต็มส่วนที่ขาดไปของ Mizar

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

[GN⁺]

ความคิดเห็นจาก 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 ปริมาณ โค้ดที่มนุษย์เขียนและเปิดเผยสู่สาธารณะ ส่งผลโดยตรงต่อความสามารถของเอเจนต์ในการสร้างโค้ดใหม่ให้ดีขึ้น ซึ่งยิ่งทำให้แรงส่งนั้นแข็งแกร่งกว่าเดิม