Lean companion cho Analysis I

• Đây là dự án chuyển các nội dung cốt lõi của giáo trình giải tích thực Analysis I do Terence Tao viết sang trợ lý chứng minh Lean
• Dự án này có cấu trúc rất phù hợp với mục tiêu của nguyên tác là nhấn mạnh tính chặt chẽ, như xây dựng các hệ thống số cơ bản và logic chứng minh
• Dự án tận dụng thư viện chuẩn Mathlib, đồng thời bao gồm cả việc tự xây dựng các khái niệm chính và để người đọc tự luyện chứng minh
• Có thể luyện tập bằng cách tự điền các chỗ trống (sorry) trong mã Lean; không cung cấp lời giải chính thức nhưng có thể mở rộng bằng cách fork
• Hữu ích cho cả người mới học Lean lẫn người học giải tích thực muốn trải nghiệm cách dùng Mathlib và Lean trong thực tế

---

Tổng quan

• Đây là dự án mã nguồn mở tái cấu trúc giáo trình giải tích thực "Analysis I" của Terence Tao bằng công cụ trợ lý chứng minh Lean
• So với nhiều sách giải tích khác, giáo trình này tập trung nhiều hơn vào quá trình xây dựng số tự nhiên, số nguyên, số hữu tỉ và số thực, cùng các công cụ lý thuyết tập hợp và logic cần thiết trong quá trình đó
• Phần lớn nội dung sách tập trung vào việc phát triển năng lực chứng minh chặt chẽ có hệ thống, nên có cấu trúc rất phù hợp với một trợ lý chứng minh như Lean

Đặc điểm của dự án Lean companion

• Cung cấp bản "dịch" các định nghĩa, định lý và bài tập của nguyên tác sang định dạng Lean
• Các tệp Lean này chứa nhiều chỗ trống (sorry) tương ứng với lời giải bài tập, cho phép người đọc học bằng cách tự điền vào
• Không cung cấp lời giải chính thức, nhưng người đọc có thể fork repository để tạo phiên bản đáp án của riêng mình

Liên hệ với Mathlib và điểm khác biệt

• Một số khái niệm đã được cài đặt sẵn trong Mathlib (thư viện toán học chuẩn của Lean), như số tự nhiên, lại được cố ý tự xây dựng riêng trước; sau đó còn có phần chứng minh tính đẳng cấu (tương đương) với phiên bản trong Mathlib
• Ví dụ, trong Chapter2.Nat, dự án xây dựng từ đầu định nghĩa số tự nhiên riêng, tách biệt với số tự nhiên của Mathlib, tự xử lý các kết quả chính, rồi ở phần cuối để người học luyện tập việc chứng minh hai phiên bản là tương đương trong Lean
• Từ các chương sau, dự án dần sử dụng nhiều hơn các định nghĩa và tính năng của Mathlib

Cách học và sử dụng

• Lean companion này không chỉ phục vụ việc học giải tích mà còn đóng vai trò như tài liệu nhập môn về cách hình thức hóa toán học trong Lean và Mathlib
• Có các bài luyện tập có cấu trúc, tương tự "Natural number game", cho phép trực tiếp định nghĩa và thực hành với các đối tượng toán học trong môi trường Lean
• Bản thân mã có thể biên dịch trong Lean, nhưng chưa được kiểm chứng hoàn toàn rằng mọi bài tập (sorry) đều thực sự giải được; vì vậy vẫn cần playtest và phản hồi

Mã nguồn mở và đóng góp

• Repository là mã nguồn mở nên ai cũng có thể tham khảo, fork và đóng góp
• Không cung cấp lời giải chính thức riêng, đồng thời hỗ trợ việc tạo ra nhiều phiên bản lời giải khác nhau
• Tính đến ngày 31 tháng 5, dự án đã được chuyển sang một repository độc lập riêng

[GN⁺]

Bình luận trên Hacker News

• Tôi thực sự rất hào hứng; nếu dự án này được chuyển sang một repo độc lập thì sẽ dễ chia sẻ và dễ tìm hơn cho mọi người. Tôi vốn luôn tò mò về toán học, và Analysis của Tao là giáo trình đầu tiên cho tôi thấy toán học được xây dựng chặt chẽ như thế nào theo cách phù hợp với tư duy lập trình của mình. Sau đó tôi cũng bắt đầu mê Lean, nhưng cảm thấy học các khái niệm toán qua Mathlib hơi phức tạp. Vì vậy tôi rất thích dự án này như một cây cầu nối từ cuốn sách sang công cụ.

  • Tôi cũng có trải nghiệm tương tự; đã học về hội tụ, dãy Cauchy, v.v., và còn nhớ cuốn sách này được xuất bản bởi Hindustan Book Agency, một nhà xuất bản phi lợi nhuận ở Ấn Độ, nên có thể mua với giá rất rẻ.

• Điều khiến tôi hào hứng nhất ở việc dạy toán bằng Lean là khả năng đưa ra phản hồi ngay lập tức: nếu sinh viên viết sai chứng minh thì nó sẽ không biên dịch. Trước đây cần TA hoặc giáo sư trực tiếp phản hồi, còn giờ trình biên dịch Lean có thể báo rất nhanh. Tôi hy vọng sau này nó còn có thể đưa ra gợi ý sửa lỗi thân thiện hơn như trình biên dịch Rust (điều này có thể cần một LLM chuyên dụng).

  • Tôi gần như đồng ý hoàn toàn, nhưng tôi cũng nghĩ quá trình ngồi suy nghĩ về chứng minh là rất quan trọng. Kinh nghiệm học toán của tôi đã lâu, nhưng có rất nhiều khoảng thời gian kiểu “thiên đường toán học” khi tôi chậm rãi suy nghĩ, vừa viết bài tập hay lời giải ra giấy. Tôi lo rằng dùng Lean có thể khiến mọi thứ chuyển sang kiểu “mò tay” nhiều hơn: nhập bừa hoặc thử cho đến khi tự động đúng. Tôi cũng từng dùng Coq một thời gian ngắn, và gần như chỉ toàn thử chỉnh sửa liên tục. Nói ngắn gọn, theorem solver rất hữu ích ở nhiều mặt, nhưng tôi băn khoăn liệu nó có làm mất đi quá trình nghiền ngẫm chậm rãi này, từ đó làm yếu đi con đường dẫn tới sự nội tại hóa, khái niệm hóa và nảy sinh ý tưởng mới hay không. Tôi muốn nghe suy nghĩ của mọi người về điều này.

• Có một kênh YouTube cá nhân nơi có thể xem trực tiếp Terence Tao dùng Lean. Tôi không phải chuyên gia trong lĩnh vực này, nhưng chỉ riêng việc xem ông làm việc cùng hoặc không cùng LLM thôi cũng đã rất thú vị (https://www.youtube.com/@TerenceTao27).

• Tôi nghĩ sẽ rất thú vị nếu đánh giá và so sánh cách tiếp cận “kiểu giáo trình truyền thống” này với phong cách của Mathlib. Các thư viện toán học được hình thức hóa thường có ưu điểm là biểu diễn kết quả theo cách tổng quát nhất có thể, và cũng dễ tái cấu trúc chính bản thân cấu trúc chứng minh để nó thanh nhã hơn. Việc refactor khá dễ vì hệ thống luôn theo dõi các phụ thuộc logic, còn với giấy bút thì không dễ như vậy. Vì thế, tôi nghĩ việc tự nhiên đặt câu hỏi liệu có ổn không khi dạy giải tích theo phiên bản “tổng quát tối đa” như Mathlib trong các khóa đại học là hoàn toàn hợp lý. Và đây cũng là băn khoăn tương tự cho mọi lĩnh vực toán học dựa trên chứng minh khác.

  • Ít nhất ở các khóa nhập môn thì tôi cho là không phù hợp. Chương trình học vốn đã có quá nhiều thứ phải đưa vào — phương pháp chứng minh, cách lập trình, rồi cả lý thuyết nền tảng. Kinh nghiệm của các giáo sư đã thật sự thử làm việc này cũng tương tự: tốt cho sinh viên giỏi, nhưng với sinh viên phổ thông thì thường bị xem là lãng phí thời gian.

  • Là một nhà toán học đã lập trình từ rất lâu, tôi nghĩ không một kiểu hình thức hóa bằng chương trình nào có thể tự nó bồi dưỡng được sự hiểu biết nền tảng. Thành kiến của tôi đến từ việc tôi học khái niệm qua các bài báo. Mã nguồn thường lấn át về mặt đọc hiểu vì ít quan tâm tới văn phong; mà bài báo khó đọc đã đủ mệt rồi, còn với code thì vì chẳng có chuẩn thống nhất nên theo trải nghiệm cá nhân của tôi còn khó hơn gấp mười.

• Tôi rất vui khi thấy theorem proving ngày càng được chú ý trong các nhánh toán học chính thống như giải tích. Trong PLT thì đã có ví dụ tiêu biểu là cuốn The Formal Semantics of Programming Languages của Winskel được kiểm chứng hình thức bằng Isabelle (http://concrete-semantics.org). Nếu ai muốn bắt đầu với theorem proving thì tôi nghĩ hướng đó dễ hơn và đáng để khuyến nghị hơn. Cũng cần nói thêm là các định lý trong giải tích vốn đã khá khó ngay từ đầu.

  • Tôi cũng sẽ không ngạc nhiên nếu chứng minh trong PL có rào cản gia nhập thấp hơn. Tôi thường nghe nói nó có cảm giác mang tính quy trình hơn — quy nạp cấu trúc, áp dụng quy nạp, chứng minh bất biến, lặp lại, v.v. Tôi không làm theorem proving nhiều, nhưng cũng chưa từng thử chứng minh toán học (đặc biệt là giải tích) bằng theorem prover. Tôi tò mò liệu các chứng minh “toán học” có đòi hỏi cách tiếp cận rất khác hay không, và mức độ chuyển giao kỹ năng giữa hai bên sẽ là bao nhiêu. Nhân tiện, tôi đã học qua Software Foundations in Rocq (có thể có bản port sang Lean?) và thấy khá thú vị.

• Tôi nghĩ dự án và cách tiếp cận này rất hợp với các chủ đề nền tảng như giải tích. Tuy vậy tôi có hai lo ngại:

  1. Các kết quả cốt lõi của giải tích trong Mathlib được xử lý một cách thống nhất bằng khái niệm filter, còn các trường hợp đặc biệt thì tách riêng theo kiểu epsilon-delta; tôi đoán Analysis của Tao sẽ dùng cách tiếp cận epsilon-delta truyền thống hơn.
  2. Mathlib là một dự án thay đổi rất nhanh, nên tên gọi và cấu trúc luôn biến động; thông tin liên kết sẽ phải được bảo trì liên tục.
  • Mọi người có thể tự kiểm tra; thực tế là phần lớn chương về giới hạn của dãy số đã được công khai dưới dạng trang mẫu, nên có thể tham khảo ở đây: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• Tôi thấy đây là một dự án rất tuyệt. Analysis I là giáo trình toán “thật sự” đầu tiên mà tôi, với tư cách kỹ sư, có thể thực sự học theo đến cùng; tôi cũng từng nhiều lần thử rồi bỏ dở với các sách khác như Rudin. Nếu có bản Lean thì những người quen cả toán lẫn lập trình có lẽ sẽ học các khái niệm một cách chặt chẽ hơn nhiều.

• Trong nhiều năm đã liên tục có những nỗ lực làm formalization chính thức cho Analysis I của Tao, nhưng lúc nào cũng khó đi xa hơn vài chương. Có thời gian tôi cũng muốn tự làm việc này — tôi nghĩ nếu đăng kèm các chứng minh đã hình thức hóa liên kết với blog lời giải Analysis I (https://taoanalysis.wordpress.com/) thì những người học theo sách sẽ thấy rất hữu ích. Tôi đã từng chia sẻ tài liệu tổng hợp trong một Discord riêng, nhưng ở đây tôi gom lại một loạt liên kết tới các dự án Lean tham khảo có thể hữu ích cho nhiều người (github, gist, tài liệu chính thức, v.v.):

  • 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/ (đây không phải sách của Tao mà là bản Lean4 của trò chơi số tự nhiên, nội dung gần như trùng với Chương 2)
  • https://github.com/djvelleman/STG4/ (tương tự, đây là trò chơi lý thuyết tập hợp, gần với Chương 3; tuy nhiên nếu xem Game/Metadata.lean thì sẽ thấy nó import Mathlib.Data.Set.Basic, tức là không định nghĩa lại lý thuyết tập hợp từ đầu mà dùng bản có sẵn — trong trường hợp này Lean đã “biết” toàn bộ lý thuyết tập hợp, nên có thể không hoàn hảo cho mục đích của chúng ta)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (ví dụ về cách xây dựng số nguyên)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean (có thể là cùng tệp như ở trên)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean (ví dụ về cách xây dựng số hữu tỉ)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (ví dụ tham khảo để định nghĩa kiểu Set tùy biến)

• Tôi tò mò việc “chứng minh đẳng cấu với đối tượng tương ứng trong Mathlib” thực sự quan trọng đến mức nào. Liệu có thể bỏ phần đẳng cấu đi mà về cơ bản cũng không thay đổi gì chăng? Ví dụ, nó có thực sự được dùng cho những việc như dịch định lý tự động hay không?

  • Các chứng minh đẳng cấu như vậy

    1. cho phép bạn chứng minh rằng đối tượng bạn tự xây dựng và đối tượng đã có trong Mathlib thật sự là cùng một thứ, đặc biệt vì phía Mathlib có thể được định nghĩa bằng những cấu trúc tổng quát hóa phức tạp hơn, nên điều này giúp hiểu được sự khác biệt
    2. đóng vai trò quyết định trong việc hiểu ký hiệu và thuật ngữ chính thức được dùng khi đọc hoặc viết về đối tượng đó trong Mathlib

  • Ít nhất thì tôi nghĩ nó có giá trị giáo dục, theo nghĩa đây là quá trình để chính bản thân người học tự xác tín rằng tập hợp và phép toán mình xây dựng quả thật là “cùng một thứ” với thứ xuất hiện ở nơi khác trong cuốn sách.

• Tôi rất vui khi thấy các giáo trình dựa trên Lean xuất hiện, nhưng tại sao lại không có HoTT (Homotopy Type Theory)? Cũng đã có bài thảo luận với chủ đề “Type Theory (HoTT) có nên thay thế lý thuyết tập hợp (ZFC) không?” (https://news.ycombinator.com/item?id=43196452). Cũng xin chia sẻ thêm một số tài nguyên cộng đồng về Lean được đăng trên HN tuần này — “100 theorems in Lean” (https://news.ycombinator.com/item?id=44075061), và dự án Lean của DeepMind (https://news.ycombinator.com/item?id=44119725).

  • Nhưng tôi không thấy có lý do gì nhất thiết phải có HoTT. Các theorem prover cho HoTT hiện vẫn chưa thân thiện với người dùng, tài liệu cũng chưa đủ tốt. Tôi cũng không thấy rõ lợi ích mà HoTT mang lại; theo tôi thì nó thường chỉ thực sự có ý nghĩa khi xử lý những cấu trúc cực kỳ khác thường như trong lý thuyết phạm trù.

  • Vì đây là cách tiếp cận theo kiểu giáo trình truyền thống, nên câu hỏi “tại sao không phải HoTT” thật ra đã tự có câu trả lời rồi. Hơn nữa, tôi nghĩ cũng có khá nhiều chuyên gia hoài nghi về hiệu quả giáo dục của nó.