คู่มือประกอบ Analysis I ใน Lean

• โปรเจกต์ที่ย้ายเนื้อหาหลักของ Analysis I หนังสือวิเคราะห์จริง ที่เขียนโดยเทอเรนซ์ เทา ไปอยู่ในตัวช่วยพิสูจน์ Lean
• โปรเจกต์นี้มีโครงสร้างที่สอดคล้องอย่างมากกับเป้าหมายของหนังสือต้นฉบับที่เน้นความเข้มงวด เช่น การสร้างระบบจำนวนพื้นฐาน และตรรกะของการพิสูจน์
• ใช้ไลบรารีมาตรฐาน Mathlib แต่ก็มีส่วนที่ให้ สร้างแนวคิดสำคัญขึ้นเองและฝึกให้ผู้อ่านพิสูจน์ด้วยตนเอง
• สามารถฝึกโดยเติม ช่องว่าง (sorry) ในโค้ด Lean ด้วยตัวเองได้ ไม่มีเฉลยทางการให้ แต่สามารถ fork ไปต่อยอดได้
• เป็นโอกาสที่มีประโยชน์สำหรับ ทั้งผู้เริ่มต้น Lean และผู้เรียนวิเคราะห์จริง ในการสัมผัสการใช้งาน Mathlib และ Lean จริง

---

ภาพรวม

• โปรเจกต์โอเพนซอร์สที่นำหนังสือวิเคราะห์จริง "Analysis I" ของเทอเรนซ์ เทา มาปรับโครงใหม่ด้วย เครื่องมือช่วยพิสูจน์ Lean
• หนังสือเล่มนี้ให้ความสำคัญกับ กระบวนการสร้างจำนวนธรรมชาติ จำนวนเต็ม จำนวนตรรกยะ และจำนวนจริง รวมถึงเครื่องมือด้านทฤษฎีเซตและตรรกะที่จำเป็น มากกว่าหนังสือวิเคราะห์เล่มอื่น ๆ ที่มีอยู่เดิม
• เนื้อหาในหนังสือจำนวนมากมุ่งพัฒนา ความสามารถในการพิสูจน์อย่างเข้มงวดอย่างเป็นระบบ จึงมีโครงสร้างที่เข้ากันได้ดีกับตัวช่วยพิสูจน์อย่าง Lean

จุดเด่นของโปรเจกต์คู่มือประกอบ Lean

• นำบทนิยาม ทฤษฎีบท และแบบฝึกหัดจากหนังสือต้นฉบับมา "แปล" ให้อยู่ในรูปแบบ Lean
• ในไฟล์ Lean เหล่านี้มี ช่องว่าง (sorry) ที่สอดคล้องกับคำตอบของแบบฝึกหัดอยู่จำนวนมาก ทำให้ผู้อ่านเรียนรู้ได้ด้วยการเติมด้วยตนเอง
• ไม่มีคำอธิบายเฉลยอย่างเป็นทางการให้ แต่ผู้อ่านสามารถ fork รีโพซิทอรีเพื่อสร้างเวอร์ชันคำตอบของตนเองได้

ความเชื่อมโยงและความแตกต่างจาก Mathlib

• แนวคิดบางอย่างที่มีอยู่แล้วใน Mathlib (ไลบรารีคณิตศาสตร์มาตรฐานของ Lean) เช่น จำนวนธรรมชาติ ถูกตั้งใจให้สร้างขึ้นเองแยกต่างหาก และต่อจากนั้นยังมีขั้นตอน พิสูจน์ความเป็นไอโซมอร์ฟิซึม (ความสมมูล) กับเวอร์ชันของ Mathlib ด้วย
• ตัวอย่างเช่น ใน Chapter2.Nat จะเริ่มจากการสร้าง natural numbers ที่นิยามขึ้นเองซึ่งแยกจากจำนวนธรรมชาติของ Mathlib ตั้งแต่ต้น จัดการผลลัพธ์สำคัญด้วยตัวเอง แล้วจึงให้ฝึกใน Lean ว่าทั้งสองเวอร์ชันเทียบเท่ากัน
• ตั้งแต่บทถัด ๆ ไป จะค่อย ๆ ใช้นิยามและฟังก์ชันของ Mathlib มากขึ้นตามลำดับ

วิธีเรียนรู้และการนำไปใช้

• คู่มือประกอบ Lean นี้ไม่ได้มีประโยชน์แค่กับการเรียนวิเคราะห์เท่านั้น แต่ยังทำหน้าที่เป็น บทนำสู่การทำให้คณิตศาสตร์เป็นทางการใน Lean และ Mathlib ด้วย
• มีแบบฝึกที่มีโครงสร้างคล้าย "Natural number game" ซึ่งเปิดโอกาสให้กำหนดนิยามวัตถุทางคณิตศาสตร์และฝึกใช้งานโดยตรงในสภาพแวดล้อมของ Lean
• ตัวโค้ดสามารถคอมไพล์ใน Lean ได้ แต่ยังไม่ได้มีการตรวจยืนยันอย่างสมบูรณ์ว่าแบบฝึกหัดทั้งหมด (sorry) สามารถแก้ได้จริงหรือไม่ จึงยังต้องการการทดสอบใช้งานและข้อเสนอแนะ

โอเพนซอร์สและการมีส่วนร่วม

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

[GN⁺]

ความคิดเห็นบน Hacker News

• ฉันตื่นเต้นมาก และคิดว่าถ้าโปรเจ็กต์นี้ถูกย้ายไปเป็น repo แยกอิสระ ก็น่าจะแชร์และค้นหาได้ง่ายขึ้นสำหรับคนอื่น ๆ ฉันสงสัยเรื่องคณิตศาสตร์มาตลอด และ Analysis ของ Tao เป็นตำราเล่มแรกที่ทำให้ฉันเห็นว่าคณิตศาสตร์ถูกประกอบขึ้นอย่างเข้มงวดอย่างไรในแบบที่เข้ากับวิธีคิดเชิงโปรแกรมของฉัน หลังจากนั้นฉันก็เริ่มสนใจ Lean ด้วย แต่รู้สึกว่า Mathlib ค่อนข้างซับซ้อนถ้าจะใช้เรียนแนวคิดทางคณิตศาสตร์ ดังนั้นฉันจึงชอบโปรเจ็กต์นี้มาก เพราะมันทำหน้าที่เป็นสะพานจากหนังสือไปสู่เครื่องมือ

  • ฉันก็มีประสบการณ์คล้ายกัน ได้เรียนเรื่องลิมิต, ลำดับโคชี ฯลฯ และยังจำได้ว่าหนังสือเล่มนี้ตีพิมพ์โดยสำนักพิมพ์ไม่แสวงหากำไรชื่อ Hindustan Book Agency ในอินเดีย ทำให้หาซื้อได้ในราคาถูกมาก

• สิ่งที่น่าตื่นเต้นที่สุดสำหรับฉันเกี่ยวกับการสอนคณิตศาสตร์ด้วย Lean คือมันให้ feedback ได้ทันที ถ้านักเรียนพิสูจน์ผิด มันก็จะคอมไพล์ไม่ผ่าน แต่ก่อนต้องให้ TA หรืออาจารย์เป็นคนตรวจและให้ feedback เอง ตอนนี้ Lean compiler บอกได้อย่างรวดเร็ว หวังว่าในอนาคตมันจะมีฟีเจอร์เสนอแนะแนวทางแก้แบบเป็นมิตรเหมือน Rust compiler ด้วย (ซึ่งอาจต้องใช้ LLM เฉพาะทาง)

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

• มีคนเล่าว่า Terence Tao มีช่อง YouTube ส่วนตัวที่ดูเขาใช้ Lean ได้โดยตรง ฉันไม่ใช่ผู้เชี่ยวชาญด้านนี้ แต่แค่ได้ดูเขาทำงานทั้งแบบใช้และไม่ใช้ LLM ก็น่าสนใจมากแล้ว (https://www.youtube.com/@TerenceTao27)

• ฉันคิดว่าน่าสนใจมากถ้าจะลองเปรียบเทียบและประเมินแนวทางแบบ "ตำราเรียนดั้งเดิม" กับแนวทางของ Mathlib ไลบรารีคณิตศาสตร์ที่ formalized แล้วมักมีข้อดีตรงที่พยายามแสดงผลลัพธ์ให้อยู่ในรูปที่ general ที่สุด และยัง refactor โครงสร้างของบทพิสูจน์ให้ elegant ขึ้นได้ง่าย การ refactor ทำได้สะดวกเพราะระบบติดตาม logical dependency ให้อยู่เสมอ แต่ถ้าใช้แค่กระดาษกับปากกาจะไม่ง่ายแบบนั้น ดังนั้นจึงเป็นคำถามที่สมเหตุสมผลว่าการสอนแคลคูลัสหรือการวิเคราะห์ในแบบ 'general สูงสุด' อย่าง Mathlib ในชั้นเรียนมหาวิทยาลัยจะเหมาะหรือไม่ และฉันคิดว่าคำถามนี้ก็ใช้ได้กับทุกสาขาคณิตศาสตร์ที่อิงการพิสูจน์เช่นกัน

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

  • ในฐานะนักคณิตศาสตร์ที่เขียนโปรแกรมมานาน ฉันคิดว่าการ formalize แบบโปรแกรมใด ๆ ก็ไม่อาจสร้างความเข้าใจระดับรากฐานได้ อคติของฉันมาจากการที่ฉันเรียนแนวคิดต่าง ๆ ผ่านงานวิจัย โค้ดมักถาโถมในด้านความอ่านยากเพราะไม่ค่อยใส่ใจสไตล์อยู่แล้ว แค่ paper ที่อ่านยากก็เหนื่อยพอแล้ว แต่โค้ดนั้นหนักกว่า 10 เท่าเพราะไม่มีมาตรฐานด้วย ตามประสบการณ์ส่วนตัวของฉัน

• ฉันดีใจที่ theorem proving กำลังได้รับความสนใจมากขึ้นในคณิตศาสตร์กระแสหลักอย่างการวิเคราะห์ ในฝั่ง PLT เคยมีกรณีตัวอย่างเด่นคือหนังสือ The Formal Semantics of Programming Languages ของ Winskel ที่ถูกตรวจพิสูจน์อย่างเป็นทางการด้วย Isabelle แล้ว (http://concrete-semantics.org) ถ้าอยากเริ่มต้น theorem proving ฉันคิดว่าทางนั้นง่ายกว่าและน่าแนะนำมากกว่า และขอเสริมว่าทฤษฎีบทในวิชาวิเคราะห์นั้นเดิมทีก็ยากมากอยู่แล้ว

  • ฉันก็คงไม่แปลกใจถ้าการพิสูจน์ในสาย PL จะมีอุปสรรคเริ่มต้นต่ำกว่า เพราะมักได้ยินว่ามันมีความเป็นงานรูทีนมากกว่า — structural induction, การใช้ induction, การพิสูจน์ invariant, ทำซ้ำไปเรื่อย ๆ ฉันไม่ได้ทำ theorem proving มากนัก และก็ไม่เคยลองพิสูจน์แบบคณิตศาสตร์จริง ๆ (โดยเฉพาะการวิเคราะห์) ด้วย theorem prover เลย เลยสงสัยว่าการพิสูจน์แบบ "คณิตศาสตร์" ต้องใช้วิธีคิดที่ต่างออกไปมากแค่ไหน และทักษะย้ายข้ามกันได้มากน้อยเพียงใด อ้างอิงเพิ่มเติมคือฉันเคยเรียน Software Foundations in Rocq (อาจมีเวอร์ชันพอร์ตไป Lean ด้วย?) และสนุกมากทีเดียว

• ฉันคิดว่าโปรเจ็กต์นี้และแนวทางแบบนี้เหมาะมากกับหัวข้อพื้นฐานอย่างการวิเคราะห์ แต่ก็มีความกังวลอยู่สองข้อ

  1. ผลลัพธ์แกนกลางด้านการวิเคราะห์ของ Mathlib ใช้แนวคิด filter เป็นกรอบรวม ส่วนกรณีพิเศษจึงค่อยจัดการแบบ epsilon-delta แยกต่างหาก ขณะที่ Analysis ของ Tao น่าจะใช้แนวทาง epsilon-delta แบบดั้งเดิมมากกว่า
  2. Mathlib เป็นโปรเจ็กต์ที่เปลี่ยนเร็วมาก ชื่อและโครงสร้างเปลี่ยนอยู่ตลอด ข้อมูลการเชื่อมโยงจึงต้องคอยดูแลรักษาอย่างต่อเนื่อง
  • พร้อมชวนให้ทุกคนไปตรวจดูเองได้ เพราะมีการเปิดเผยเกือบทั้งบทว่าด้วยลิมิตของลำดับเป็นหน้าตัวอย่างอยู่แล้ว จึงแชร์ลิงก์ที่เกี่ยวข้องไว้ https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• ฉันคิดว่าเป็นโปรเจ็กต์ที่ยอดเยี่ยมมาก Analysis I เป็นตำราคณิตศาสตร์ "จริงจัง" เล่มแรกที่ในฐานะวิศวกร ฉันสามารถไล่ตามและเรียนจนจบได้จริง ๆ ก่อนหน้านี้ก็เคยพยายามกับหนังสือเล่มอื่น ๆ (เช่น Rudin) หลายครั้งแล้วล้มเหลว ถ้ามีเวอร์ชัน Lean ก็น่าจะช่วยให้คนที่คุ้นทั้งคณิตศาสตร์และการเขียนโปรแกรมได้เรียนแนวคิดต่าง ๆ อย่างเข้มงวดมากขึ้น

• เป็นความจริงที่ตลอดหลายปีมานี้มีความพยายามทำ formalization ของ Analysis I ของ Tao แบบเป็นทางการใน Lean อยู่เรื่อย ๆ แต่ก็มักไปได้ไม่เกินไม่กี่บท ฉันเองก็เคยอยากลองทำเรื่องนี้เหมือนกันอยู่พักหนึ่ง — ฉันคิดว่าถ้าเอาบทพิสูจน์แบบ formalized ไปลงคู่กับบล็อกเฉลย Analysis I (https://taoanalysis.wordpress.com/) คนที่เรียนจากหนังสือก็น่าจะใช้ประโยชน์ได้มาก ฉันเคยแชร์สิ่งที่รวบรวมไว้ใน Discord ส่วนตัวมาแล้ว แต่ที่นี่จะขอแชร์ลิงก์อ้างอิงโปรเจ็กต์ Lean ต่าง ๆ ที่น่าจะมีประโยชน์สำหรับหลายคนไว้ในที่เดียว (github, gist, เอกสารทางการ ฯลฯ)

  • https://github.com/cruhland/lean4-analysis
  • https://github.com/cruhland/lean4-axiomatic
  • https://github.com/Shaunticlair/tao-analysis-lean-practice
  • https://github.com/vltanh/lean4-analysis-tao
  • https://github.com/gabriel128/analysis_in_lean
  • https://github.com/mk12/analysis-i
  • https://github.com/melembroucarlitos/Tao_Analysis-LEAN
  • https://github.com/leanprover-community/NNG4/ (อันนี้ไม่ใช่หนังสือของ Tao แต่เป็นเวอร์ชัน Lean4 ของ Natural Number Game โดยมีเนื้อหาเกือบตรงกับ Chapter 2)
  • https://github.com/djvelleman/STG4/ (ในทำนองเดียวกัน เป็นเกมทฤษฎีเซต คล้ายกับ Chapter 3 แต่ถ้าดูที่ Game/Metadata.lean จะเห็นว่ามี import Mathlib.Data.Set.Basic จึงเป็นการเรียกใช้ทฤษฎีเซตที่มีอยู่แล้ว ไม่ได้สร้างขึ้นใหม่ทั้งหมด — ในกรณีนี้ Lean จึง "รู้" ทฤษฎีเซตอยู่แล้ว ซึ่งอาจไม่ตรงกับจุดประสงค์ของเราอย่างสมบูรณ์)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (ตัวอย่างการสร้างจำนวนเต็ม)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean (อาจเป็นไฟล์เดียวกับข้างบน)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean (ตัวอย่างการสร้างจำนวนตรรกยะ)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (ตัวอย่างอ้างอิงสำหรับการนิยามชนิด Set แบบกำหนดเอง)

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

  • การพิสูจน์ isomorphism แบบนี้

    1. ช่วยให้พิสูจน์ได้ว่าวัตถุที่คุณสร้างขึ้นกับวัตถุที่มีอยู่แล้วใน Mathlib เหมือนกันจริง โดยเฉพาะเมื่อฝั่ง Mathlib อาจนิยามผ่านโครงสร้างทั่วไปที่ซับซ้อนกว่า จึงช่วยให้เข้าใจความต่างได้
    2. มีบทบาทสำคัญต่อการทำความเข้าใจสัญกรณ์และคำศัพท์ทางการที่ใช้เวลาอ่านหรือเขียนวัตถุนั้นใน Mathlib

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

• ยินดีที่ได้เห็นตำรา Lean-based ปรากฏขึ้น แต่ก็อดสงสัยไม่ได้ว่าทำไมไม่มี HoTT (Homotopy Type Theory)? ยังมีบทความตั้งประเด็นว่า Type Theory(HoTT) ควรมาแทนที่ทฤษฎีเซต (ZFC) หรือไม่ ด้วย (https://news.ycombinator.com/item?id=43196452) และยังแชร์ทรัพยากรชุมชนที่เกี่ยวกับ Lean เพิ่มเติมจาก HN ในสัปดาห์นี้ด้วย — 100 theorems in Lean (https://news.ycombinator.com/item?id=44075061) และโปรเจ็กต์ Lean ของ DeepMind (https://news.ycombinator.com/item?id=44119725)

  • แต่ฉันก็ไม่เห็นเหตุผลว่าทำไมต้องมี HoTT ด้วย theorem prover สำหรับ HoTT ยังใช้งานไม่สะดวกนัก และเอกสารก็ยังไม่เพียงพอ อีกทั้งฉันยังไม่เห็นชัดว่า HoTT ให้ประโยชน์อะไร โดยทั่วไปดูจะมีนัยสำคัญเฉพาะเวลาจัดการโครงสร้างประหลาดมาก ๆ อย่าง category theory เท่านั้น

  • ด้วยความที่นี่เป็นแนวทางแบบตำราเรียนดั้งเดิมอยู่แล้ว คำถามว่า "ทำไมไม่ใช่ HoTT" ก็มีคำตอบอยู่ในตัว และฉันคิดว่ายังมีผู้เชี่ยวชาญจำนวนมากที่กังขาเรื่องประสิทธิผลทางการศึกษาอยู่ด้วย