Nền tảng toán học

Chứng minh hình thức (Lean)

Phần mềm chứng minh như Lean kiểm tra một chứng minh toán học giống cách trình biên dịch kiểm tra một chương trình: quy câu hỏi "chứng minh này đúng không?" về việc kiểm tra phán đoán kiểu $\Gamma \vdash t : P$ , do một hạt nhân tin cẩn nhỏ xác nhận.

Trực giácVì sao tin một chứng minh bạn không đọc hết được?

Mathlib, thư viện toán học của Lean 4, hiện có tới hàng triệu dòng chứng minh — nhiều hơn bất kỳ ai có thể đọc hết từng dòng. Nhưng các nhà toán học vẫn tin nó, giống như ta tin con dấu kiểm định thang máy chứ không tự hàn lại từng sợi cáp: một quy trình kiểm tra nhỏ, cố định (hạt nhân) đã xác nhận từng bước một, và hạt nhân đó đủ ngắn để soát bằng tay.

Đồ thị phụ thuộc của một chứng minh đã kiểm: mỗi nút là một bổ đề, mỗi cạnh là một lần dùng kết quả trước; hạt nhân đi qua mọi cạnh.

Đại họcPhép tính các cấu trúc quy nạp

Định nghĩa: Hạng thức, kiểu, và phán đoán kiểu

Lô-gíc gốc của Lean là Phép tính các cấu trúc quy nạp (CIC): một lý thuyết kiểu phụ thuộc, nơi kiểu có thể phụ thuộc vào giá trị (kiểu hàm phụ thuộc $\Pi\,(x:A)\,B(x)$ , đọc là "với mọi $x:A$ , có một giá trị kiểu $B(x)$ "), và kiểu mới được xây bằng khai báo quy nạp (số tự nhiên, danh sách, kiểu bằng nhau mệnh đề). Mọi đối tượng được phân loại bởi phán đoán kiểu $\Gamma \vdash t : P$ : "trong ngữ cảnh $\Gamma$ , hạng thức $t$ có kiểu $P$ ".

\Gamma \vdash t : P

Theo tương ứng Curry–Howard, một mệnh đề $P$ chính là một kiểu, và một chứng minh của $P$ là một hạng thức $t$ thuộc kiểu đó — chứng minh chính là lập trình. Đây là lý do tại sao thuật toán kiểm tra kiểu, thứ vốn đã phải tồn tại để dịch chương trình, cũng đủ để kiểm chứng minh.

\vdash t : P \;\Longrightarrow\; P

Hai tầng của phần mềm chứng minh
Tầng	Việc	Độ tin cẩn
Bộ dịch chi tiết / tactic	Tìm hạng thức chứng minh $t$ từ script tactic mức cao	Không cần tin: lỗi ở đây chỉ tốn thời gian
Hạt nhân	Kiểm lại rằng $t$ thật sự có kiểu $P$	Tin cẩn: đây là tiêu chí de Bruijn

Nâng caoTiêu chí de Bruijn và phép bằng qua Eq.rec

Tiêu chí de Bruijn nói một phần mềm chứng minh đáng tin khi có một hạt nhân nhỏ, kiểm tra độc lập, xác nhận mọi hạng thức chứng minh, nên $|\text{kernel}| \ll |\text{tactic engine}|$ : tính đúng đắn dựa trên vài trăm dòng mã, không dựa vào bộ máy tactic đã sinh ra hạng thức đó. Phép bằng quy nạp $a = b$ được định nghĩa bởi một hàm dựng duy nhất $\mathrm{refl} : \forall\, a,\ a = a$ , và phép khử $\mathsf{Eq.rec}$ (quy tắc J) là nguyên thủy duy nhất hạt nhân cần để suy ra mọi tính chất khác của phép bằng.

\mathsf{Eq.rec} : \{C : \forall\, y,\ a=y \to \mathrm{Sort}\} \to C\,a\,(\mathrm{refl}\,a) \to \forall\, y\,(h:a=y),\, C\,y\,h

Định lý: Tính đối xứng của phép bằng từ Eq.rec

Tồn tại hạng thức $\mathrm{Eq.symm} : a = b \to b = a$ chỉ dựng từ $\mathrm{refl}_a : a = a$ và $\mathsf{Eq.rec}$ ; tính đối xứng là một định lý của CIC, không phải một tiên đề thêm.

Vì sao đúng?

Nếu phép bằng cần tiên đề riêng cho đối xứng, kết hợp, tương thích..., hạt nhân tin cẩn sẽ phình ra theo mỗi tính chất mới của $=$ . Suy ra tất cả từ một phép khử giữ hạt nhân nhỏ.

Chứng minh

Cố định $a$ . Ta muốn một hàm nhận $h : a = b$ (với $b$ tuỳ ý) và trả về chứng minh $b = a$ . Áp dụng $\mathsf{Eq.rec}$ với motive $C(y, h) := (y = a)$ — một họ mệnh đề chỉ số theo điểm $y$ và chứng minh $h$ nối $a$ với $y$ .

Phép khử yêu cầu một chứng minh cho trường hợp gốc $C(a, \mathrm{refl}\,a)$ , tức $a = a$ ; ta cấp $\mathrm{refl}\,a$ . Điều này hợp lệ vì trường hợp gốc luôn được chỉ số bởi $\mathrm{refl}$ tại điểm khởi đầu $a$ .

$\mathsf{Eq.rec}$ sau đó trả, với mọi $y$ và mọi $h : a = y$ , một chứng minh của $C(y,h) = (y = a)$ . Thay $y := b,\ h := h$ : ta nhận đúng chứng minh của $b = a$ .

Gói lại thành $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$ cho ra hạng thức kiểu $\mathrm{Eq.symm} : a = b \to b = a$ . Hạt nhân chấp nhận nó chỉ bằng cách khớp phép áp dụng này với chữ ký kiểu của $\mathsf{Eq.rec}$ — không cần lập luận về khái niệm "đối xứng" ở mức hạt nhân.

Định lý: Tính kết hợp của phép bằng từ Eq.rec

Tồn tại hạng thức $\mathrm{Eq.trans} : a = b \to b = c \to a = c$ chỉ dựng từ $\mathsf{Eq.rec}$ .

Vì sao đúng?

Nối các phép bằng ( $a=b=c$ nên $a=c$ ) được dùng trong hầu như mọi chứng minh; nếu đây là tiên đề thay vì hạng thức suy ra được, hạt nhân phải tin tiên đề đó thay vì xác nhận nó bằng tính toán.

Chứng minh

Cố định $a,b$ và $h_1 : a = b$ . Cho $h_2 : b = c$ với $c$ tuỳ ý, ta muốn chứng minh $a = c$ . Áp dụng $\mathsf{Eq.rec}$ lên $h_2$ với motive $C(y, h) := (a = y)$ , chỉ số theo điểm $y$ và chứng minh $h$ nối $b$ với $y$ .

Trường hợp gốc cần là $C(b, \mathrm{refl}\,b)$ , tức $a = b$ — chính là $h_1$ . Vậy $h_1$ là chứng minh trường hợp gốc cấp cho $\mathsf{Eq.rec}$ .

$\mathsf{Eq.rec}$ sau đó trả, với mọi $c$ và mọi $h_2 : b = c$ , một chứng minh của $C(c, h_2) = (a = c)$ , đúng như ta cần.

Vậy $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ có kiểu $\mathrm{Eq.trans} : a = b \to b = c \to a = c$ . Chú ý mẫu hình chung với đối xứng: cả hai chứng minh đều "vận chuyển" một sự kiện theo một phép bằng bằng cách chọn motive $C$ phù hợp, rồi để quy tắc rút gọn cố định của hạt nhân cho $\mathsf{Eq.rec}$ trên $\mathrm{refl}$ làm việc thật.

Đại họcỨng dụng thực tiễn: từ trình biên dịch đến số học

Chứng minh hình thức không còn là thứ chỉ nằm trong phòng thí nghiệm. CompCert, một trình biên dịch C được xác minh hình thức trong Coq, có chứng minh do máy kiểm rằng mã assembly nó sinh ra luôn hoạt động như chương trình nguồn — điều không bộ kiểm thử nào đảm bảo được. AWS và Signal dùng mã mật mã đã xác minh hình thức (trong công cụ như thư viện TLS s2n của AWS, HACL và F) để loại bỏ hẳn nhiều lớp lỗi an toàn bộ nhớ và lỗi kênh kề. Và trong toán học thuần túy, Thí nghiệm Tensor Lỏng (2020–2022) của Lean đã hình thức hóa một định lý khó của Peter Scholze trong toán học cô đặc, và nhóm của Terence Tao đã hình thức hóa chứng minh giả thuyết Polynomial Freiman–Ruzsa (PFR) trong Lean chỉ vài tháng sau khi chứng minh của con người xuất hiện năm 2023.

Ví dụ: Kiểm kiểu chứng minh $n+0=n$

Chỉ ra, ở mức hạt nhân, vì sao hạng thức xây bằng quy nạp cho $\forall\, n : \mathbb{N},\ n + 0 = n$ được chấp nhận.

Lời giải

Phép cộng trên $\mathbb{N}$ định nghĩa bằng quy nạp trên đối số thứ hai: $n + 0 := n$ và $n + \mathrm{succ}\,m := \mathrm{succ}\,(n+m)$ . Vậy trường hợp gốc của đích $n + 0 = n$ rút gọn bằng tính toán về $n = n$ , chính là $\mathrm{refl}\,n$ — hạt nhân chấp nhận không cần lập luận lô-gíc gì, chỉ mở định nghĩa.

Với định lý tổng quát $\forall n,\ n + 0 = n$ , trường hợp gốc này tầm thường theo định nghĩa trên, nên phát biểu này không cần quy nạp (khác với $\forall n,\ 0 + n = n$ , cần quy nạp vì đệ quy trên đối số thứ hai).

Vai trò của hạt nhân chỉ là mở $+$ theo định nghĩa đệ quy trên hạng thức $n+0$ , ra $n$ , rồi kiểm hai vế của đích bằng nhau theo định nghĩa — quy "chứng minh này đúng không" về một tính toán kết thúc, đúng là tiêu chí de Bruijn hoạt động.

Ví dụ: Dịch đã xác minh như một phép bằng có kiểu

CompCert phát biểu định lý đúng đắn của nó như một tính chất bảo toàn ngữ nghĩa. Giải thích "chứng minh là một hạng thức thuộc kiểu đó" mang lại gì cho kỹ sư so với việc kiểm thử trình biên dịch thông thường.

Lời giải

Định lý của CompCert có dạng "với mọi chương trình nguồn $S$ dịch ra assembly $A$ , mọi hành vi quan sát được của $A$ là hành vi của $S$ " — một phát biểu định lượng phổ dụng trên mọi chương trình nguồn, không chỉ những chương trình trong bộ kiểm thử.

Bộ kiểm thử chỉ kiểm hữu hạn cặp $(S,A)$ và không thể loại trừ lỗi dịch sai ở chương trình số 4.000.001. Một hạng thức chứng minh Coq $t$ của phát biểu định lượng phổ dụng thì được kiểm kiểu một lần, cho toàn bộ lượng từ, bởi hạt nhân — cùng hạt nhân dùng cho mọi bổ đề khác của CompCert, nên không có niềm tin mới nào được đưa thêm cho mỗi trường hợp kiểm thử.

Vì hạng thức chứng minh là toàn phần và định lý nói về chính mã nguồn Coq thật của trình biên dịch (trích xuất sang OCaml), bất kỳ thay đổi nào phá vỡ đảm bảo đơn giản sẽ không qua được kiểm kiểu, bắt được các hồi quy mà bộ kiểm thử hồi quy hữu hạn hoàn toàn bỏ lỡ — đây chính xác là lý do mã CompCert sinh ra có không lỗi dịch sai nào bị các chiến dịch fuzzing tìm thấy, trong khi các chiến dịch đó tìm thấy hàng trăm lỗi ở GCC và Clang.

Hiện trạng nghiên cứu tính đến năm 2026

Việc hình thức hóa giờ đủ nhanh để theo kịp nghiên cứu gần thời gian thực: hình thức hóa giả thuyết PFR của Terence Tao (2023) chỉ mất vài tuần, không phải vài năm, và cộng đồng Lean đã hình thức hóa các trường hợp đặc biệt của Định lý Lớn Fermat và phần lớn Thí nghiệm Tensor Lỏng trong khoảng hai năm sau các lập luận gốc. Các mặt trận đang hoạt động gồm tìm tactic có AI trợ giúp (AlphaProof, DeepSeek-Prover) đề xuất hạng thức chứng minh cho hạt nhân kiểm, hình thức hóa hợp tác theo "bản thiết kế" cho các kết quả biên giới (dự án Định lý Lớn Fermat, phong cách EGA/SGA gốc của Grothendieck được làm lại như một dự án Lean), và xác minh hình thức lan vào hạ tầng thường ngày (nghiên cứu bộ kiểm mượn của Rust, mạch rollup đã xác minh trong blockchain). Nút thắt còn mở không phải ở hạt nhân — tiêu chí de Bruijn chưa bị phá vỡ — mà ở công sức người và AI cho elaboration: biến một lập luận không hình thức thành hạng thức mà hạt nhân kiểm được.

Phán đoán kiểu $\Gamma \vdash t : P$ khẳng định điều gì?

Tiêu chí de Bruijn được tóm tắt tốt nhất là:

Trong chứng minh $\mathrm{Eq.symm} : a = b \to b = a$ , mệnh đề nào được cấp cho trường hợp gốc $C(a, \mathrm{refl}\,a)$ ?

Hệ thống thực tế nào dựa vào chứng minh máy kiểm rằng assembly sinh ra luôn hoạt động như chương trình nguồn?

Tài liệu tham khảo

Leonardo de Moura, Sebastian Ullrich (2021). The Lean 4 Theorem Prover and Programming Language
Xavier Leroy (2009). Formal verification of a realistic compiler
Terence Tao, et al. (2023). A Proof of the Polynomial Freiman-Ruzsa Conjecture · arXiv:2311.05762