Toán học bị ma ám

• Lean là ngôn ngữ lập trình được thiết kế để hình thức hóa toán học, cho phép các nhà toán học thao tác các định lý toán học như những đoạn mã
• Người dùng viết định lý, chứng minh, tiên đề dưới dạng mã, và quá trình chứng minh được thực hiện thông qua tập lệnh gọi là tactic
• Ngay cả khi chứng minh chưa được hoàn thành, vẫn có thể tạm dừng bằng sorry, nhưng đây là một dạng chứng minh giả giống với any trong TypeScript
• Nếu thêm sai tiên đề (ví dụ: 2 = 3), sẽ phát sinh nguy cơ mâu thuẫn logic và khả năng chứng minh mọi khẳng định
• Lean chỉ suy ra kết luận dựa trên các tiên đề đã chọn và hệ thống chứng minh về mặt logic, nên việc giữ gìn tính đúng đắn toán học có ý nghĩa quan trọng

---

Lean: Ngôn ngữ làm việc với toán học như mã

• Lean là ngôn ngữ lập trình chuyên dùng để viết các phát biểu toán học được hình thức hóa
• Các nhà toán học dùng Lean để biểu diễn toán học bằng mã và cấu trúc hóa định lý, chứng minh của nhau nhằm hợp tác và chia sẻ
• Họ đưa ra một tương lai trong đó một lượng lớn tri thức toán học của nhân loại có thể được biểu diễn dưới dạng mã, từ đó kiểm chứng tự động và kết hợp một cách cơ giới

Những bước đầu trong chứng minh với Lean

• Trong Lean có thể viết một khai báo định lý đơn giản như theorem two_eq_two : 2 = 2 := by sorry
• Khi chứng minh chưa hoàn thiện, ta chèn sorry, nhưng đây chỉ là mẹo tạm thời chứ không phải chứng minh thật sự
  • sorry sẽ qua được kiểm tra chứng minh của Lean, nhưng về logic thì không đáng tin cậy
• Để có chứng minh đầy đủ, cần dùng tactic như rfl (reflexivity) để chứng minh các đẳng thức hiển nhiên như 2 = 2
• Những nội dung đã chứng minh có thể được tái sử dụng trong các định lý khác bằng exact và các lệnh tương tự, nhấn mạnh tính mô-đun

Tiên đề và mâu thuẫn: Khi toán học bị ma ám

• Nếu thêm tiên đề như axiom math_is_haunted : 2 = 3, Lean sẽ xem tiên đề đó là đúng
• Tiên đề này có thể được dùng trong các bước chứng minh sau đó, và thậm chí có thể chứng minh các kết luận toán học vô lý (ví dụ: 2 + 2 = 6)
• Việc sử dụng tactic rewrite cho phép thay thế 2 bằng 3, rồi kết thúc quy trình chứng minh đẳng thức bằng rfl
• Nếu tiên đề sai gây ra mâu thuẫn, Lean cũng rơi vào trạng thái mọi mệnh đề đều chứng minh được (sụp đổ logic)
• Trên thực tế, vào đầu thế kỷ 20, các mâu thuẫn trong hệ tiên đề như nghịch lý Russell đã dẫn tới những suy tư nền tảng căn bản về toán học
• Như vậy, Lean cho thấy việc chọn tiên đề là nhân tố quyết định để duy trì tính hợp lệ của hệ thống logic

Lean với tư cách trình kiểm tra chứng minh

• Nếu các tiên đề được chọn đúng và Lean nhất quán về logic, nó cung cấp các kết luận có độ tin cậy về mặt lý thuyết
• Từ những đẳng thức đơn giản đến các định lý cực kỳ phức tạp (ví dụ: Fermat’s Last Theorem), tất cả đều được kiểm chứng theo cùng một nguyên lý
• Các định lý lớn được hoàn thiện như một cấu trúc cây, tích lũy qua chứng minh lặp lại các cấu trúc con và định lý cấp thấp
• Ví dụ, có một dự án quy mô lớn đang hình thức hóa Fermat's Last Theorem trong Lean; vào giai đoạn cuối sẽ có một hệ thống chứng minh chính thức hoàn chỉnh không còn dùng sorry

Niềm vui khi học Lean

• Chứng minh với Lean là sự kết hợp sáng tạo giữa lập trình và toán học
• Bắt đầu từ việc chứng minh các mệnh đề đơn giản, rồi dần dần xây dựng chặt chẽ những toán học sâu và phức tạp trở thành một niềm vui quan trọng
• Các tài liệu hướng dẫn chính thức và cộng đồng (ví dụ: Natural Numbers Game, Mathematics in Lean, v.v.) rất phù hợp cho người mới bắt đầu
• Khi dùng Lean, bạn trực tiếp hình thức hóa logic và có thể khám phá lại vẻ đẹp của ý tưởng tinh tế cùng lập luận
• Kết luận rằng, ngay cả khi không có lý do rõ ràng, với một số nhóm người, Lean mang lại một niềm thích thú đặc biệt

[GN⁺]

Ý kiến trên Hacker News

• Dạo này tôi đang nghĩ đến ý tưởng viết lại tin tức hoặc các bài phi hư cấu bằng một hệ thống giống Lean (hoặc chính Lean), xem mỗi phát biểu như một định lý cần được chứng minh, và phần chứng minh cũng bao gồm cả trích dẫn; ví dụ có thể xử lý bằng một chứng minh tổng hợp kiểu “nếu ba nguồn tôi phê duyệt đều khẳng định đây là sự thật thì đây là sự thật”, rồi có lẽ còn có thể đánh dấu toàn bộ tài liệu để người đọc thấy được những khẳng định đã được “chứng minh”; không hoàn hảo, nhưng là một nỗ lực dùng công nghệ để khôi phục phần nào sự nghiêm ngặt mà báo chí ngày nay từng đảm nhiệm
  • Việc hình thức hóa các phát biểu bằng ngôn ngữ tự nhiên là một lĩnh vực đầy rẫy khó khăn, vì những lý do khá giống với việc khó viết mã tương tác với thế giới thực; để các sự kiện có thể liên kết với nhau hoặc được biểu đạt, ta phải xử lý rất tỉ mỉ trong khuôn khổ hình thức mọi khái niệm vốn được xem là hiển nhiên như đồng nhất, thời gian, quan hệ nhân quả, v.v.; dù vậy đây thực sự là một bài toán rất hấp dẫn; OpenCog từng là một dự án theo đuổi hướng này đến cùng, và trong học thuật cũng có hẳn một lĩnh vực riêng là biểu diễn tri thức và suy luận (KRR); tạp chí IJCAI cũng đầy các nghiên cứu liên quan, và các nhà triết học cũng đã xây dựng nhiều hệ logic để hình thức hóa các kiểu lập luận khác nhau về thời gian, tính khả hữu, xác suất, v.v., nhưng đáng tiếc là chúng không dễ kết hợp với nhau (trừ khi gần đây việc đó đã được giải quyết)
  • Tôi nghĩ niềm tin quan trọng nhất mà ta nên có với tin tức phần lớn không phải thứ có thể được chứng minh như một tập hợp các mệnh đề tuyệt đối; các công cụ tính chuỗi suy luận như xác suất Bayes có lẽ phù hợp hơn; tôi đã từng thấy các công cụ để ước lượng bằng số theo kiểu đó
  • Tôi từng có trải nghiệm rằng sau khi học toán ở đại học thì khả năng viết phi hư cấu của mình cải thiện rất nhiều; khi đọc các bài luận do SO của tôi và em gái tôi viết, tôi áp dụng sự nghiêm ngặt như đang xem một chứng minh logic, kiểu như “ở đây nói C suy ra từ B, nhưng lý do B suy ra từ A thực ra lại bị thiếu, vậy thì không thể nói C suy ra từ A được”; có vẻ như với các công cụ như LLM, ta có thể biến chuyện đó thành một chương trình, nhưng hiện tượng ảo giác (tạo ra các khẳng định không có thật) khiến giới hạn của nó khá rõ ràng
  • Cần phải cẩn thận, vì cách tiếp cận này có thể rất dễ trao cho những tuyên bố vốn cực đoan hoặc vô nghĩa một hào quang khách quan logic; quan điểm chính trị của Gottlob Frege, một trong những cha đẻ của logic hiện đại, có thể xem như một lời cảnh báo liên kết liên quan
  • Có lẽ điều thú vị hơn là tìm cách vẽ toàn bộ cấu trúc lập luận của một chủ đề như một tấm bản đồ; ví dụ bắt đầu từ câu hỏi lớn như “Chúa có tồn tại không?”, rồi triển khai có hệ thống các luận cứ ủng hộ, phản đối, các phản biện đối với chúng, và cả phản biện đối với phản biện; với mỗi khẳng định, trích dẫn kiểu “Plato đã đưa ra lập luận này” sẽ được dùng không phải như bằng chứng mà như ngữ cảnh lịch sử; điều cốt lõi không phải là phân thắng bại mà là tạo ra một bản đồ lập luận để tránh cứ xoay vòng quanh cùng một điểm tranh luận
• Tôi đang tự hỏi có phải rốt cuộc ta đang xây dựng một dạng từ điển chứng minh, bắt đầu từ vài chân lý hiển nhiên, rồi chất chồng các chứng minh khác lên trên một cách logic; khi đó các chứng minh mới chỉ đơn giản là tổ hợp logic của các chứng minh đã có; tôi rất muốn ai đó biến thứ này thành một game phong cách Zachtronics! Có một game tên là Euclidea mang lại cảm giác tương tự trong lĩnh vực hình học, và ý tưởng xây cả một tòa tháp logic như vậy thật sự rất cuốn hút; không biết có phải toán học thuần túy thực chất chính là như vậy không, và các giáo sư toán thuần có cảm thấy hưng phấn khi mở rộng “từ điển logic” này không; tôi cũng nhớ mang máng là có một nhà toán học nổi tiếng từng lập ra một danh sách các chứng minh nền tảng, nên nếu ai biết đó là ai (hay cái gì) và nó được gọi là gì thì rất mong được chỉ giúp; chắc có lẽ đó là các tiên đề (axioms)
  • Thật ra đã có một trò chơi liên quan, dù có thể không hoàn toàn đúng thứ bạn muốn (và nó không phải game xây toàn bộ toán học); tôi đã chơi thử và thấy khá vui; đó chính là leanprover-community/nng4 được nhắc đến trong bài này
  • Về ý “hãy làm nó thành game phong cách Zachtronics”, có thể nói toán học chính là game đó (nói đùa một chút thôi), nhưng tôi nghĩ phiên bản game hóa thực sự cũng sẽ rất vui; toán học thuần túy quả thực là một hệ thống như vậy; ở bậc đại học cảm giác đó khá đúng, còn lên tới nghiên cứu bài báo thì hơi khác; nếu bạn muốn cảm giác như chơi game, tôi khuyên thử giáo trình đại số trừu tượng như Dummit and Foote, phần chứng minh trong đó có niềm vui kiểu game; mà các sách nổi tiếng thì nếu bí quá thường cũng có lời giải trên mạng
  • Có thể bạn đang nói đến các tiên đề của Euclid, tức là một hệ thống nơi các khái niệm như điểm, đường thẳng, mặt phẳng, đường song song được định nghĩa; trên mặt cầu thay vì mặt phẳng thì hệ này bị phá vỡ; hoặc cũng có thể bạn đang nhắc đến lý thuyết tập hợp Zermelo-Fraenkel (ZF/ZFC), nền tảng mà toán học hiện đại được xây dựng trên đó
  • Cũng có một game tên là Bombe, một biến thể của Minesweeper; thay vì trực tiếp mở ô, bạn chơi bằng cách tạo ra các quy tắc kiểu “khi nào thì có thể cắm cờ”; lên cấp cao hơn, các quy tắc này liên kết với nhau như các lemma (bổ đề); khi kỹ năng người chơi tăng lên thì còn có thể nới lỏng ràng buộc của bộ công cụ để khái quát hóa hơn nữa liên kết game
  • Về bản chất, toán học là quá trình bắt đầu từ các tiên đề rồi suy ra kết luận; dĩ nhiên có lẽ không chỉ có thế, nhưng ở trình độ của tôi thì tôi đang hiểu như vậy
• Hơi bắt bẻ một chút thôi, nhưng việc nói định lý two_eq_two trông như một hàm thì khá kỳ; vì nó không có đối số nên đúng hơn là gần với một hằng số hơn (dù tất nhiên tôi biết hằng số cũng là hàm không đối số); có lẽ sẽ thuyết phục hơn nếu dùng x_eq_x để rồi áp dụng như một hàm trong 2_eq_2, như dưới đây

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Ở đây x_eq_x trông giống một hàm, và trong 2_eq_2 nó thực sự được dùng theo cách đó
  • Nhận xét đó đúng đấy! Lý do tôi không làm vậy là vì cách Lean xử lý đối số (đặc biệt là các khái niệm như dependent types — đưa vào x thì trả về chứng minh x = x) với tôi vẫn còn khá lạ, lại là một chủ đề đáng được tách riêng ra, nên tôi dự định sẽ nói trong bài tiếp theo
• Điều tôi thấy khó khi học Lean là các tactics (rfl chẳng hạn) quá bao quát, nên ngay cả học qua tutorial cũng khó nắm chính xác ý nghĩa; ví dụ trong C thì có thể lần theo sự thay đổi trạng thái tới tận mức bit, còn Lean thì có gì đó hơi mơ hồ; với cả cú pháp tactic rewrite (rw) cũng khiến tôi thấy không tự nhiên
  • Tôi cũng luôn thấy khó làm quen với tactics trong Coq (giờ là Rocq); chẳng hạn tôi từng có trường hợp có “A = B” và “P(A,A)” nhưng muốn chuyển thành “P(A,B)” thì rewrite lại không hoạt động vì những lý do khó giải thích (có lẽ liên quan đến định nghĩa của cấu trúc trung gian); trong khi đó Metamath và cơ sở dữ liệu set.mm thì buộc bạn chứng minh hoàn toàn bằng suy luận cụ thể, không có tactic nào cả (chỉ dùng các quy tắc suy diễn như ax-mp), nhưng đổi lại lại phải nhớ hàng loạt utility lemma nên cũng không hề dễ
  • Đó cũng là một trong những lý do tôi thích Agda hơn; Agda hầu như không có tactic, và dùng Curry-Howard correspondence để viết trực tiếp proof term như đang viết bằng một ngôn ngữ lập trình hàm; bù lại, nếu lười trừu tượng hóa và tạo hàm thì ngay cả những thứ tầm thường cũng sẽ trở nên cực kỳ phiền phức, nên tính kỷ luật rất quan trọng
  • Ít nhất trong Lean, bạn có thể "go to definition" để xem cách tactic được định nghĩa và hoạt động bên trong; khi mới học thì số lượng thứ phải xem khá choáng ngợp, nhưng cuối cùng vẫn có thể lần hết được (dù đi sâu đến tận lý thuyết kiểu cơ bản thì lại hơi khó hình dung), và bạn nói cú pháp rewrite không tự nhiên, vậy thì tôi khá tò mò không biết một cú pháp rewrite “tự nhiên” sẽ trông như thế nào
  • Điều khiến tôi thấy thú vị là tất cả tactics đều là mã ở “mức người dùng”, nằm ngoài kernel cốt lõi của hệ chứng minh; điều đó hợp lý vì ta muốn giữ kernel nhỏ và đã được kiểm chứng mà không phải sửa đổi, nhưng cũng có nghĩa là khi tactics được nâng cấp hay chỉnh sửa thì các chứng minh cũ có thể bị hỏng; tôi khá tò mò ngoài thực tế chuyện đó gây vấn đề đến mức nào
  • Trái với kỳ vọng của tôi, trong Lean có vẻ reflection và rewrite còn cơ bản hơn cả addition; Lean có addition dựng sẵn nhưng dường như vẫn phải viết rfl hoặc rewrite đi lặp lại; có thể Lean có thứ gì đó như prelude để tự động hóa phần này chăng
• Tôi đang thắc mắc có cách nào để đọc proof trong Lean theo kiểu noninteractive, không phải bấm từng bước, hay không; khi chơi natural number game, proof chỉ toàn là chuỗi lệnh kiểu rw [x] nên rất khó đọc; đúng là trong editor có thể xem trạng thái từng dòng, nhưng cứ phải bấm liên tục thì mất mạch, giống như nếu Python mà không có thụt đầu dòng, chỉ có cấu trúc khối rồi bắt bạn nhấp từng chỗ để hiểu luồng thì cũng vậy; có thể do góc nhìn của tôi bị ảnh hưởng bởi việc đầu game chỉ có ít lệnh bị giới hạn, nhưng tôi vẫn muốn biết trong môi trường Lean đầy đủ thì luồng đó có đỡ hơn không

  • Có cách nào để đọc chứng minh trong Lean theo kiểu noninteractive không?
    Tôi cũng mới tò mò về chuyện này gần đây nên đã tìm thử; blog lean-in-latex có đưa ra một cách giúp theo dõi luồng đó bên ngoài editor mà không cần nhấp, và cũng cho thấy cộng đồng Lean tiếp cận chuyện này như thế nào

  • Rocq trước đây từng có cái gọi là “ngôn ngữ chứng minh toán học”; khó tìm ví dụ dùng thực tế, nhưng đại khái nó trông như sau

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    Cách tiếp cận này giúp nó đọc giống như “chứng minh viết tay” trong bài báo, nhưng vì gần như không ai dùng nên đã biến mất; ngôn ngữ chứng minh Isar của Isabelle cũng tương tự, thậm chí còn gần với cách chuẩn hơn, ví dụ:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Bạn có thể viết rõ toàn bộ cấu trúc logic và các kết quả trung gian, rồi chỉ rút gọn bằng by ... ở những chỗ mà chi tiết không quá quan trọng; tôi không biết Lean có thứ tương tự không, nhưng ít nhất đây cũng là vài từ khóa tìm kiếm hoặc chủ đề để hỏi trên diễn đàn Lean
  • Câu hỏi thực sự rất hay! Tôi vẫn còn là người mới nên chưa dám khẳng định hoàn toàn, nhưng xin chia sẻ cảm nhận của mình; sau khoảng hai tháng dùng Lean, tôi thấy việc đọc mã chứng minh khác với đọc mã lập trình, nó giống “quét” hơn là “đọc” tuần tự; bạn chú ý tới cấu trúc lập luận tổng thể, tactic nào được dùng, lemma nào được gọi; trong mã Lean thực tế, mỗi goal mới thường được thụt vào, xong goal thì lại lùi ra, nên hình dạng của lập luận rất quan trọng để đọc; có thể xem ví dụ PR của tôi; khi đã quen với tactics, bạn sẽ nhìn intro là biết đang đi vào quantifier, nhìn constructor là biết đang tách goal, v.v.; rốt cuộc tactics là một macro/DSL tạo ra proof tree (term tree), và khi nhìn mã chứng minh tôi cảm giác như đang thao tác trên một cái cây (chia nhánh, điền các chỗ trống theo thứ tự, v.v.); dù vậy, việc phải nhấp để biết chính xác assertion ở giữa chứng minh vẫn là một hạn chế; một chứng minh có ý tưởng tốt thì có thể đọc rõ ràng giống như diễn tiến logic trong một bài báo, nên người muốn truyền đạt ý đồ thường sẽ viết tên dễ hiểu, trình bày mạch lạc, tách lemma nhỏ, và đưa giả thuyết lên trước rồi giải bằng đoạn proof ngắn; ngược lại, những phần mà về mặt máy móc thì dài dòng nhưng với nhà toán học lại quá hiển nhiên thường được xử lý kiểu “golfing” (viết ngắn nhất có thể); kiểu golf đôi khi làm mã ngắn hơn bằng cách chỉ nói tới những phần mà con người đã trực giác nắm được; tóm lại, cấu trúc khi đọc Lean thường là ngầm định, nhưng có thể làm cho rõ hơn, và khi bạn quen tactic hơn thì cũng sẽ nắm được cấu trúc tốt hơn mà không cần nhấp; chỉ cần lướt tên lemma cũng có thể thấy dòng chảy lớn, và thứ tự thường cũng dễ tái dựng
• Nội dung thực sự rất hay, tôi nghĩ hiếm có ai giải thích được những thứ như vậy theo cách dễ tiêu hóa; bí quyết là chỉ ra tất cả những bước nhỏ mà chuyên gia thường bỏ qua
  • Cảm ơn!
• Không biết trong chủ đề này có ai có ý kiến về tương lai của Lean so với idris/coq/agda không; tôi muốn học biểu diễn tri thức, nhưng trước khi đào sâu bất kỳ thứ gì thì tôi khá lo về quy mô cộng đồng và rủi ro tương lai; trước đây tôi từng đầu tư thời gian vào clojure core.logic rồi bị hụt hẫng vì mức độ quan tâm quá thấp/cộng đồng quá nhỏ, nên giờ hơi ngại bắt đầu
  • Theo trải nghiệm thực tế của tôi thì Lean và Coq/Rocq được dùng nhiều hơn Idris và Agda khá rõ, thư viện và cộng đồng cũng lớn hơn; Rocq chủ yếu được dùng cho kiểm chứng chương trình, chắc một phần vì nó có lịch sử lâu hơn và cũng có nhiều nét đặc thù, nhưng Lean có thể sẽ sớm đuổi kịp; Lean hiện là lựa chọn phổ biến nhất cho việc chứng minh định lý toán học; các dự án nổi tiếng của Rocq có CompCert, CertiCoq, seL4, và còn có các trường hợp dùng trong kiểm chứng phần mềm máy bay ngoài đời thực (xem danh sách dự án đã tổng hợp); phía Lean có mathlib (bộ sưu tập chứng minh toán học), Định lý cuối cùng của Fermat (dự án chứng minh FLT), PFR và nhiều dự án quy mô lớn khác; theo tôi biết thì Idris và Agda chưa có nhiều dự án “thế giới thực”, dù có thể tôi nhớ chưa chuẩn; tất cả các cộng đồng này đều vẫn rất nhỏ nếu so với C++ hay JavaScript, và thực tế kiểm chứng chương trình là một công việc rất chậm và khá tẻ nhạt; có lẽ về lâu dài sẽ có thay đổi nền tảng nào đó nhờ AI, nhưng những kỹ năng bạn học được vẫn sẽ hữu ích
  • Tôi nghĩ thật ra không nên “đặt cược” vào lĩnh vực này; trên thực tế đa số nhà toán học không quá quan tâm đến formalization (hình thức hóa), vì khoảng cách giữa chứng minh viết tay và cú pháp nghiêm ngặt mà máy tính đòi hỏi là rất lớn; cứ tiếp cận nó như một thứ đáng học và đáng thực hành vì vui là được; còn về triển vọng tương lai, gần đây Lean có vẻ năng động nhất, nhưng mỗi hệ đều có một tệp người dùng lâu năm riêng nên cũng khó mà kết luận trước
• Tôi đang tò mò liệu chỉ cần ném ngẫu nhiên gì đó vào Lean, không dùng mẹo hay kỹ thuật gì, rồi dựa vào việc Lean chấp nhận hay không, có thể dẫn tới những phát hiện thú vị không; hoặc có thể tự động hóa việc này bằng hệ thống tự động hay llm để thử hàng loạt chứng minh/lý thuyết khó hiểu rồi xem cái nào thành công không? Câu hỏi có thể hơi ngô nghê, vì tôi mới chỉ hiểu Prolog ở mức rất sơ sài
  • Với tư cách là người làm certified programming chuyên nghiệp, tôi nghĩ AI sinh sinh và formal methods là một cặp kết hợp tuyệt vời; việc LLM có thay thế được lập trình viên hay không có lẽ cũng phụ thuộc vào chuyện AI có thể kết hợp tốt thế nào với certified programming và suy luận tổ hợp,

    Nếu chỉ ném ngẫu nhiên vào thì có thể có phát hiện thú vị không?
    AI truyền thống làm tốt ở các bài toán có không gian trường hợp nhỏ như cờ caro; cờ vua đã khó hơn đôi chút, còn cờ vây thì với AI phi học máy gần như là bất khả thi; ngôn ngữ hình thức có số lượng trường hợp và trạng thái tìm kiếm lớn đến mức khó tưởng tượng; nếu bản chất bài toán đủ rõ thì có thể brute force bằng SMT solver; ban đầu SMT solver và proof assistant là hai nhánh formal methods khác nhau, nhưng giờ chúng đang ngày càng bổ trợ cho nhau (xem Sledgehammer, Lean-SMT)
    Nếu dùng llm hay hệ tự động để thử các chứng minh/lý thuyết ngẫu nhiên thì sao?
    Hướng này chưa hẳn là dòng nghiên cứu chủ lưu, nhưng đã có rất nhiều thử nghiệm; ngay cả trước làn sóng LLM cũng đã có nhiều năm được các nhà tài trợ lớn rót vốn; từng có những nỗ lực như “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies”, và gần đây hơn là DeepSeek-Prover; hiện vẫn hoàn toàn bỏ ngỏ việc nên huấn luyện thế nào và giới hạn tương lai của nó sẽ đi đến đâu,
    Các LLM hiện tại vẫn còn khá yếu với ngôn ngữ Rocq và Lean, và khi chúng trả lời sai thì việc sửa lại rất đau đớn; dù vậy, tôi vẫn kỳ vọng rằng theo thời gian chất lượng của các công cụ AI sẽ tăng lên rất nhiều

  • Đây thực sự là một lĩnh vực nghiên cứu và thử nghiệm rất sôi động!
    Cộng đồng Lean tập trung khá đông trên Zulip, và bạn có thể xem nhiều luồng tham khảo trong kênh Machine-Learning-for-Theorem-Proving
• Là người lần đầu quan tâm đến Lean sau khi xem alphaproof, tôi thấy bài giới thiệu này quá tuyệt; không biết bạn có thể chia sẻ mình đang làm gì với Lean không?
  • Hiện tại tôi chỉ đang học toán bằng Lean; cụ thể là đi theo giáo trình Lean của Tao, và tự điền vào các chỗ sorry còn để trống trong phần bài tập (các lời giải của tôi ở đây)
• Tôi đang thắc mắc liệu Lean có chế độ xác minh nào để tự động ngăn việc dùng chứng minh không đáng tin (proof với sorry) hoặc cứ thêm tiên đề mới hay không; ví dụ có kiểm tra được kiểu “chứng minh này hoàn toàn không dùng sorry theo bất kỳ cách nào” hoặc “nó chỉ phụ thuộc vào sức mạnh chứng minh của một tập tiên đề cố định” không?
  • Có lẽ ví dụ #print axioms some_theorem được nhắc ở phần cuối bài chính là thứ bạn đang tìm; với nó, bạn có thể biết chứng minh đó phụ thuộc trực tiếp hay gián tiếp vào sorry hoặc các tiên đề chưa được kiểm tra hay không
  • Có thể dùng print axioms để kiểm tra xem có tiên đề bổ sung nào không, và đồng thời xem nó có biên dịch được mà không có warning hay error không; tiện ích SafeVerify còn bắt được cả một số mẹo mà các hệ RL từng tìm ra
  • Ngoài ra, điều này cũng có thể làm bằng macro, như được nói ở đây