Lean companion cho Analysis I
(terrytao.wordpress.com)- Terence Tao đã khởi động một kho lưu trữ companion chuyển các định nghĩa, định lý và bài tập trong giáo trình giải tích thực Analysis I sang mã Lean
- Do đặc thù giáo trình xử lý một cách chặt chẽ việc xây dựng số tự nhiên, số nguyên, số hữu tỉ, số thực cùng lý thuyết tập hợp và logic, tài liệu này có cấu trúc phù hợp để học bằng trợ lý chứng minh
- Phạm vi hiện tại gồm một phần Chương 2, lý thuyết tập hợp cơ bản 3.1 và đến mục 4.1 về số nguyên, bao gồm cả đẳng cấu với số tự nhiên của Mathlib
- Mã biên dịch được trong Lean nhưng vẫn còn nhiều
sorry; tác giả khuyến nghị điền chúng trong các bản fork thay vì cung cấp lời giải chính thức - Tài liệu này có thể được dùng như một lộ trình thay thế để giải bài tập bằng Lean, đồng thời cũng là tài liệu nhập môn để làm quen với việc dùng Mathlib ở các phần về sau
Dự án chuyển Analysis I sang Lean
- Lean companion to “Analysis I” là dự án “dịch” nhiều định nghĩa, định lý và bài tập của Analysis I sang Lean
- Có thể giải các bài tập trong sách bằng cách điền các
sorrytương ứng trong mã Lean - Dự án không có kế hoạch lưu trữ lời giải chính thức cho bài tập trong companion; các phiên bản đã điền
sorrycó thể được tạo dưới dạng fork của kho lưu trữ
Vì sao giáo trình và Lean phù hợp với nhau
- Analysis I là giáo trình tập trung nhiều hơn vào các vấn đề nền tảng nhằm bổ sung cho các giáo trình giải tích thực truyền thống
- Xây dựng số tự nhiên, số nguyên, số hữu tỉ, số thực
- Lý thuyết tập hợp và logic giúp phát triển các chứng minh có độ chặt chẽ cao
- Khi cuốn sách được viết, các trợ lý chứng minh như Coq, Agda đã tồn tại, nhưng kiểm chứng hình thức khi đó không phải là mối quan tâm
- Sau khi trải nghiệm kiểm chứng hình thức, người ta nhận thấy nội dung cuốn sách rất phù hợp với trợ lý chứng minh
- Lý thuyết kiểu ngây thơ được dùng ngầm khi sách xây dựng các hệ số chuẩn phù hợp với lý thuyết kiểu phụ thuộc của Lean
- Hỗ trợ quotient type của Lean cũng khớp với cách xây dựng trong sách
Phạm vi hiện đã được chuyển sang Lean
- Hiện các mục sau đã được dịch sang Lean
Quan hệ với Mathlib
- Phần hình thức hóa được thiết kế để ở một số điểm thì tách khỏi thư viện toán học chuẩn của Lean là Mathlib, còn ở những điểm khác thì phụ thuộc vào Mathlib
- Mathlib đã có sẵn khái niệm số tự nhiên chuẩn
- Trong phần hình thức hóa Lean, trước tiên dự án phát triển
Chapter2.Nat, tức số tự nhiên được xây dựng lại “bằng tay”- Khi làm việc trong namespace
Chapter2, có thể dùng nó dưới tênNat - Thiết lập các kết quả cơ bản song song với các bổ đề liên quan đến số tự nhiên trong Mathlib
- Nhiều chứng minh trong số này được để lại làm bài tập cho độc giả và hiện được thay bằng
sorry
- Khi làm việc trong namespace
- Ở mục kết, dự án thiết lập một đẳng cấu giữa số tự nhiên thay thế này và số tự nhiên của Mathlib
- Chính xác hơn, bản thân đẳng cấu đó cũng được đặt làm bài tập
- Sau đó, dự án không dùng tiếp phần xây dựng số tự nhiên của Chương 2 nữa mà dùng số tự nhiên của Mathlib
- Dự kiến ở các chương sau của sách, dự án sẽ tiếp tục theo mô hình ngày càng phụ thuộc nhiều hơn vào định nghĩa và hàm của Mathlib thay vì các đối tượng tự xây dựng ở các chương trước
Cách sử dụng và trạng thái kiểm chứng
- Mã trong kho lưu trữ biên dịch được trong Lean
- Tuy nhiên, hiện chưa kiểm thử xem tất cả nhiều
sorrytrong mã có thật sự có thể được điền hay không - Cũng cần kiểm tra liệu các bổ đề cần thiết hoặc API của các tệp Lean đã đủ chưa
- Mục tiêu là xác nhận liệu có thể điền
sorrymột cách tự nhiên về mặt khái niệm mà không phải dựa vào các kỹ thuật lập trình Lean khó hiểu hay không
- Mục tiêu là xác nhận liệu có thể điền
- Tác giả mong các tình nguyện viên playtest companion để xác nhận liệu có thể thực sự giải các bài tập trong Lean hay không
- Các phản hồi khác cũng được hoan nghênh
Tính chất như tài liệu nhập môn Lean và Mathlib
- Companion này có thể dùng không chỉ cho giải tích thực mà còn để nhập môn Lean và Mathlib
- Tính chất này phần nào tương tự Natural number game
- Natural number game có nhiều phần trùng về chủ đề với Chương 2 của Analysis I
1 bình luận
Ý kiến trên Hacker News
Tôi cho rằng điểm thú vị nhất khi dạy toán bằng Lean là phản hồi tức thì. Nếu chứng minh của sinh viên sai thì đơn giản là nó không biên dịch được
Trước đây phải có người như trợ giảng, giảng viên hoặc chuyên gia xem thì mới nhận được phản hồi, nhưng giờ trình biên dịch Lean có thể đưa ra phản hồi nhanh chóng
Trong tương lai, sẽ thật tốt nếu trình biên dịch Lean cũng cung cấp phản hồi mang tính giáo dục hơn, giống như trình biên dịch Rust gợi ý cách sửa mã, và có lẽ có thể cần một LLM chuyên dụng
Trước đây khi học toán, người ta thường dành nhiều thời gian ngẫm nghĩ bài tập, thử đủ thứ trên giấy, và quá trình đó đôi khi dẫn đến việc nội hóa khái niệm và nảy ra ý tưởng mới
Tôi tự hỏi liệu khi dùng Lean, người học có thể chuyển sang kiểu thử bừa, kiểm tra ngẫu nhiên và tuôn ra liên tục hay không. Khi tôi vài lần động đến Coq, ký ức còn lại chủ yếu cũng là mò mẫm và thử đủ thứ
reduce(r.num, r.denom) = reduce(a, b)cross_equals(a, b, r.num, r.denom)r.denom * a = r.num * bKhông dùng LLM; một mô hình cục bộ nhỏ đang chạy bên trong tiện ích mở rộng VS Code. Hy vọng một ngày nào đó mô hình cục bộ nhỏ đó sẽ mạnh đến mức vượt xa con người. Chi tiết có tại https://acornprover.org/docs/tutorial/proving-a-theorem/
Thật sự rất đáng mong đợi. Hy vọng nó được chuyển sang một kho lưu trữ riêng để dễ tìm và dễ gửi cho người khác
Ban đầu tôi tò mò về toán học, và Analysis của Tao là cuốn giáo trình đầu tiên cho tôi thấy toán học được xây dựng theo cách nghiêm ngặt mà tư duy lập trình vẫn kỳ vọng
Sau đó tôi cũng thử Lean một chút và thấy thỏa mãn tương tự, nhưng Mathlib khá phức tạp nếu dùng để học các khái niệm toán học. Vì vậy tôi rất mừng khi có một cây cầu nối giữa sách và công cụ
Thật vui khi thấy chứng minh định lý đang có đà trong các chủ đề toán học chính thống như giải tích
Trong lĩnh vực lý thuyết ngôn ngữ lập trình, khi các công cụ đã bắt đầu khá hoàn thiện vào khoảng giữa thập niên 2010, một giáo trình tiêu biểu như The Formal Semantics of Programming Languages của Winskel từng được kiểm chứng hình thức bằng Isabelle. Không phải là bản chép lại 1:1 hoàn chỉnh, nhưng http://concrete-semantics.org là một ví dụ
Nếu quan tâm đến chứng minh định lý, cá nhân tôi nghĩ hướng đó là điểm khởi đầu dễ hơn nhiều. Vì bản thân các định lý giải tích đã khá khó rồi
Ta làm quy nạp cấu trúc, áp dụng giả thiết quy nạp để chỉ ra bất biến được duy trì, rồi tiếp tục như vậy
Tôi cũng chưa làm nhiều chứng minh định lý, và cũng chưa làm các chứng minh “toán học” như giải tích bằng trợ lý chứng minh, nhưng nếu chứng minh toán học đòi hỏi một cách tiếp cận khác hẳn thì tôi tò mò kỹ năng có thể chuyển giao giữa hai bên đến mức nào
Tôi cũng muốn nhắc đến Software Foundations của Rocq. Có thể đã có bản port sang Lean, nhưng khi tôi theo phần đầu thì thấy khá dễ chịu
Sẽ rất thú vị nếu đánh giá cách tiếp cận “giáo trình” chính thống khác với cách tiếp cận của Mathlib như thế nào
Nhìn chung, các thư viện toán học được hình thức hóa diễn đạt kết quả ở mức tổng quát nhất có thể, và giúp dễ tái cấu trúc phần triển khai chứng minh theo hướng trực quan và thanh nhã hơn
Việc tái cấu trúc dễ là vì hệ thống luôn theo dõi điều gì suy ra logic từ điều gì. Khi làm bằng giấy bút thì không có điều đó, nên thường bỏ lỡ các cơ hội làm lại
Việc dạy giải tích thực ở bậc đại học theo phiên bản “tổng quát tối đa” kiểu Mathlib có hợp lý hay không cũng là một câu hỏi tự nhiên. Tất nhiên các lĩnh vực toán học dựa trên chứng minh khác cũng vậy
Theo tôi biết, kinh nghiệm của các giảng viên đã thử thực tế cũng tương tự. Với sinh viên trình độ cao thì ổn, nhưng với sinh viên trung bình thì rất có thể sẽ lãng phí thời gian trên lớp
Thiên kiến của tôi đến từ việc tôi học các khái niệm toán học qua bài báo
Tôi cảm thấy mã tạo thêm gánh nặng rất lớn, và thường không tuân theo bất kỳ chuẩn phong cách nào. Nói với tư cách một người từng phải đọc cả những bài báo toán học bị đánh giá là không thể hiểu nổi, thì mã còn tệ hơn gấp 10 lần vì gần như không có tiêu chuẩn nào về khả năng hiểu được
Trên kênh YouTube của chính Terence Tao cũng có vài video dùng Lean. https://www.youtube.com/@TerenceTao27
Tôi không biết chi tiết, nhưng việc xem ông ấy làm việc có hoặc không dùng LLM thật thú vị
Với một chủ đề nền tảng như giải tích, tôi nghĩ đây là một dự án rất hay và một cách tiếp cận tốt
Có hai mối lo hiện lên ngay. Thứ nhất, các kết quả giải tích cốt lõi của Mathlib dùng khái niệm filter để xử lý giới hạn một cách tổng quát và thống nhất. Dù vậy, một số kết quả vẫn được chuyên biệt hóa dưới dạng 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
Thứ hai, Mathlib chuyển động nhanh và thường xuyên bị phá vỡ. Tên bị đổi và việc tái cấu trúc diễn ra liên tục, nên các kho lưu trữ phụ sẽ cần được bảo trì liên tục
https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6
Đây là một ý tưởng khá cấp tiến, nhưng tôi nghĩ giáo dục toán học nên tập trung vào việc tạo ra các hệ thống đại số máy tính như Mathematica và các trình chứng minh định lý như Lean. Cũng cần đưa mạnh vào cả trực quan hóa và ứng dụng thực tiễn
Ở mức cực đoan, có thể là một hình thức mà không làm toán trên giấy chút nào nhưng vẫn có thể chứng minh mọi thứ đã học trong Lean
Hệ thống hiện nay tập trung vào vô tận các phép tính thủ công; tôi cảm thấy nó trông quá vô dụng và nhàm chán, khiến người ta ghét toán
Tài liệu Lean thì hay đấy. Nhưng sao lại không có HoTT?
“Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
https://news.ycombinator.com/item?id=43196452
Các tài liệu Lean khác xuất hiện trên HN tuần này:
“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
Động cơ chính xác thì ngoài lĩnh vực của tôi nên tôi không biết, nhưng có vẻ Agda là cách phù hợp hơn Lean để hình thức hóa các ý tưởng đó
Cuối năm nay cũng sẽ có một giáo trình mới, đóng vai trò như bản cập nhật hiện đại hơn cho cuốn sách HoTT hiện có, và cũng có bản hình thức hóa bằng Agda
https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
https://github.com/HoTT-Intro/Agda
HoTT hoàn toàn chưa gần với việc được chấp nhận như một chuẩn hợp lý, và với đa số mọi người thì đây là chủ đề khiến họ mắc kẹt ngay từ đầu
Nó giống như hỏi một nhà phát triển framework JavaScript rằng tại sao họ không làm framework cho Elm hay Haskell vậy
Công sức bỏ ra để khiến trình chứng minh định lý HoTT dễ dùng hơn ít hơn rất nhiều, và tài liệu cũng nghèo nàn hơn nhiều
Lợi ích của HoTT cũng không rõ ràng. Có vẻ nó chỉ giảm bớt công việc khi xử lý những cấu trúc rất khó hiểu trong lý thuyết phạm trù
Terrence Tao có vài giáo trình về giải tích, và đây là tài liệu đồng hành bằng Lean cho cuốn đầu tiên trong số đó. Ông ấy không có giáo trình về lý thuyết kiểu, nên không có lý thuyết kiểu bậc cao. Ngay từ đầu việc muốn làm đã hoàn toàn khác
Rất tuyệt. Analysis I là giáo trình toán “thật sự” đầu tiên mà tôi, một kỹ sư chứ không phải nhà toán học, cảm thấy có thể hoàn toàn theo kịp và giải được sau nhiều lần thử các sách khác như Rudin
Hy vọng tài liệu đồng hành Lean sẽ giúp những người quen thuộc với toán học và lập trình, và muốn học một cách nghiêm ngặt, tiếp cận dễ dàng hơn
Trong vài năm qua đã có những nỗ lực đều đặn nhằm hình thức hóa cuốn Analysis I của Tao bằng Lean, và cũng có những người từng muốn làm đúng việc mà Tao hiện đang làm. Đáng tiếc là phần lớn không vượt quá vài chương đầu, nhưng hy vọng Tao có thể đi xa hơn
Tôi cũng từng nghĩ đến việc tự làm thử. Vì nếu gắn các chứng minh đã được hình thức hóa cho từng bài tập vào blog chú giải Analysis I của tôi https://taoanalysis.wordpress.com/, có lẽ sẽ hữu ích cho những người đang học theo cuốn sách
Tôi cũng đã đăng lên máy chủ Discord riêng của cuốn sách, nhưng thấy có thể hữu ích ở đây nên chia sẻ các tài liệu liên quan
https://github.com/cruhland/lean4-analysis — lấy từ 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/ — không theo sách của Tao, nhưng là phiên bản Lean4 của trò chơi số tự nhiên nên nội dung rất giống chương 2
https://github.com/djvelleman/STG4/ — là trò chơi lý thuyết tập hợp trên Lean4 nên có thể tương tự chương 3. Tuy nhiên, trong https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean có
import Mathlib.Data.Set.Basic, nên có vẻ họ nhập tập hợp của Lean thay vì định nghĩa tập hợp mới và xây dựng các tiên đề. Cách tiếp cận này có thể khiến Lean biết “quá nhiều” về lý thuyết tập hợp, nên có thể không phù hợp với mục đích nàyhttps://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — dùng để 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 — dùng để xây dựng số hữu tỉ
https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — cho thấy một cách định nghĩa kiểu
Settùy chỉnh