Vì sao không cứ dùng Lean?

 (lawrencecpaulson.github.io)
1 điểm bởi GN⁺ 11 ngày trước | 1 bình luận | Chia sẻ qua WhatsApp
  • Lịch sử hình thức hóa toán học không bắt đầu với Lean; từ gần 60 năm trước, nhiều dòng hệ thống khác nhau đã tích lũy sẵn các kỹ thuật cốt lõi và thành tựu quan trọng
  • Các công cụ như AUTOMATH năm 1968, họ LCF, HOL, Rocq, ACL2, Mizar đã tạo ra nhiều hình thức hóa rộng khắp, từ giải tích thực đến định lý số nguyên tố, định lý bốn màu và giả thuyết Kepler
  • Lean đã nhanh chóng xây dựng các định nghĩa của toán học hiện đại nhờ thư viện lớn và cộng đồng năng động, nhưng propositions as types hay kiểu phụ thuộc không phải là con đường duy nhất cho proof assistant
  • Isabelle nêu bật các ưu điểm như tự động hóa mạnh, khả năng đọc cao, và tránh kiểu phụ thuộc, đồng thời tiếp nối truyền thống LCF xây dựng việc kiểm tra chứng minh bằng rào chắn trừu tượng của kernel mà không cần proof object
  • Khi xu hướng AI sắp xếp các chứng minh có cấu trúc và dịch chúng sang hệ thống khác ngày càng mạnh lên, gánh nặng phải xem một công cụ duy nhất là tiêu chuẩn tuyệt đối có thể sẽ còn giảm đi trong tương lai

Các hệ thống ban đầu và những dòng phát triển khác

  • AUTOMATH

    • AUTOMATH từ năm 1968 đã bao gồm hầu hết các yếu tố cần thiết cho hình thức hóa toán học
    • Năm 1977, Jutting đã dùng AUTOMATH để hình thức hóa Foundations of Analysis của Landau, bắt đầu từ logic thuần túy và đi tới cả xây dựng số phức
    • Ông dùng lớp tương đương và tập số hữu tỉ, đồng thời cũng chứng minh hình thức tính đầy đủ Dedekind của trục số thực
    • Thành tựu này không được lặp lại trong suốt 20 năm, mãi đến giữa thập niên 1990 việc hình thức hóa số thực mới xuất hiện lại trong HOL Light của John Harrison và Isabelle/HOL của Jacques Fleuriot
    • Ký pháp rất bất tiện và hoàn toàn không có tự động hóa, nên chứng minh vừa dài vừa khó đọc
    • Dù vậy, tác giả cho rằng nó xử lý lớp tương đương tốt hơn Rocq; khác với setoid hell mà người dùng Rocq thường gặp, Jutting đã thực hiện việc hình thức hóa lớp tương đương một cách điềm tĩnh

  • Boyer và Moore

Dòng phát triển sau LCF

  • Edinburgh LCF tập trung vào lý thuyết ngôn ngữ lập trình, nhưng ý tưởng dùng ngôn ngữ hàm làm meta-language cho proof assistant đã lan rộng
  • Nhiều nhóm ở Cambridge, INRIA, Cornell và nơi khác đã dùng ML để tạo ra các công cụ như HOL đời đầu, Coq (nay là Rocq), Nuprl
  • Nhóm HOL tập trung vào kiểm chứng phần cứng, nhưng do kiểm chứng phần cứng dấu chấm động nên đã cần tới giải tích thực
  • John Harrison đã chứng minh các kết quả toán học thực thụ như định lý số nguyên tố trong họ HOL thông qua công thức tích phân Cauchy
  • Với mục tiêu kiểm chứng càng nhiều càng tốt trong 100 theorems, HOL Light thường xuyên đứng ở nhóm đầu
  • Đến năm 2014, các hệ thống thuộc dòng này đã hình thức hóa nhiều định lý cao cấp
  • Nhìn chung, các định lý này có chứng minh dài và phức tạp, quy mô hình thức hóa cũng rất lớn, và đóng vai trò then chốt trong việc giảm bớt những điểm còn nghi vấn của định lý

Sự trỗi dậy của cộng đồng Lean

  • Các nhà toán học cho rằng những thành tựu hình thức hóa trước đó chưa chạm tới các cấu trúc tinh vi của toán học hiện đại dòng chính như Grothendieck schemes hay perfectoid spaces
  • Tom Hales đã chọn hướng tích lũy các định nghĩa này thành thư viện, tập trung vào tích lũy định nghĩa hơn là chứng minh, và chọn Lean
  • Ông đã trình bày hướng đi này trong chương trình Big Proof, nơi các ý tưởng tương tự cũng được thảo luận cùng lúc
  • Kevin Buzzard nghe điều đó rồi quyết định thử dùng Lean trong giáo dục, từ đó tốc độ lan rộng tăng mạnh
  • Một bước ngoặt quan trọng của cộng đồng Lean, theo tác giả, là thoát khỏi sự ám ảnh với chứng minh kiến tạo từng chi phối Rocq trong thời gian dài
  • Trực giác luận xuất hiện sau nghịch lý Russell và kéo theo những hàm ý nhất định cho cả khái niệm số thực
  • Martin-Löf type theory rõ ràng là một hình thức chủ nghĩa hình thức trực giác, nhưng tác giả viết rằng không thể nhìn Rocq đơn giản như vậy
  • Dù thế, trong nhiều bài viết liên quan Rocq, chứng minh kiến tạo vẫn lặp đi lặp lại cả ở những chỗ không liên quan hoặc vô nghĩa; tác giả cho rằng xu hướng này đã cản trở ứng dụng toán học của Rocq và nhường vị trí đó cho Lean

propositions as types và sự khác biệt của LCF

  • Propositions as types là tính đối ngẫu nối các ký hiệu logic ∀, ∃, →, ∧, ∨ với các toán tử tạo kiểu Π, Σ, →, ×, +
  • Khuôn khổ này đẹp và có năng suất về mặt lý thuyết, nhưng không phải con đường duy nhất
  • Nếu giới hạn proof assistant thành phần mềm kiểm tra chứng minh dựa trên nguyên lý propositions as types, thì phần lớn nghiên cứu của nửa thế kỷ qua sẽ bị đẩy ra ngoài định nghĩa
  • Khi đó chỉ còn Rocq, Lean và Agda
  • Ngay cả AUTOMATH cũng không phải một ví dụ của propositions as types; dù có những yếu tố giống Π và →, phần logic vẫn được đặt bằng các tiên đề như trong giáo trình logic thông thường
  • Từ 50 năm trước, de Bruijn đã cho rằng cần tách kiểu và mệnh đề
  • Ví dụ điển hình là phép chia phải nhận ba đối số, và giá trị của (x/y) sẽ phụ thuộc vào chứng minh của (y \ne 0), vì thế cần proof irrelevance
  • Tác giả cũng nhấn mạnh rằng nhận thức cho rằng cách tiếp cận LCF cũng chính là propositions as types là không đúng sự thật
  • Rocq và Lean có Prop, là sort của mệnh đề; tại đó mọi proof object của cùng một mệnh đề đều được đánh giá là cùng một giá trị, nhờ vậy cung cấp proof irrelevance
  • Nhưng điều đó không làm các proof object khổng lồ biến mất; trong hệ thống thực tế chúng vẫn còn đó
  • Khám phá cốt lõi của Robin Milner là trong LCF, bản thân proof object là không cần thiết
  • Đưa kernel chứng minh vào abstract data type của ML, rồi dùng các quy tắc suy diễn làm constructor, thì có thể kiểm tra chứng minh một cách động
  • Tác giả cho rằng nhờ abstraction barrier của ML, việc gian lận là bất khả thi
  • Trong thời đại RAMmageddon, việc những term khổng lồ không chỉ ra điều gì mà vẫn chiếm hàng chục MB trở nên đặc biệt phi lý
  • Tác giả cũng phê phán việc nghiên cứu tiếp tục đi theo hướng làm cho những term không cần thiết đó trông thanh nhã hơn

Lý do để chọn Isabelle

  • Nếu đồng nghiệp dùng Lean, chuyên môn của nhóm cũng nằm ở Lean, và thư viện tiên đề cần thiết cũng có trên Lean, thì dùng Lean là lựa chọn tự nhiên
  • Tuy vậy, nếu có thể tự do lựa chọn thì vẫn có lý do rõ ràng để cân nhắc Isabelle

  • Tự động hóa

    • Tác giả xem tự động hóa mạnh nhất là ưu điểm nổi bật, và cho rằng ngay cả khi so với các “hammer” thường ngày thì cũng không gì sánh được với sledgehammer
    • Tác giả cũng viết rằng mảng đại số máy tính cần được bàn riêng

  • Khả năng đọc

  • Tránh kiểu phụ thuộc

    • Vì không có kiểu phụ thuộc, nó tránh được universe level và nhiều điểm kỳ quặc khiến người mới lúng túng
    • Tác giả viết rằng ngay cả trong mathlib của Lean và SSReflect, Mathematical Components của Rocq, việc dùng kiểu phụ thuộc cũng không được khuyến khích
    • Điểm khó cốt lõi của kiểu phụ thuộc là nếu triển khai đúng nghĩa thì bản thân việc kiểm tra kiểu sẽ trở nên không quyết định được
    • Điều này là do việc quyết định đẳng thức là không quyết định được, và lúc ban đầu đây từng được xem là điều hiển nhiên
    • Khoảng từ năm 1990, sự đồng thuận chuyển sang hướng làm cho kiểm tra kiểu trở nên quyết định được bằng cách hạ đẳng thức xuống definitional/intensional equality
    • Kết quả là (T(N+1)) và (T(1+N)) trở thành hai kiểu khác nhau
    • Những hạn chế này ảnh hưởng đến cả chứng minh thực tế, và bản thân việc kiểm tra definitional equality vẫn còn tốn kém tính toán

Toán học hiện đại vẫn làm được mà không cần kiểu phụ thuộc

  • Tác giả viết rằng vào năm 2017, ông còn thận trọng hơn nhiều khi đánh giá Isabelle có thể gánh được tới mức toán học nào
  • Khi đó, người ta rất dễ nghĩ rằng muốn xử lý những chủ đề như sau thì kiểu phụ thuộc là không thể thiếu
  • Nhưng thông qua nghiên cứu liên quan đến Alexandria, tác giả đã học được nhiều điều, và kết luận then chốt là đừng cố nhồi mọi thứ vào kiểu

Hướng đi sắp tới và AI

  • Lean làm đúng rất nhiều điều, và còn hỗ trợ cả khối chứng minh lồng nhau, nên về tiềm năng có thể trở thành một ngôn ngữ chứng minh đủ dễ đọc
  • Giờ đây cộng đồng Lean cần thực sự tận dụng những tính năng như vậy, còn người dùng Isabelle thì phần lớn đã làm điều đó từ trước
  • Sự minh bạch của văn bản chứng minh mà con người thực sự đọc được quan trọng hơn proof object để máy tính kiểm tra
  • Sự trỗi dậy của AI càng làm khác biệt này rõ nét hơn
  • Chứng minh do AI tạo ra thường khá lộn xộn, nhưng lại dễ dọn dẹp bằng sledgehammer, và nếu cấu trúc tốt thì dù chi tiết hơi quá vẫn có thể đọc được
  • Làm như vậy sẽ dễ nắm luồng tiến triển và dễ rút gọn về dạng đơn giản hơn
  • Gần đây cũng đã có nghiên cứu trong đó mô hình ngôn ngữ trực tiếp gọi sledgehammer
  • AI cũng có thể dễ dàng dịch các chứng minh có cấu trúc, dễ đọc từ proof assistant này sang proof assistant khác
  • Khi đó, gánh nặng của chính việc phải chọn hệ thống nào sẽ giảm đi

Bổ sung phần thiếu về Mizar

  • Lịch sử hình thức hóa toán học sẽ không thể đầy đủ nếu thiếu Mizar và thư viện toán học đồ sộ của nó
  • Ngôn ngữ Isar của Isabelle cũng chịu ảnh hưởng lớn từ Mizar
  • Tác giả nói riêng để đính chính việc đã bỏ sót Mizar, và sẽ bàn về Mizar trong bài viết tiếp theo

Bài viết liên quan

1 bình luận

 
GN⁺ 11 ngày trước
Ý kiến Hacker News

  • Phần lớn độc giả HN gần với lập trình viên hơn là nhà toán học, nên nhìn Lean từ góc độ lập trình thực tế hơn là từ góc độ chứng minh toán học có lẽ sẽ hữu ích hơn
    Có cuốn sách về Lean dưới góc nhìn lập trình hàm là https://leanprover.github.io/functional_programming_in_lean/ khá hay
    Tôi cũng đang học Lean nên có thể vẫn còn hơi lạc quan kiểu người mới, nhưng gần đây đang hướng tới việc viết và chứng minh những đoạn mã mà lập trình viên bình thường cũng dùng, như các thuật toán nén/giải nén thực tế kiểu ví dụ lean-zip
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • Khi đọc cuốn sách này, tôi đã thử tự tay nghịch một bộ đơn giản hóa đại số máy tính cơ bản bằng Lean
      https://github.com/dharmatech/symbolism.lean
      Đây là bản port từ mã C#, và khả năng biểu đạt của Lean lớn đến mức đáng kinh ngạc
    • Nếu dùng cho mục đích đó thì Dafny cũng có vẻ là một lựa chọn tương tự
      Trước đây tôi có thấy nó từng được nhắc đến khá nhiều, nhưng gần đây không theo dõi kỹ lĩnh vực này nữa
    • Tôi nhớ có những thử nghiệm về chứng minh tính đúng đắn của phần mềm từ thập niên 1990, và hình như phần chú thích chứng minh cuối cùng còn phát sinh nhiều lỗi hơn chính phần mềm thực tế
      Ngoài ra tôi còn thấy thêm hai rào cản. Thứ nhất là bản thân việc biết phần mềm cần phải làm gì đã rất khó, và điều người dùng muốn làm không nhất thiết trùng với điều khách hàng trả tiền
      Thứ hai là chất lượng công việc của nhiều lập trình viên vốn quá thấp, nên khó mà kỳ vọng họ xử lý tốt ngôn ngữ chân lý hơn các ngôn ngữ như Java
      Tuy vậy, điểm thứ hai có thể sẽ biến mất khi được thay bằng các hệ thống AI biết chú ý cẩn thận những gì cần thiết, và khi đó cục diện có thể thay đổi
    • Tôi cũng tự hỏi lập trình phi hàm thì sao
      Theo tôi, lập trình hàm cũng chẳng liên quan nhiều tới đa số lập trình viên hơn là toán học thuần vốn từ lâu đã bị bỏ lại phía sau

  • Có vẻ tác giả bài viết hiểu Lean khá sai, mà điều đó càng lạ hơn vì ông ấy trông như người rất rành lĩnh vực này
    Ông ấy dường như cho rằng Lean giữ nguyên đối tượng chứng minh, và cuối cùng kiểm tra một đối tượng chứng minh khổng lồ với mọi định nghĩa đã được bung hết ra, nhưng thực tế không phải vậy
    Lean về cơ bản triển khai gần như đúng loại tối ưu hóa mà tác giả ca ngợi ở LCF. Có thể hình dung như việc vừa chứng minh vừa xóa bảng để tiếp tục
    Trong Lean4, nếu viết bằng theorem thay vì def thì đối tượng chứng minh đó sẽ không còn được dùng nữa, và đây không chỉ là tối ưu hóa mà là một tính chất cốt lõi của ngôn ngữ. theorem là opaque
    Kể cả khi term chứng minh còn tồn tại thì cũng chỉ để người dùng có thể xem trong chế độ tương tác, còn kernel thậm chí không thể quan tâm đối tượng chứng minh đó thực ra là gì

    • Đây gần với khác biệt khái niệm hơn là khác biệt triển khai
      Trong LCF, chứng minh và term là hai thứ khác nhau, và theo tôi vốn dĩ nên như vậy. Kiểu lẫn lộn theo Curry-Howard này là không cần thiết, nhưng nhiều người lại tưởng đó là cách duy nhất để làm toán bằng máy tính
      Nếu muốn thì trong LCF bạn vẫn có thể lưu và dùng lại chứng minh, còn trong Lean nếu muốn thì cũng có thể xóa chúng đi như một tối ưu hóa
    • Trong lý thuyết kiểu phụ thuộc, đối tượng chứng minh chính là một term lấp đầy một kiểu nào đó, nên tôi thắc mắc điều đó có nghĩa là cách triển khai của Lean có thể dựng chứng minh mà không cần thực sự tạo ra các term như vậy hay không
    • Nghe có vẻ đúng
      Cách tiếp cận kiểu trừu tượng có thể tiết kiệm bộ nhớ đôi chút, nhưng chỉ là khác biệt ở hệ số hằng chứ không cải thiện về mặt tiệm cận
      Những lời phàn nàn kiểu Lean lãng phí hàng chục MB có lẽ quan trọng vào thập niên 1980–90, nhưng ngày nay có thể đó không còn là lợi thế mang tính quyết định nữa

  • Tôi thường nghe nói Lean tốt cho lập trình hàm, nhưng nếu đi từ Agda sang thì nó khá giống một bản hạ cấp vụng về
    Mọi người cũng khen tactic của nó, nhưng theo trải nghiệm của tôi thì tactic của Coq mạnh hơn và dễ dùng hơn
    Có thể tất cả chỉ là thiên kiến ấn tượng ban đầu, nhưng đến lúc này tôi thấy điểm mạnh của Lean không phải vì nó làm một thứ nào đó tốt nhất, mà vì nó khá ổn trên mọi mặt và cộng đồng lớn
    Tôi hiểu vì sao nó hấp dẫn, nhưng cũng hơi tiếc vì cảm giác như phải đánh đổi bớt vẻ đẹp và sức mạnh

    • Nói cho cùng thì đây cũng là câu chuyện hiệu ứng mạng lưới
      Tuy vậy, những hiệu ứng như thế thường ở thời điểm đó trông như sẽ tồn tại mãi mãi, nhưng thực tế lại không bền đến vậy. Nếu chỉ riêng điều đó là quan trọng thì Perl giờ vẫn phải là ông lớn
      Riêng với Lean thì việc có thư viện lớn từ sớm là yếu tố đáng kể. Khá giống vai trò CPAN từng có với Perl
      Nhưng nếu nhìn theo các định luật scaling thì với phần lớn người dùng, giá trị của thư viện lớn có lẽ chỉ tăng theo log của kích thước
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Lúc đầu khoảng cách này có vẻ không thể vượt qua, nhưng đến một lúc nào đó không nhất thiết phải bắt kịp quy mô; tính dễ dùng sẽ quan trọng hơn
      Hơn nữa, việc port thư viện toán học lại rất hợp với LLM. Mã nguồn đã được kiểm chứng, đích đến cũng có thể kiểm chứng, và lộ trình suy luận nhìn chung cũng chuyển sang được
      Nói ngược lại, nhờ LLM mà rào cản làm việc trên các nền tảng nhỏ hơn cũng thấp hơn dự đoán. Nếu tôi có thể chuyển thư viện bên đó sang nền tảng của mình, thì cũng có khả năng chuyển cả các chứng minh của tôi sang đó
    • Ngược lại, điều đó có vẻ cho thấy cộng đồng cuối cùng cũng đã trưởng thành để bắt đầu làm công việc thực tế
      Công cụ hoàn hảo không phải cốt lõi; quan trọng hơn là hoàn thành được việc với một công cụ đủ tốt
    • Agda có thể tốt hơn với vai trò trình kiểm tra chứng minh, nhưng tôi không xem nó là lựa chọn thực dụng để làm phần mềm
      Lean thật sự có tiềm năng phát triển thành một ngôn ngữ hàm cho phát triển phần mềm, thậm chí có thể là người kế nhiệm của Haskell
    • Tôi đã dùng Agda một chút, còn Lean thì nhiều hơn, và thấy việc viết chương trình hàm thông thường trong Lean dễ hơn hẳn so với làm chứng minh toán học
      Khác biệt chủ yếu có lẽ nằm ở hỗ trợ công cụ. Tài liệu của Agda nghèo nàn, cài đặt rồi vận hành trên hệ thống cũng phiền phức, và gần như ép bạn phải dùng Emacs
      Trong khi đó Lean có tài liệu riêng hướng dẫn cả cách viết tiện ích cat, và nhìn chung cho trải nghiệm tooling hiện đại hơn nhiều
    • Tôi tò mò cụ thể Agda tốt hơn ở điểm nào trong lập trình hàm
      Thường lời khen tôi nghe nhiều nhất là về dependent pattern matching, và ở phần đó thì tôi thấy Lean khá yếu
      Nhưng nếu ngay cả trong FP nói chung mà bạn cũng thấy Agda thân thiện hơn, tôi muốn nghe rõ là ở điểm nào

  • Isabelle/HOL thì bản thân ngôn ngữ cũng ổn, nhưng tooling có những khuyết điểm sâu sắc vượt xa chuyện bám vào mô hình desktop
    Ngôn ngữ của nó không khác Lean đến mức chắc chắn là tốt hơn, và tôi cũng đồng ý với một số phê bình nhắm vào dependent type
    Cuối cùng thì hai ngôn ngữ này chỉ đang chọn các đánh đổi khác nhau, và những lựa chọn đó đã khiến mỗi bên trở thành công cụ khá hiệu quả trong khu vực riêng của mình. Bản thân miền chứng minh rất rộng nên mỗi hệ hình sẽ có điểm mạnh điểm yếu khác nhau, còn Lean chỉ là tối ưu cho một phần khác của bài toán
    Sledgehammer thì tốt, nhưng chuyện Lean có một thứ tương tự có lẽ chỉ còn là vấn đề thời gian
    Nó có thể hữu ích ở giai đoạn dò tìm, nhưng lại tốn tài nguyên, và dù giúp làm chứng minh ngắn đi, tôi vẫn thích toàn bộ các bước chứng minh được hiện ra rõ ràng trong mã công khai hơn là kiểu by sledgehammer nửa như phép màu
    Ngược lại, phát triển chính Isabelle thì đau đớn hơn Lean rất nhiều, đặc biệt là trong quá trình giao tiếp với các nhà phát triển
    Thái độ trên mailing list kiểu không có bug, chỉ có hành vi ngoài dự kiến trông vừa trẻ con vừa thiếu chuyên nghiệp
    Và việc châm chọc mức dùng RAM của các hệ giống Lean cũng khá buồn cười nếu nhìn vào cơn háu ăn bộ nhớ của chính Isabelle

    • Vấn đề ở đây là việc biến chứng chỉ UNSAT thành dạng có thể kiểm tra nhanh hoàn toàn không phải chuyện đơn giản
      Về cơ bản, độ khó của nó gần giống với việc dùng chứng minh hình thức ngay từ đầu
    • Lần cuối tôi kiểm tra thì Isabelle/HOL hình như dùng một custom Emacs mode làm giao diện
      Cũng có thể tôi đang nhầm với một hệ HOL khác
    • Tôi không biết Sledgehammer là gì, nhưng nghe mô tả thì nó gần như đúng là công cụ grind của Mathlib
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Điểm thú vị của Lean là Lean là ngôn ngữ, nhưng thứ mọi người chủ yếu nói đến thực ra lại là thư viện Mathlib
    Những người làm Mathlib có vẻ khá thực dụng, nên họ đưa logic cổ điển vào trong các kiểu của Lean và chỉ dùng một phần logic trực giác

    • Ví dụ dùng để giải thích luật bài trung là sai
      “Một điều gì đó không thể vừa đúng vừa sai cùng lúc” không phải luật bài trung mà là luật không mâu thuẫn
      Luật bài trung là p đúng hoặc not p đúng
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • Bên khoa học máy tính hiện đang tự làm CSLib riêng
      https://www.cslib.io https://www.github.com/leanprover/cslib
      Logic trực giác về bản chất có ý nghĩa ở chỗ biến các lập luận toán học thành cấu trúc có thể tính toán được, nên khá thú vị khi nghĩ xem họ sẽ xử lý chuyện này thế nào
      Thực ra, ngay khi bạn viết thuật toán bằng Lean thì bạn đã ở trong một dạng ràng buộc kiến tạo nào đó rồi, và cho mục đích ấy thì có lẽ chừng đó logic là đủ
    • Điều này làm tôi nhớ đến câu đùa về 5 giai đoạn chấp nhận toán học kiến tạo
      phủ nhận, tức giận, mặc cả, trầm cảm, chấp nhận
      Các bài giảng và bài viết liên quan của Andrej Bauer cũng đáng xem
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Ở đây phải là intuitionistic logic chứ không phải intuitive logic
    • Dù có nhiều ràng buộc và bế tắc như vậy, tôi vẫn tò mò không biết khi nào và vì sao người ta lại thích logic trực giác hơn

  • Tôi nghĩ kiểu bài viết thế này nên có nhiều hơn
    Ngay cả trước kiểu tư duy bầy đàn cứ mặc nhiên đẩy mọi người sang cứ dùng X đi, vẫn luôn có những lý do đủ thuyết phục để ít nhất xem xét phương án khác
    Dù cuối cùng vẫn bỏ lựa chọn thay thế và theo dòng chính, tôi nghĩ chọn sau khi hiểu địa hình vẫn tốt hơn

    • Tôi không hoàn toàn đồng ý
      Ngay bây giờ chúng ta vẫn đang tạo ra quá nhiều framework và lựa chọn thay thế, chắc phần nào vì thấy vui
      Thay vì cải thiện công cụ hiện có hay đơn giản là làm việc thực tế, người ta thường lao vào sinh sôi vô tận ngôn ngữ, thư viện và build tool
      Theo tôi, nếu số ngôn ngữ, thư viện và build tool hiện nay chỉ còn một nửa thì có khi còn tốt hơn
    • Cuối cùng thì vẫn là còn tùy tình huống
      Càng rời xa dòng chính thì tài liệu càng ít, bug từ những góc ít ai khai phá càng nhiều, và số người có thể giúp đỡ bạn cũng càng giảm
      Khi có hơn hai mươi lựa chọn chồng chất lên nhau, thì trung bình mà nói cứ chọn phương án tiêu chuẩn rồi đi tiếp là đúng hơn. Sự chú ý là hữu hạn; nếu viết báo cáo khảo sát cho từng dependency thì rốt cuộc lại không giải được bài toán chính
      Chỉ có hai ngoại lệ: hoặc công cụ tiêu chuẩn thực sự không hợp với use case của tôi, hoặc chính công cụ tiêu chuẩn đó lại giao cắt mạnh với bài toán cốt lõi mà tôi đang cố giải

  • Cuộc thảo luận này khiến tôi liên tưởng đến những bài viết chỉ ra giới hạn của Python trong tính toán khoa học
    Khi một cộng đồng vượt qua khối lượng tới hạn quanh một công cụ đủ ổn, điều đó sẽ lấn át hầu hết các yếu tố còn lại
    Nó tạo ra đà phát triển, rồi tutorial, bài giải thích và tài liệu tốt hơn cứ chồng lên nhau, đến mức gần như đạt vận tốc thoát
    Lean có vẻ đang ở đúng vị trí đó, còn có cả Terrance Tao làm người ủng hộ mạnh mẽ
    Vì thế, câu nói kiểu “ngôn ngữ X tốt hơn” không hẳn là sai hoàn toàn, nhưng lại dễ bỏ lỡ câu hỏi quan trọng hơn
    Cốt lõi là liệu nó có thực sự tốt hơn công cụ mà ai cũng biết, có thể dùng ngay, và đang nhận nhiều thời gian cải tiến hơn hay không
    Cuối cùng trông khá giống tình huống worse is better, hoặc ít nhất là tốt và phổ biến thì cũng đã đủ

    • Tôi thấy đây là một điểm hay: LLM có thể khiến việc dịch giữa các hệ hình thức khác nhau trở nên khá hiệu quả
      Đặc biệt trong lĩnh vực này, kết quả dịch còn có thể được kiểm chứng tự động ở mức đáng kể, nên bản thân lựa chọn ban đầu có thể không phải vấn đề quá lớn
    • Nhưng trong thời đại AI, tầm quan trọng của khối lượng tới hạn sẽ giảm đi nhiều
      AI có thể tự viết mã mà không cần một thư viện cộng đồng khổng lồ, và cũng không cần cả triệu tutorial trôi nổi trên Internet vì nó có thể đọc trực tiếp tài liệu và đặc tả
      Cũng không cần tránh những ngôn ngữ không có thị trường việc làm. AI đâu cần xây dựng sự nghiệp, nó chỉ cần làm xong việc đang được giao
      Vì thế những ngôn ngữ nhỏ và DSL vốn trước đây không có cơ hội giờ có thể lại có cửa được chấp nhận
      Tôi nghĩ AI cũng có thể chấm dứt tình trạng đơn văn hóa ngôn ngữ đã kéo dài trong lập trình

  • Câu “hầu như mọi thứ ngày nay được hình thức hóa bằng hệ nào thì AUTOMATH cũng đã có thể hình thức hóa bằng nó” nghe khá giống với việc nói rằng ngày nay mọi thứ viết bằng ngôn ngữ hiện đại thì 50 năm trước cũng đều có thể viết bằng assembly
    Về mặt kỹ thuật có thể đúng, nhưng về mặt kinh tế thì hoàn toàn khác

    • Assembly nhìn chung là Turing-complete, nhưng ở phía các proof engine thì tôi không rõ phép so sánh tương ứng chính xác sẽ là gì

  • Khoảng 15 năm trước tôi từng thử động vào Coq/Rocq và vài công cụ khác, nhưng thấy phần mềm bản thân nó khó hiểu kinh khủng, thậm chí còn hơn cả các khái niệm
    Điểm lạ ở proof assistant / interactive theorem prover là tính chất interactive khiến nó thành kiểu kết hợp giữa ngôn ngữ và IDE, và trên thực tế hai thứ này gắn với nhau rất chặt
    Vì vậy khó mà nói riêng về ngôn ngữ; cũng phải xét luôn môi trường mà nó được dùng trong
    Tôi không phải fan cuồng của VS Code, nhưng rõ ràng một IDE mở rộng được đã được vô số người dùng, được đổ rất nhiều tiền vào và được mài giũa thì đi trước xa các môi trường của những lựa chọn khác
    Những lộ trình nhập môn tuyệt vời như Natural Numbers Game dường như cũng chỉ khả thi nhờ khả năng hack và hệ sinh thái của VS Code
    Tuy vậy, điều tôi lo khi học Lean là khả năng mở rộng cú pháp giống con dao hai lưỡi
    Sau khi học ngôn ngữ, người ta sẽ muốn đọc mã viết bằng ngôn ngữ đó, nhưng nếu mỗi dự án lại bắt đầu tự dựng đầy DSL riêng thì có thể mọi thứ sẽ vượt khỏi tầm kiểm soát
    Cuối cùng chuyện này phụ thuộc vào việc cộng đồng và hệ sinh thái có tiết chế đến đâu, nên tôi đang nhìn nó với cả hy vọng lẫn dè chừng

  • Lean không phải proof assistant được các nhà toán học yêu thích nhất, cũng không phải công cụ hợp nhất cho kiểm chứng hình thức phần mềm
    Nhưng nó làm được cả hai ở mức tạm ổn, và đổi lại đã nắm được thứ khó kiếm nhất là đà phát triển
    Hơn nữa, trong thời đại AI, lượng mã do con người công khai viết ra còn ảnh hưởng trực tiếp tới việc các agent tạo mã mới tốt đến đâu, nên đà đó lại càng mạnh hơn