คอมแพเนียน Lean สำหรับ Analysis I

 (terrytao.wordpress.com)
2 คะแนน โดย GN⁺ 2025-06-01 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Terence Tao เริ่มต้นรีโพซิทอรีคอมแพเนียนที่ย้ายคำนิยาม ทฤษฎีบท และโจทย์แบบฝึกหัดจากหนังสือ Analysis I มาเป็นโค้ด Lean
  • ด้วยลักษณะของหนังสือที่จัดการการสร้างจำนวนธรรมชาติ จำนวนเต็ม จำนวนตรรกยะ และจำนวนจริง รวมถึงทฤษฎีเซตและตรรกะอย่างเคร่งครัด จึงมีโครงสร้างที่เหมาะกับการเรียนรู้ผ่าน proof assistant
  • ขอบเขตปัจจุบันครอบคลุมบางส่วนของบทที่ 2, ทฤษฎีเซตพื้นฐานใน 3.1 และ จำนวนเต็ม ใน 4.1 พร้อมทั้งมีไอโซมอร์ฟิซึมกับจำนวนธรรมชาติของ Mathlib
  • โค้ดสามารถคอมไพล์ใน Lean ได้ แต่ยังมี sorry อยู่จำนวนมาก และแนะนำให้เติมคำตอบลงในฟอร์กแทนการโฮสต์เฉลยทางการ
  • เอกสารชุดนี้เป็นทั้งเส้นทางทางเลือกสำหรับการทำโจทย์แบบฝึกหัดใน Lean และยังใช้เป็นสื่อเริ่มต้นเพื่อค่อย ๆ เรียนรู้การใช้ Mathlib ในบทหลัง ๆ ได้

โปรเจกต์ย้าย Analysis I ไปเป็น Lean

  • Lean companion to “Analysis I” เป็นโปรเจกต์ที่ “แปล” คำนิยาม ทฤษฎีบท และโจทย์แบบฝึกหัดหลายส่วนของ Analysis I ไปเป็น Lean
  • โจทย์แบบฝึกหัดในหนังสือสามารถแก้ได้ด้วยการเติม sorry ที่สอดคล้องกันในโค้ด Lean
  • มีแผนว่าจะไม่โฮสต์เฉลยแบบฝึกหัดอย่างเป็นทางการไว้ในคอมแพเนียน และสามารถสร้างเวอร์ชันที่เติม sorry แล้วเป็นฟอร์กของรีโพซิทอรีได้

ทำไมหนังสือกับ Lean จึงเข้ากันได้ดี

  • Analysis I เป็นหนังสือที่มุ่งเน้นประเด็นพื้นฐานมากขึ้น เพื่อเสริมตำราการวิเคราะห์จริงแบบเดิม
    • การสร้างจำนวนธรรมชาติ จำนวนเต็ม จำนวนตรรกยะ และจำนวนจริง
    • ทฤษฎีเซตและตรรกะที่ช่วยให้พัฒนาบทพิสูจน์ที่มีความเคร่งครัดสูงได้
  • ตอนเขียนหนังสือมี proof assistant อย่าง Coq และ Agda อยู่แล้ว แต่การพิสูจน์แบบเป็นทางการไม่ใช่ประเด็นที่ผู้เขียนสนใจในเวลานั้น
  • หลังจากได้สัมผัสการพิสูจน์แบบเป็นทางการ จึงยืนยันได้ว่าเนื้อหาในหนังสือ เข้ากับ proof assistant ได้ดี
  • ทฤษฎีชนิดแบบไร้พิธีการ ที่ใช้โดยนัยในการสร้างระบบจำนวนมาตรฐานในหนังสือ เข้ากันได้ดีกับ dependent type theory ของ Lean
  • การรองรับ quotient type ของ Lean ก็สอดคล้องกับวิธีการสร้างในหนังสือเช่นกัน

ขอบเขตที่ย้ายมาเป็น Lean แล้วในปัจจุบัน

ความสัมพันธ์กับ Mathlib

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

วิธีใช้งานและสถานะการตรวจสอบ

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

บทบาทในฐานะสื่อเริ่มต้นสำหรับ Lean และ Mathlib

  • คอมแพเนียนนี้สามารถใช้เป็นสื่อเริ่มต้นสำหรับ Lean และ Mathlib ได้ ไม่ใช่แค่สำหรับการวิเคราะห์จริงเท่านั้น
  • ในแง่นี้มีลักษณะคล้ายกับ Natural number game อยู่พอสมควร
  • Natural number game มีเนื้อหาทับซ้อนเชิงหัวข้อกับบทที่ 2 ของ Analysis I อยู่มาก

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

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

 
GN⁺ 2025-06-01
ความคิดเห็นจาก Hacker News

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

    • เห็นด้วยเกือบทั้งหมด แต่ก็น่าคิดว่าการเรียนรู้การพิสูจน์อาจขาด การคิดช้าๆ ไป
      การเรียนคณิตศาสตร์สมัยก่อนมีเวลาจำนวนมากในการนั่งครุ่นคิดกับโจทย์ ลองนั่นลองนี่บนกระดาษ และกระบวนการนั้นบางครั้งก็นำไปสู่การซึมซับแนวคิดและไอเดียใหม่ๆ
      พอใช้ Lean อาจกลายเป็นการลองแบบส่งเดช ตรวจแบบสุ่ม และเททุกอย่างออกมาเสียมากกว่าไหม ตอนที่เคยลองจับ Coq อยู่ไม่กี่ครั้ง ความทรงจำหลักๆ ก็คือการลองปรับโน่นนี่ไปเรื่อยๆ
    • Acorn ทำงานแบบนั้นอยู่แล้ว เมื่อพิสูจน์ไม่สำเร็จแต่ “เกือบถูก” มันจะแสดงข้อเสนอแนะใน VS Code เช่น
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      ไม่ได้ใช้ LLM แต่มีโมเดลโลคัลขนาดเล็กทำงานอยู่ในส่วนขยาย VS Code หวังว่าสักวันโมเดลโลคัลขนาดเล็กนั้นจะแข็งแกร่งจนเหนือกว่ามนุษย์มากๆ รายละเอียดเพิ่มเติมอยู่ที่ https://acornprover.org/docs/tutorial/proving-a-theorem/

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

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

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

    • ไม่แปลกใจถ้าการพิสูจน์ด้านภาษาโปรแกรมจะง่ายกว่าในฐานะเนื้อหาเริ่มต้น อย่างที่หลายคนพูดกัน มันดูมี ขั้นตอนที่เป็นแบบแผน มากกว่ามาก
      ทำอุปนัยเชิงโครงสร้าง ใช้สมมติฐานอุปนัยเพื่อแสดงว่าอินวาเรียนต์ยังคงอยู่ แล้วก็เดินหน้าต่อไปในทำนองนั้น
      ผมไม่ได้ทำการพิสูจน์ทฤษฎีบทมามากนัก และก็ยังไม่เคยทำพิสูจน์แบบ “คณิตศาสตร์” อย่างแคลคูลัสเชิงวิเคราะห์ด้วย proof assistant แต่ถ้าการพิสูจน์ทางคณิตศาสตร์ต้องใช้วิธีเข้าหาที่ต่างกันมาก ก็สงสัยว่าทักษะระหว่างสองฝั่งจะถ่ายโอนกันได้แค่ไหน
      ขอพูดถึง Software Foundations ของ Rocq ด้วย อาจมีพอร์ตไป Lean แล้วก็ได้ แต่ตอนลองตามช่วงต้นๆ ไป รู้สึกค่อนข้างลื่นไหลดี

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

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

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

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

    • ตรวจดูเองได้เลย บทส่วนใหญ่ที่ว่าด้วยลิมิตของลำดับจำนวนจริงเปิดเป็นหน้าตัวอย่างไว้แล้ว
      https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

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

  • ดีจังที่มีตำรา Lean แต่ทำไมถึงไม่มี HoTT ล่ะ?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    แหล่งข้อมูล Lean เพิ่มเติมที่ขึ้น HN ในสัปดาห์นี้:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • การ formalize แนวคิดหลายอย่างของ HoTT ตอนนี้กำลังดำเนินอยู่ในคอมมูนิตี้ Agda https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      แรงจูงใจที่แน่ชัดอยู่นอกสาขาของผมเลยไม่รู้ แต่ดูเหมือน Agda จะเป็นวิธีที่ดีกว่า Lean สำหรับการ formalize แนวคิดเหล่านั้น
      ช่วงปลายปีนี้ยังมีกำหนดออกตำราใหม่ที่เป็นการอัปเดตให้ทันสมัยกว่าเดิมของหนังสือ HoTT เล่มเดิมด้วย และก็มีการ formalize ด้วย Agda ด้วย
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT เป็นหัวข้อที่เทคนิคสูงมากและแคบมาก ดังนั้นการทำโปรเจกต์ทะเยอทะยานสองอย่างพร้อมกันแบบนี้จึงไม่สมเหตุสมผล
      HoTT ยังไม่ได้ใกล้เคียงเลยที่จะถูกยอมรับเป็นมาตรฐานที่สมเหตุสมผล และสำหรับคนส่วนใหญ่ก็เป็นหัวข้อที่ติดขัดตั้งแต่เริ่ม
      คล้ายกับการถามนักพัฒนา JavaScript framework ว่าทำไมไม่ทำ framework สำหรับ Elm หรือ Haskell
    • ผมก็ไม่รู้ว่าทำไมต้องมี HoTT ด้วย
      งานที่ลงไปเพื่อทำให้เครื่องพิสูจน์ทฤษฎีบท HoTT ใช้งานสะดวกนั้นน้อยกว่ามาก และเอกสารก็ด้อยกว่ามาก
      ประโยชน์ของ HoTT ก็ไม่ชัดเจน ดูเหมือนจะช่วยลดงานเฉพาะตอนจัดการกับโครงสร้างที่ลึกลับมาก ๆ ใน category theory เท่านั้น
    • คำถามว่า “ทำไมไม่มี HoTT” ฟังดูแปลกอยู่
      Terrence Tao มีตำรา analysis อยู่หลายเล่ม และนี่คือเอกสารประกอบใน Lean สำหรับหนังสือเล่มแรกของเขา เขาไม่ได้มีตำรา type theory ดังนั้นจึงไม่มี higher type theory ตั้งแต่แรกสิ่งที่ตั้งใจจะทำก็คนละเรื่องกันโดยสิ้นเชิง
    • แค่ข้อเท็จจริงที่ว่านี่เป็นเอกสารประกอบสำหรับตำราที่มีอยู่แล้ว ก็เป็นคำตอบของ “ทำไมไม่ใช่ HoTT” ได้แล้ว อีกเหตุผลหนึ่งอาจเป็นเพราะผู้คนสงสัยคุณค่าทางการศึกษาของมัน

  • เจ๋งมาก Analysis I เป็นตำรา “คณิตศาสตร์จริง ๆ” เล่มแรกที่ผมซึ่งเป็นวิศวกร ไม่ใช่นักคณิตศาสตร์ รู้สึกว่าสามารถตามและแก้โจทย์ไปได้จนจบ หลังจากลองหนังสือเล่มอื่น ๆ อย่าง Rudin มาหลายครั้ง
    หวังว่าเอกสารประกอบ Lean จะทำให้คนที่คุ้นกับคณิตศาสตร์และการเขียนโปรแกรม และอยากเรียนอย่างเข้มงวด เข้าถึงได้ง่ายขึ้น

  • ในช่วงไม่กี่ปีที่ผ่านมา มีความพยายามอย่างต่อเนื่องที่จะ formalize หนังสือ Analysis I ของ Tao ด้วย Lean และก็มีคนที่พยายามทำสิ่งเดียวกันกับที่ Tao กำลังทำอยู่พอดี น่าเสียดายที่ส่วนใหญ่ไปได้ไม่เกินไม่กี่บทแรก แต่หวังว่า Tao จะไปได้ไกลกว่านั้น
    ผมเองก็เคยคิดว่าจะลองทำดูเหมือนกัน เพราะถ้านำ proof ที่ formalize แล้วของแบบฝึกหัดแต่ละข้อไปแนบไว้ในบล็อกคำอธิบาย Analysis I ของผม https://taoanalysis.wordpress.com/ ก็น่าจะเป็นประโยชน์กับคนที่อ่านตามหนังสือ
    ผมโพสต์ไว้ใน Discord server แบบปิดของหนังสือแล้ว แต่เห็นว่าน่าจะมีประโยชน์ที่นี่ด้วย จึงขอแชร์แหล่งข้อมูลที่เกี่ยวข้อง
    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 จึงมีเนื้อหาใกล้เคียงกับบทที่ 2 มาก
    https://github.com/djvelleman/STG4/ — เป็นเกมทฤษฎีเซตบน Lean4 จึงอาจใกล้เคียงกับบทที่ 3 อย่างไรก็ตาม ใน https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean เห็นว่ามี import Mathlib.Data.Set.Basic ดังนั้นดูเหมือนจะนำเซตของ Lean มาใช้ แทนที่จะนิยามเซตขึ้นใหม่และตั้งสัจพจน์เอง แนวทางนี้อาจทำให้ 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 — แสดงวิธีหนึ่งในการนิยาม type Set แบบกำหนดเอง