Vì sao không đơn giản chỉ dùng Lean

 (lawrencecpaulson.github.io)
1 điểm bởi GN⁺ 6 giờ 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, dòng LCF, HOL, Rocq, ACL2 và Mizar đã tạo ra nhiều công trình 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 toán học hiện đại dựa trên thư viện lớn và cộng đồng năng động, nhưng propositions as types hay dependent types không phải là con đường duy nhất cho proof assistant
  • Isabelle nhấn mạnh các ưu điểm như tự động hóa mạnh, khả năng đọc cao, và tránh dependent types, đồng thời tiếp nối truyền thống LCF trong việc tổ chức kiểm tra chứng minh bằng hàng rào trừu tượng của kernel ngay cả khi không có proof object
  • Khi AI ngày càng tham gia vào việc sắp xếp chứng minh có cấu trúc và dịch giữa các hệ thống khác nhau, áp lực phải xem một công cụ duy nhất như tiêu chuẩn tuyệt đối có thể sẽ còn giảm thêm 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, đi từ logic thuần túy đến cả cấu tạo 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 quả này đã không xuất hiện lại trong 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 quay 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 các chứng minh dài và khó đọc
    • Dù vậy, tác giả cho rằng nó vẫn tốt hơn Rocq trong việc xử lý các lớp tương đương; khác với setoid hell mà người dùng Rocq gặp phải, Jutting đã 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 siêu ngôn ngữ cho proof assistant đã lan rộng
  • Nhiều nhóm tại Cambridge, INRIA, Cornell và nơi khác đã dùng ML để xây dựng các công cụ như HOL đời đầu, Coq (nay là Rocq), và Nuprl
  • Nhóm HOL tập trung vào kiểm chứng phần cứng, nhưng việc kiểm chứng phần cứng dấu chấm động khiến họ cần đến giải tích thực
  • John Harrison đã chứng minh những kết quả toán học thật sự lớn như định lý số nguyên tố trong dòng 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 định lý càng tốt trong danh sách 100 theorems, HOL Light thường xuyên đứng ở nhóm dẫn đầ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ý cấp cao
  • Các định lý này nhìn chung có chứng minh dài và phức tạp, công việc hình thức hóa cũng rất đồ sộ, đồng thời đóng vai trò then chốt trong việc giảm bớt những điểm còn nghi vấn của chính các đị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 xây dựng các định nghĩa đó 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 những ý tưởng tương tự cũng được thảo luận
  • Kevin Buzzard nghe điều này và quyết định thử dùng Lean cho giảng dạy, từ đó sự lan rộng càng tăng nhanh
  • Một bước ngoặt quan trọng của cộng đồng Lean được nêu ra là việc thoát khỏi sự ám ảnh với chứng minh kiến tạo vốn thống trị Rocq trong thời gian dài
  • Chủ nghĩa trực giác xuất hiện sau nghịch lý Russell và cũng kéo theo những hàm ý nhất định đối với 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 trực giác, nhưng tác giả viết rằng Rocq không thể bị nhìn đơn giản như vậy
  • Dù vậy, trong các bài báo liên quan đến Rocq, chứng minh kiến tạo vẫn lặp đi lặp lại ngay cả ở những nơi nó không liên quan hoặc không có ý nghĩa; tác giả cho rằng xu hướng này đã cản trở việc áp dụng Rocq vào toán học và nhường chỗ 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 bộ tạo kiểu Π, Σ, →, ×, +
  • Khuôn khổ này đẹp và có sức sản sinh lớn 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 theo 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; tuy có các yếu tố tương tự Π và →, logic của nó vẫn được thiết lập 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 biệt 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), do đó cần đến proof irrelevance
  • Tác giả cũng khẳng định rằng quan niệm cho rằng cách tiếp cận LCF giống propositions as types là không đúng sự thật
  • Trong Rocq và Lean có Prop, sort dành cho mệnh đề; tại đây mọi proof object của cùng một mệnh đề đều được đánh giá là cùng một giá trị, qua đó cung cấp proof irrelevance
  • Nhưng điều đó không có nghĩa là các proof object khổng lồ biến mất; trong hệ thống thực tế chúng vẫn còn tồn tại
  • Khám phá cốt lõi của Robin Milner là trong LCF không cần chính proof object
  • Nếu đặt kernel chứng minh vào trong abstract data type của ML và 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
  • Nhờ abstraction barrier của ML, tác giả cho rằng không thể gian lận
  • Trong thời đại RAMmageddon, việc các term khổng lồ chiếm hàng chục MB dù không biểu thị gì thêm trở nên đặc biệt phi lý
  • Tác giả cũng phê phán việc còn có cả nghiên cứu nhằm làm cho những term không cần thiết đó trở nên 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à điều 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 đây là điểm mạnh với khả năng tự động hóa mạnh nhất, và cho rằng ngay cả khi so với các “hammer” thường thấy, cũng không gì sánh được với sledgehammer
    • Ông cũng viết rằng mảng đại số máy tính cần được xem xét riêng

  • Khả năng đọc

  • Tránh dependent types

    • Vì không có dependent types, nó tránh được universe level và nhiều điểm dị thường dễ làm người mới bối rối
    • 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 dependent types cũng không được khuyến khích
    • Điểm khó cốt lõi của dependent types 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 tính bằng nhau là không quyết định được, và ban đầu điều đó từng được xem là đương nhiên
    • Từ khoảng năm 1990, sự đồng thuận dần chuyển sang hạ khái niệm bằng nhau xuống definitional/intensional equality để việc kiểm tra kiểu trở nên quyết định được
    • Kết quả là (T(N+1)) và (T(1+N)) trở thành hai kiểu khác nhau
    • Những giới hạn này có ảnh hưởng đến cả chứng minh thực tế, và ngay cả việc kiểm tra definitional equality cũng vẫn tốn kém tính toán

Toán học hiện đại vẫn có thể làm được mà không cần dependent types

  • Tác giả viết rằng vào năm 2017 ông còn thận trọng hơn nhiều về việc Isabelle có thể gánh được đến đâu trong toán học
  • Khi đó, người ta dễ nghĩ rằng để xử lý các chủ đề như sau thì dependent types là bắt buộc
  • Tuy nhiên, thông qua nghiên cứu liên quan đến Alexandria, tác giả đã học được nhiều điều, và tổng kết rằng điểm cốt lõi là không nhồi mọi thứ vào kiểu

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

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

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

  • Lịch sử hình thức hóa toán học không thể trọn vẹn 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 thêm để sửa lại 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⁺ 6 giờ 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