Lean 4: Ngôn ngữ lập trình chứng minh định lý hiện đại
Lean 4 là hệ thống chứng minh định lý và ngôn ngữ lập trình được phát triển bởi Leonardo de Moura tại Microsoft Research. Với triết lý “toán học có thể tính được”, Lean 4 kết hợp giữa trợ lý chứng minh hình thức và ngôn ngữ lập trình hàm thuần khiết. Đây là công cụ đột phá cho toán học và khoa học máy tính.
Lean 4 là gì?
Lean 4 là thế hệ thứ tư của hệ thống Lean, ra mắt năm 2021. Khác với Lean 3 (chủ yếu là trợ lý chứng minh), Lean 4 là một ngôn ngữ lập trình hoàn chỉnh:
- Turing-complete: có thể tính toán mọi thứ mà ngôn ngữ lập trình thông thường làm được
- Hệ thống kiểu phụ thuộc: kiểu dữ liệu có thể phụ thuộc vào giá trị
- Tactic-based proof: chứng minh bằng chiến thuật, gần gũi với lập trình
- Compiler front-end: biên dịch hiệu quả, tích hợp tốt với hệ sinh thái
Lean 4 Official Site cung cấp tài liệu và môi trường thử nghiệm trực tuyến.
Tại sao Lean 4 quan trọng?
Toán học hình thức (formal mathematics) là việc chứng minh định lý bằng máy tính. Lean 4 làm cho điều này khả thi ở quy mô lớn:
- mathlib: thư viện toán học lớn nhất trong bất kỳ hệ thống chứng minh nào, với hàng chục nghìn định lý đã chứng minh
- Feit-Thompson theorem: một trong những định lý phức tạp nhất toán học đã được chứng minh hoàn chỉnh bằng Lean
- Xử lý song song: Lean 4 hỗ trợ đa luồng và lập trình đồng thời tốt hơn Lean 3
Năm 2023, nhóm phát triển đã chứng minh Odd Order Theorem (định lý nhóm Feit-Thompson) trong Lean 4 — một cột mốc lịch sử.
Cú pháp và ví dụ cơ bản
Lean 4 có cú pháp ngắn gọn, gần giống Python nhưng mạnh mẽ hơn nhiều:
def greet : String := "Hello, Lean 4!"
theorem and_comm (P Q : Prop) : P ∧ Q → Q ∧ P := by
intro h
exact And.intro h.right h.left
structure Point where
x : Nat
y : Nat
#eval Point.mk 3 4
Trong ví dụ trên, theorem khai báo chứng minh, by bắt đầu tactic proof, intro đưa giả thiết vào, exact hoàn thành chứng minh. Lean 4 cũng có structure để định nghĩa kiểu dữ liệu.
Hệ thống kiểu và proof với dependent type
Điểm mạnh cốt lõi của Lean 4 là hệ thống kiểu phụ thuộc:
- Prop và Type: Prop là kiểu logic (mệnh đề), Type là kiểu dữ liệu. Mọi mệnh đề đều là kiểu, mọi kiểu đều là mệnh đề.
- Sigma types:
Σ (x : α), β xcho phép kiểu phụ thuộc vào giá trị - Pattern matching: khớp mẫu mạnh với inductive types
- Auto-derivation: Lean 4 tự động suy luận kiểu phức tạp
Tactic language và chứng minh tương tác
Tactic là cách viết chứng minh từng bước:
theorem add_zero (n : Nat) : n + 0 = n := by
induction n
· simp
· simp [*, Nat.succ_eq_add_one]
Trong ví dụ, induction là tactic chia trường hợp. simp đơn giản hóa biểu thức. Lean 4 có hàng trăm tactic tích hợp sẵn, từ cơ bản đến nâng cao như ring, omega, linarith.
Ứng dụng thực tế
Lean 4 không chỉ là công cụ lý thuyết:
- Verified compilers: dự án Cicada – compiler cho Lean 4 đã được chứng minh đúng
- Cryptography: chứng minh bảo mật giao thức mã hóa
- AI/ML: xác minh tính đúng đắn của model và thuật toán học máy
- Toán học: cộng đồng mathlib đang số hóa toán học hiện đại
Nhiều trường đại học đã bắt đầu giảng dạy Lean 4, bao gồm MIT, Caltech, và Đại học Oxford.
Bắt đầu với Lean 4
- Truy cập Live Lean 4 để thử nghiệm trực tuyến
- Cài đặt qua
elantool quản lý phiên bản Lean - Đọc Theorem Proving in Lean 4 — sách hướng dẫn chính thức
- Khám phá mathlib4 để xem các chứng minh thực tế
Nhiều trường đại học đã bắt đầu giảng dạy Lean 4, bao gồm MIT, Caltech, và Đại học Oxford. Khóa học Pierce’s course tại UPenn là điểm khởi đầu phổ biến.
So sánh với các hệ thống khác
Lean 4 so với Coq, Isabelle, Agda:
- Lean vs Coq: Lean 4 có cú pháp dễ đọc hơn, hệ thống macro mạnh hơn, hiệu suất biên dịch tốt hơn
- Lean vs Isabelle: Isabelle dễ học hơn nhưng Lean có cộng đồng năng động hơn và hệ sinh thái phong phú
- Lean vs Agda: Agda thiên về lập trình hàm, Lean cân bằng giữa lập trình và chứng minh
Kết luận
Lean 4 đại diện cho bước tiến lớn nhất trong toán học hình thức. Kết hợp ngôn ngữ lập trình mạnh mẽ với hệ thống chứng minh đáng tin cậy, Lean 4 mở ra cánh cửa cho việc xác minh mọi thứ — từ chương trình máy tính đến định lý toán học. Cho developer quan tâm đến tính đúng đắn tuyệt đối, Lean 4 là công cụ đáng học.
