Giới thiệu về Lean dành cho lập trình viên

Lập trình Giới thiệu về Lean dành cho lập trình viên Cú pháp và ngữ nghĩa của toán học Ronen Lahat Ngày 19/5/2026 15 phút đọc Chia sẻ Bàn cờ vô hạn. Hình ảnh được tạo bởi Grok (xAI) Giới thiệu về các công cụ hỗ trợ chứng minh Tôi là một kỹ sư phần mềm đã chuyển sang lĩnh vực khoa học dữ liệu và tôi làm việc hàng ngày với các thuật toán học máy. Tôi bị cuốn hút bởi sự kỳ diệu rõ ràng của chúng và bởi toán học làm nền tảng cho chúng. Mở bất kỳ thư viện học máy nào, bạn sẽ tìm thấy các thủ thuật toán học liên quan đến phân tích ma trận, tích chập, đường cong Gaussian, v.v. Những điều này, đến lượt mình, được xây dựng trên các tiên đề và quy tắc cơ bản hơn nữa, chẳng hạn như ứng dụng hàm và logic. Trong hành trình tìm hiểu các nguyên tắc cơ bản này, tôi đã sưu tầm cả một kệ sách toán học, nhiều cuốn trong số đó giờ đây đã phủ bụi. Tôi cũng đăng ký học tại Open University, nơi tôi tham gia các lớp học qua Zoom và tìm hiểu về cú pháp và 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 lệ trên bàn cờ, trong khi các định lý là các nước chơi hợp lệ, một số thú vị hơn những nước khác. Chứng minh một định lý có nghĩa là làm sáng tỏ lối chơi đủ để 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 một điều không thể. Ví dụ: “Hai quân tượng nằm trên các ô vuông màu trắng, và một quân tượng không bao giờ có thể chuyển sang một ô vuông có màu khác.” Nhưng trên thực tế, các khóa học rất tẻ nhạt. Tôi được giao các tệp PDF để giải bằng tay và sau đó gửi bản quét bài làm của mình trực tuyến. Trong khi viết nguệch ngoạc bằng bú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 định: Xây dựng một chứng minh 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 đầu thế kỷ này. Tôi cần một IDE, với các gợi ý kiểu, tô sáng cú pháp và thông báo lỗi mô tả, và tương tác với nó. Những suy nghĩ của tôi không phải là mới. Ý tưởng đầu tiên được gọi là tương ứng Curry-Howard, được giải thích dưới đây. Ý tưởng sau là mục tiêu của các công cụ hỗ trợ 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). Các công cụ hỗ trợ chứng minh tương tác so với các công cụ chứng minh định lý tự động Các trình kiểm tra định lý như nhân của Lean có thể xác định xem các biểu thức có được định dạng tốt hay không, liệu các bước có hợp lệ hay không và liệu kết luận cuối cùng có hợp lệ hay không. Các công cụ hỗ trợ chứng minh tương tác được xây dựng dựa trên chúng và cũng sẽ giúp bạn xây dựng các chứng minh của mình và đề xuất các bước. Các công cụ chứng minh định lý tự động (ATP) cố gắng tự tìm ra chứng minh bằng cách sử dụng các kỹ thuật AI. Lean hoạt động như một trình kiểm tra và hỗ trợ 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 được hỗ trợ bởi AI trên kênh YouTube của mình bằ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ở x năm tuổi” có khả năng đã được chính thức hóa bằng Lean (ví dụ 1, ví dụ 2 và 3). Các dự án và điểm chuẩn AI như LeanDojo, miniF2F, ProofNet, PutnamBench, FormalMATH, 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 huy chương bạc tại Olympic Toán học Quốc tế. Các thành phần suy luận cốt lõi của AlphaProof của DeepMind. a: Một tác nhân chứng minh quan sát trạng thái chiến thuật Lean ban đầu, b: Mạng lưới chứng minh (một mô hình transformer 3 tỷ tham số lấy cảm hứng từ AlphaZero) tạo ra danh sách các chiến thuật tiềm năng, c: Tìm kiếm cây sử dụng đầu ra của mạng lưới chứng minh để hướng dẫn việc khám phá các đường dẫn chứng minh tiềm năng. Đây là một hệ thống thần kinh-biểu tượng với nhiều kiến trúc được kế thừa từ AlphaZero chơi cờ vây. Trích từ bài báo của Nature, theo Giấy phép Creative Commons. Hiện có một kho tài liệu hướng dẫn và hướng dẫn phong phú cho Lean, cũng như một cộng đồng tốt, nhưng đối tượng mục tiêu dường như không phải là các nhà phát triển có kinh nghiệm trong các ngôn ngữ lập trình khác. Tôi đã gặp khó khăn trong việc phân tích cú pháp của Lean trong đầu, và khi học, tôi nhận thấy mình đang đi trên một con đường chưa được khai phá. Hy vọng các phần sau đây sẽ hướng dẫn bạn trên con đường này. Sự tương ứng Curry-Howard Hãy bắt đầu với một định lý logic đơn giản, một điều bạn có thể phải chứng minh trong một lớp logic đại học: (P → Q → R) → (P ∧ Q → R) Toán tử → biểu thị phép kéo theo logic, nhưng trong sự tương ứ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 như một hàm. ∧ là phép "và" logic. Nói một cách đơn giản, chúng ta đang hỏi liệu câu lệnh này có đúng không: "Nếu tôi có một hàm mà, khi cho P, tạo ra một hàm từ Q đến R, thì nếu tôi đã có cả P và Q, tôi có thể tạo ra R." Lưu ý: (P → Q → R) là một "hàm curried" (Haskell Curry cũng là người phải chịu trách nhiệm ở đây), và cú pháp này tương đương với (P → (Q → R)). Về mặt lập trình, đó là một hàm trả về một hàm khác, sau đó có thể được gọi là foo(bar)(baz). Nó tương đương về mặt logic với foo nhận cả bar và baz dưới dạng một tuple foo((bar, baz)), nhưng đó là điều chúng ta đang cố gắng chứng minh ở đây. Tương tự, toàn bộ câu có thể được viết là (P → Q → R) → P ∧ Q → R. Hãy hình dung điều này với một ví dụ cụ thể: Nếu tôi có một máy bán hàng tự động mà khi cho một đồng xu (P) trả về một cốc mì ăn liền (Q → R), mà khi cho nước nóng (Q) trả về mì (R), điều đó có nghĩa là tôi có thể tạo ra một hệ thống mà khi cho cả đồng xu và nước nóng (P ∧ Q) làm đầu vào, tôi có thể trả về mì. Máy bán mì cốc. Những máy này đã cung cấp nước nóng cho bạn. Wikimedia Foundation. Nếu bạn được yêu cầu chứng minh rằng điều này là có thể với tư cách là một lập trình viên, bạn có thể bị cám dỗ làm như vậy 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: Hãy thử nó trong TypeScript playground, việc sửa đổi bất cứ điều gì sẽ gây ra lỗi kiểu. Được viết một cách tổng quát và đơn giản hóa (playground): Chúng ta đã định nghĩa một hàm — định lý của chúng ta — nhận một hàm curried (P → Q → R) làm tham số và xuất ra một hàm nhận một kiểu tích P ∧ Q và xuất ra R, tức là (P ∧ Q → R). Hàm này đóng vai trò là "bằng chứng" rằng định lý logic là đúng. Chứng minh có vẻ hợp lý và thậm chí còn thỏa mãn các kiểu thể hiện định lý gốc.