Giới thiệu Lean: Ngôn ngữ lập trình để chứng minh định lý toán học

Lean là một trợ lý chứng minh định lý (proof assistant) giúp kết nối giữa lập trình và toán học thông qua đối ứng Curry-Howard. Bài viết này sẽ hướng dẫn lập trình viên cách tiếp cận Lean, từ cú pháp cơ bản đến các khái niệm như kiểu phụ thuộc và chiến thuật chứng minh, đồng thời xem xét vai trò của AI trong lĩnh vực này.

Là một kỹ sư phần mềm chuyển sang làm khoa học dữ liệu, tôi làm việc hàng ngày với các thuật toán học máy (machine learning). Tôi bị cuốn hút bởi vẻ đẹp huyền ảo của chúng cũng như nền tảng toán học bên dưới. "Mổ xẻ" bất kỳ thư viện học máy nào, bạn sẽ thấy những mẹo toán học liên quan đến phân tích ma trận, tích chập, đường cong Gauss và nhiều thứ khác. Những thứ này lại được xây dựng dựa trên các tiên đề và quy tắc cơ bản hơn, như việc áp dụng hàm và logic.

Trong hành trình tìm hiểu những nguyên thủy này, tôi đã sưu tập cả một giá sách toán học, nhiều cuốn trong số đó giờ đây đang nằm im thu bụi. Tôi cũng đã học tại Đại học Mở, nơi tôi tham dự các lớp học trên Zoom và tìm hiểu về cú pháp cũng như tiên đề, sau đó là cách kết hợp chúng để xây dựng các định lý.

Chủ đề này thật hấp dẫn: các tiên đề giống như các quân cờ và các nước đi hợp pháp trên bàn cờ, trong khi các định lý là những nước đi chơi hợp lệ, một số thú vị hơn những cái khác. Chứng minh một định lý có nghĩa là giải trình tự nước đi vừa đủ để thuyết phục người chơi rằng nó có thể đạt được, hoặc bác bỏ nó bằng cách chỉ ra sự không thể.

Kiến trúc lõi của AlphaProof

Tuy nhiên, trên thực tế, các khóa học lại khá tẻ nhạt. Tôi được đưa các file PDF để giải bằng tay và sau đó gửi bản quét công việc của mình lên mạng. Trong khi loay hoay viết chì trên giấy, vật lộn với các bài tập khóa học, tôi có hai nhận thức:

Xây dựng một chứng minh cũng giống như lập trình.
Tôi không thể tiếp cận toán học trong những điều kiện của thế kỷ 21 này. Tôi cần một IDE, với gợi ý kiểu (type hints), tô sáng cú pháp và thông báo lỗi mô tả, và tương tác với nó một cách trực tiếp.

Tư duy của tôi không hề mới. Ý tưởng đầu tiên được gọi là đối ứng Curry-Howard (Curry-Howard correspondence), sẽ được giải thích bên dưới. Ý tưởng thứ hai là mục tiêu của các trợ lý chứng minh như Lean và các tiện ích mở rộng IDE của chúng (thường là tiện ích mở rộng VS Code).

Trợ lý chứng minh tương tác so với Trình chứng minh định lý tự động

Các trình kiểm tra định lý như nhân (kernel) của Lean có thể xác định xem các biểu thức có được hình thành tốt không, các bước có hợp pháp không và kết luận cuối cùng có hợp lệ không. Trợ lý chứng minh tương tác dựa trên chúng và cũng giúp bạn xây dựng các chứng minh cũng như gợi ý các bước. Trình chứng minh định lý tự động (ATP) cố gắng tìm chứng minh bằng chính nó bằng các kỹ thuật AI. Lean hoạt động như một trình kiểm tra và trợ lý chứng minh, nhưng nó kết hợp tốt với AI tạo sinh để hoạt động hiệu quả như một ATP.

Terence Tao đã phát trực tiếp các chứng minh hỗ trợ bởi AI trên kênh YouTube của mình bằng cách sử dụng Lean 4 và GitHub Copilot. Hầu hết các tiêu đề dưới dạng "AI vừa giải quyết một vấn đề mở tồn tại x năm" có khả năng đã được chính thức hóa bằng Lean (ví dụ 1, 2 và 3). Các dự án và điểm chuẩn AI như LeanDojo, miniF2F, ProofNet, PutnamBench, FormalMATH đều sử dụng Lean. OpenAI và Meta đã đào tạo các mô hình để sử dụng Lean, và AlphaProof của DeepMind đã sử dụng nó để giành được huy chương bạc tại Olympic Toán học Quốc tế.

Đối ứng Curry-Howard

Hãy bắt đầu với một định lý logic đơn giản, một cái mà bạn có thể phải chứng minh trong lớp logic đại học:

(P → Q → R) → (P ∧ Q → R)

Toán tử → biểu thị hàm ý logic, nhưng trong đối ứng Curry-Howard giữa các chứng minh và các chương trình máy tính, nó có thể được đọc là một hàm. ∧ là "và" logic. Tiếng Việt đơn giản là: "Nếu tôi có một hàm mà, cho P, tạo ra một hàm từ Q đến R, thì nếu tôi đã có cả P và Q rồi, tôi có thể tạo ra R".

Hãy tưởng tượng điều này với một ví dụ cụ thể: Nếu tôi có một máy bán nước tự động mà cho một đồng xu (P) trả lại một cốc mì ăn liền (Q → R), cái mà khi có nước nóng (Q) trả lại mì (R), điều đó có nghĩa là tôi có thể tạo ra một hệ thống mà cho cả đồng xu và nước nóng (P ∧ Q) làm đầu vào, tôi có thể trả lại mì.

Máy bán mì Cup Noodle

Nếu bạn được yêu cầu chứng minh rằng điều này là khả thi với tư cách là một lập trình viên, bạn có thể muốn làm điều đó bằng cách viết một hàm phù hợp với kịch bản này. Trong TypeScript, chúng ta có thể viết như sau:

declare const P: unique symbol;
declare const Q: unique symbol;
declare const R: unique symbol;

type Coin = { [P]: never };
type HotWater = { [Q]: never };
type Noodles = { [R]: never };

function theorem(
  f: (c: Coin) => (h: HotWater) => Noodles
): (input: [Coin, HotWater]) => Noodles {
  return (input) => f(input[0])(input[1]);
}

Chúng ta đã định nghĩa một hàm — định lý của chúng ta — nhận một hàm currying (P → Q → R) làm tham số và xuất ra một hàm nhận kiểu product P ∧ Q và xuất ra R, tức là (P ∧ Q → R). Hàm này đóng vai trò là "chứng nhân" rằng định lý logic là đúng. Chứng minh nghe có vẻ hợp lý và nó thậm chí còn thỏa mãn các kiểu dữ liệu mô tả định lý gốc trong TypeScript.

Hãy nói điều này mạnh mẽ hơn: Chứng minh là hợp lý vì nó thỏa mãn kiểu dữ liệu. Các mệnh đề là kiểu (types), và các chứng minh là các thuật ngữ (terms) của những kiểu đó. Chúng ta cũng thấy rằng các liên từ ∧ là kiểu product / tuple, và các hàm ý logic Q → R là các hàm. Mũi tên tương đương nhau cả về mặt cú pháp và ngữ nghĩa.

Hãy triển khai điều này trong Lean:

example (f : P → Q → R) (pair : P ∧ Q) : R :=
  f pair.left pair.right

example là một cách để định nghĩa các khai báo ẩn danh chỉ để kiểm tra kiểu (khác với từ khóa theorem), và kiểu của nó (điều theo sau dấu hai chấm : đến định nghĩa :=) là định lý của chúng ta. Chứng minh đạt được khi một định nghĩa "cư ngụ" (inhabit) trong kiểu này.

Những khái niệm nâng cao bạn chưa thấy

Kiểu phụ thuộc (Dependent Types)

Hãy xem xét kiểu sau phức tạp hơn một chút:

∀ x : Nat, 0 ≤ x

Nó có nghĩa là: "Với mọi giá trị (∀) của x là số tự nhiên, 0 nhỏ hơn hoặc bằng x." Điều đầu tiên chúng ta nhận thấy là các ký hiệu toán học Unicode; chúng có thể được tự động hoàn thành trong IDE bằng \forall hoặc đơn giản là thay thế bằng từ khóa ASCII forall.

Điều này khiến chúng ta ngạc nhiên vì nó không giống một kiểu. Kiểu phụ thuộc vào giá trị của x — điều mà chúng ta thường nhận được từ các thư viện xác thực phức tạp như Zod, chứ không phải từ các trình kiểm tra kiểu tĩnh như TypeScript. Đó là một kiểu "phụ thuộc" vào các giá trị. Tuy nhiên, các kiểu của Lean không dựa vào các kiểm tra thời gian chạy (runtime) theo cách Zod làm; nó vẫn là một kiểu, dù có phức tạp.

Các vũ trụ (Universes)

Trong sân chơi hoặc IDE, chúng ta có thể kiểm tra kiểu của các thuật ngữ với #check:

#check 3 -> Nat

Bây giờ hãy kiểm tra kiểu của Nat:

#check Nat -> Type

Type là một kiểu của Type 1, và cứ thế. Điều này cho thấy không có sự phân biệt cú pháp cứng nhắc giữa các kiểu và các thuật ngữ trong Lean. Các kiểu là các thuật ngữ có kiểu của riêng chúng, xếp chồng lên nhau như các lớp của hành tây — các lớp này được gọi là "vũ trụ" (universes). 3 là một thuật ngữ của kiểu Nat và Nat là một thuật ngữ của kiểu Type, Type n có kiểu Type (n+1), v.v.

Lean phải theo dõi các cấp độ vũ trụ để tránh nghịch lý người cạo râu: "Một người cạo râu cạo cho tất cả những người không tự cạo râu cho mình, thì người cạo râu có tự cạo râu cho mình không?" Với các vũ trụ kiểu, người cạo râu là một quy trình có kiểu chỉ có thể hoạt động trên các phần tử của một kiểu từ một vũ trụ dưới nó, nó không thể hoạt động trên các phần tử ở cấp độ của chính mình, bao gồm cả bản thân anh ta.

Các mệnh đề (Propositions)

Hãy thử một kiểu khó hơn nữa:

∀ x y z n : Nat, n > 2 → x * y * z ≠ 0 → x^n + y^n ≠ z^n

Tiếng Việt đơn giản: "Điều này có đúng không? Với mọi số tự nhiên x, y, z và n, cho một chứng minh rằng n > 2 và x * y * z ≠ 0, chúng ta có thể tạo ra một chứng minh rằng x^n + y^n ≠ z^n".

Đây là Định lý Cuối cùng của Fermat, đã làm các nhà toán học đau đầu trong 358 năm sau khi Fermat tuyên bố chứng minh của riêng mình không vừa với lề trang giấy. Định nghĩa sử dụng sorry là một chỗ giữ chỗ cho một chứng minh chưa hoàn chỉnh. Nó sẽ biên dịch nhưng sẽ báo cho bạn: declaration uses 'sorry'. Cảm giác như sử dụng any của TypeScript để tắt tiếng các lỗi kiểu, nhưng một người đánh giá có thể nhận thấy và yêu cầu bạn sửa lỗi lint. Cung cấp chứng minh này là "mục tiêu" của bạn.

Chiến thuật (Tactics)

Trước đó, chúng ta đã giải ví dụ máy bán nước tự động chỉ bằng cách áp dụng hàm, nhưng có nhiều nguyên thủy thú vị hơn trong Lean. Trong Lean, bạn có thể bắt đầu chứng minh của mình bằng by kích hoạt chế độ "tactic":

example (f : Coin → HotWater → Noodles) : Coin ∧ HotWater → Noodles := by
  intro pair
  exact f pair.left pair.right

Điều này cho phép bạn xây dựng chứng minh từng bước một, trong khi ngăn bên phải của IDE (InfoView) dần dần hiển thị các giả định cục bộ và mục tiêu của bạn, được đánh dấu bằng ⊢. Các chiến thuật là sự kết hợp giữa macro và đường cú pháp giúp giải quyết trạng thái chứng minh cho nhân ngôn ngữ kiểm tra kiểu. Chúng giúp bạn suy nghĩ một cách phân tích và khai báo khi giải quyết các mục tiêu của mình.

Huấn luyện viên thảo luận chiến thuật với đội

Bạn sẽ phải làm quen với các chiến thuật giống như một người học SQL làm với các cấu trúc phân tích như GROUP BY, PIVOT và LEFT JOIN. Một số chiến thuật giúp phân tách mục tiêu thành các nghĩa vụ nhỏ hơn, chẳng hạn như intro, cases, constructor, apply hoặc refine. Những chiến thuật khác viết lại biểu thức bằng cách sử dụng các giả định về sự tương đương, chẳng hạn như rw hoặc simp.

Suy nghĩ theo các chiến thuật là một kỹ năng thanh lịch chỉ có thể đến từ kinh nghiệm. Để sử dụng lại một ẩn dụ trước, nó giống như một nhà phân tích dữ liệu kéo lên đúng các hàm phân tích và dễ dàng làm sạch, làm phong phú và tóm tắt các bảng — hoặc một kỹ sư phần mềm cao cấp nối các lệnh Bash đúng cách hoặc nhận ra mẫu thiết kế sạch nhất cho công việc.

Kết luận

Lean có đường cong học tập dốc, một phần do cú pháp và việc sử dụng các chiến thuật mà bạn phải học. Tuy nhiên, sự vất vả với Lean đi kèm một phần thưởng: bạn đang học toán học. Các kiểu, vũ trụ, chiến thuật, định lý và chứng minh không phải là những kỳ quặc của một ngôn ngữ lập trình khác mà là các khái niệm mà các nhà toán học và logic học đã vật lộn trong nhiều thế hệ.

Khi bạn đã nắm vững các nguyên tắc cơ bản, hãy thử chuyển sang các chủ đề nâng cao hơn với Mathematics in Lean, nơi bạn sẽ giải quyết các vấn đề trong toán học rời rạc, đại số tuyến tính, giải tích vi phân và tô pô. Hoặc đi sâu vào nền tảng bắt đầu từ số không (theo nghĩa đen) thông qua người bạn đồng hành Lean của Tao cho cuốn sách "Analysis I". Mathlib, thư viện cộng tác của Lean, đã có 1,6 triệu dòng toán học được chính thức hóa mà bạn có thể sử dụng để kết nối với tất cả các nhánh của toán học.