Tại sao không nhất thiết phải dùng Lean? Lịch sử và tương lai của hình thức hóa toán học

Trong giới hình thức hóa toán học hiện nay, dường như có một áp lực vô hình rằng khi đề xuất một dự án mới, bạn bắt buộc phải giải thích lý do tại sao không sử dụng Lean. Điều này gợi nhớ cho tôi về lý do tôi rời bỏ thế giới của các kiểu phụ thuộc (dependent types) cách đây 40 năm: sự sùng bái, tính khép kín và sự tuân thủ mù quáng.

Không thể phủ nhận rằng Lean là một ngôn ngữ tuyệt vời với công cụ hỗ trợ tốt, thư viện khổng lồ và một cộng đồng người dùng hùng hậu, nhiệt thành. Gần đây, cộng đồng này đã đạt được những thành tựu đáng kinh ngạc. Tuy nhiên, chúng ta không được quên rằng lịch sử hình thức hóa toán học đã kéo dài gần 60 năm. Trong cơn hưng phấn của sự tiến bộ ngày nay, chúng ta cần nhớ rằng chúng ta đã đến được đây không phải bằng cách đi theo đám đông.

Lịch sử lâu đời trước Lean

Một phần của sự cường điệu xung quanh Lean là tuyên bố thường xuyên rằng "Lean đã làm cho việc hình thức hóa toán học trở nên khả thi". Xin lỗi, nhưng chúng ta đã đạt được cột mốc đó từ năm 1968. Hệ thống AUTOMATH của NG de Bruijn khi đó đã bao gồm hầu hết các thành phần cần thiết. Đến năm 1977, Jutting đã sử dụng nó để hình thức hóa cuốn Foundations of Analysis (Cơ sở của Phân tích) của Landau, bao gồm việc xây dựng các số phức bắt đầu từ logic thuần túy.

Jutting đã làm việc với các lớp tương đương và các tập hợp số hữu tỷ. Ông đã chứng minh hình thức sự đầy đủ Dedekind của đường số thực. Thành tựu của ông không được ai sánh kịp trong 20 năm, bất chấp sự tiến bộ vượt bậc về sức mạnh tính toán. Cuối cùng, vào giữa những năm 90, các số thực được hình thức hóa một lần nữa bởi John Harrison (sử dụng HOL Light) và Jacques Fleuriot (Isabelle/HOL).

Tôi tin rằng hầu như mọi thứ đã được hình thức hóa ngày nay trong bất kỳ hệ thống nào đều có thể đã được thực hiện trong AUTOMATH. Nhược điểm chính của nó là ký pháp thực sự khủng khiếp và sự thiếu hoàn toàn tự động hóa. Các bằng chứng rất dài và khó đọc. Tuy nhiên, đối với lập luận về các lớp tương đương, nó có lẽ vẫn tốt hơn Rocq (trước đây là Coq).

Các hướng đi khác biệt

Từ một góc độ hoàn toàn khác, công trình của Robert Boyer, J Moore và nhiều đồng nghiệp của họ đã ra đời. Được công bố lần đầu vào năm 1973 với tiêu đề "Proving theorems about LISP functions" (Chứng minh định lý về các hàm LISP), họ đặt ra mục tiêu là kiểm chứng mã code, không phải toán học. "Logic tính toán" của họ có những hạn chế rõ ràng đối với toán học nói chung, nhưng điều đó không ngăn cản việc sử dụng nó để hình thức hóa nhiều kết quả sâu sắc, từ định lý bất hoàn toàn của Gödel đến tính tương hỗ bậc hai và định lý Banach–Tarski. Phiên bản hiện đại được gọi là ACL2 và chủ yếu được áp dụng để kiểm chứng phần cứng. Bạn có thể đi rất xa bằng cách khác biệt.

Hệ thống Edinburgh LCF mang tính đột phá tập trung hẹp vào lý thuyết ngôn ngữ lập trình, nhưng ý tưởng sử dụng ngôn ngữ lập trình hàm làm ngôn ngữ siêu (metalanguage - do đó có tên ML) cho một trợ lý chứng minh đã có tác động rộng lớn. Các nhóm tại Cambridge, INRIA, Cornell và những nơi khác đã xây dựng công cụ sử dụng ML, bao gồm các phiên bản đầu tiên của HOL, Coq (nay là Rocq) và Nuprl.

Sự trỗi dậy của Lean và triết lý "Mệnh đề như là kiểu"

Tôi biết ít về sự phát triển của Lean, nhưng tôi biết một chút về cách nó quét sạch cộng đồng toán học. Các nhà toán học đã nhận xét một cách dè dặt rằng không một trong các bằng chứng được đề cập ở trên liên quan đến các cấu trúc tinh tế xuất hiện trong toán học chính thống như các lược đồ Grothendieck hoặc không gian hoàn hảo (perfectoid spaces).

Tom Hales có ý tưởng xây dựng một thư viện gồm các định nghĩa như vậy — chỉ các định nghĩa, chưa cần nói đến bằng chứng — và ông chọn Lean cho mục đích đó. Kevin Buzzard nghe điều này và quyết định thử Lean cho giảng dạy. Phần còn lại là lịch sử.

Một hành động then chốt của cộng đồng Lean là từ bỏ sự ám ảnh kỳ lạ với "chứng minh kiến tạo" (constructive proofs) đã thống trị Rocq trong suốt thời gian tồn tại của nó. Sự ám giác này đã cản trở việc áp dụng Rocq vào toán học, để lại sân chơi cho Lean.

Tuy nhiên, có một vấn đề lớn trong cách cộng đồng này định nghĩa "trợ lý chứng minh". Nhiều người định nghĩa nó là một phần mềm kiểm tra bằng chứng theo nguyên tắc "mệnh đề như là kiểu" (propositions as types). Và giống như vậy, hầu hết nghiên cứu của nửa thế kỷ qua bị xóa sổ. Không còn gì ngoại trừ Rocq, Lean và Agda. Ngay cả AUTOMATH cũng không phải là một trường hợp của mệnh đề như là kiểu. De Bruijn đã hiểu 50 năm trước rằng các danh mục kiểu và mệnh đề cần được giữ riêng biệt.

Tiếp cận LCF và vấn đề bộ nhớ

Cả Rocq và Lean đều bao gồm kiểu Prop của các mệnh đề. Điều này cung cấp sự không liên quan của bằng chứng (proof irrelevance), nghĩa là tất cả các đối tượng bằng chứng cho một mệnh đề nhất định đều đánh giá cùng một giá trị. Nhưng tại sao chúng ta vẫn giữ các đối tượng bằng chứng khổng lồ này?

Rằng các đối tượng bằng chứng là không cần thiết là phát hiện then chốt của Robin Milner cho LCF. Tất cả những gì bạn cần là một ngôn ngữ lập trình (ML!) cung cấp các kiểu dữ liệu trừu tượng. Đặt hạt nhân bằng chứng của bạn bên trong một kiểu dữ liệu trừu tượng, với các quy tắc suy luận tại các hàm tạo, và xong! Các bằng chứng được kiểm tra động. Không thể gian lận nhờ các rào cản trừu tượng của ML.

Trong thời đại của "RAMmageddon" (thảm họa bộ nhớ), việc lãng phí hàng chục megabyte cho các thuật ngữ khổng lồ không biểu thị gì cả là điều điên rồ.

Tại sao nên cân nhắc Isabelle?

Nếu đồng nghiệp của bạn đang sử dụng Lean và các điều kiện tiên quyết của bạn nằm trong thư viện Lean, tất nhiên bạn nên dùng Lean. Nhưng nếu bạn tự do lựa chọn, một mục đích chính của bài viết này là cung cấp cho bạn lý do để cân nhắc Isabelle.

Một khó khăn chính với các kiểu phụ thuộc là nếu thực hiện đúng, việc kiểm tra kiểu phải không thể quyết định được (undecidable). Đó là vì sự bằng nhau là không thể quyết định được. Để làm cho việc kiểm tra kiểu có thể quyết định được, sự bằng nhau bị hạ cấp xuống sự bằng nhau định nghĩa hoặc nội hàm (intensional equality). Mặc dù hạn chế này có tác động thực tế đến các bằng chứng, việc kiểm tra sự bằng nhau định nghĩa vẫn là một gánh nặng tính toán nặng nề.

Lean làm đúng nhiều thứ và có khả năng dễ đọc, thậm chí hỗ trợ các khối bằng chứng lồng nhau. Bây giờ cộng đồng người dùng của nó phải tận dụng các tính năng này, giống như người dùng Isabelle đang làm. Sự minh bạch tối thượng không phải là một đối tượng bằng chứng mà máy tính có thể kiểm tra, mà là một văn bản bằng chứng mà con người thực sự có thể đọc được.

Tương lai: AI và sự chuyển dịch

Sự trỗi dậy của AI đang làm cho những khác biệt này trở nên rõ rệt hơn. Các bằng chứng của AI có xu hướng lộn xộn, nhưng dễ dàng dọn dẹp chúng bằng công cụ "sledgehammer". Vì chúng được cấu trúc tốt — trong kinh nghiệm hạn chế của tôi, sử dụng Claude — chúng dễ đọc mặc dù thường quá chi tiết. Bạn có thể thấy những gì đang diễn ra và tìm cách đơn giản hóa chúng.

Cũng có nghiên cứu gần đây trong đó các mô hình ngôn ngữ tự gọi sledgehammer. Cuối cùng, AI có thể dễ dàng dịch các bằng chứng có cấu trúc dễ đọc từ một trợ lý chứng minh này sang trợ lý khác. Khi đó, bạn không còn cần lo lắng về việc chọn hệ thống nào nữa.

Và tất nhiên, không thể nào quên Mizar. Không một lịch sử nào về hình thức hóa toán học là hoàn chỉnh mà không có sự thảo luận về Mizar và thư viện toán học rộng khắp của nó. Ngôn ngữ Isar của Isabelle vay mượn nặng nề từ Mizar. Nhưng đó là câu chuyện cho bài viết lần sau.