Kiểm chứng chứng minh định lý do AI tạo ra: Lean 4 và quy trình tái dựng

Khi AI nói đã hoàn tất một chứng minh toán học, bước kiểm tra đáng tin cậy nhất là đưa tệp Lean 4 vào đúng dự án rồi tái dựng. Một đoạn giải thích bằng ngôn ngữ tự nhiên chỉ cho thấy mô hình đã tạo ra lập luận nghe hợp lý; nó chưa chứng minh rằng mệnh đề, giả định và kết luận khớp với bài toán ban đầu.

Bài viết tập trung vào cách kiểm tra một sản phẩm do AI tạo ra. Người đọc cần phân biệt câu trả lời bằng chữ, mệnh đề hình thức và proof term mà Lean kernel chấp nhận. Nếu dùng kết quả cho nghiên cứu, phần mềm hoặc thiết kế kỹ thuật, hãy lưu cả phiên bản Lean, Mathlib, imports, nhật ký build và danh sách tiên đề.

Ba mức độ của một chứng minh đã qua kiểm tra

Câu trả lời tự nhiên là lớp đầu tiên. AI viết ra các bước suy luận, nhưng người đọc phải tự đối chiếu định nghĩa, phép tính và các bước chuyển. Google DeepMind lưu ý rằng những bước trung gian nghe hợp lý vẫn có thể sai; đây là lý do các hệ thống như AlphaProof chuyển sang quy trình hình thức.

Lớp thứ hai là statement, tức mệnh đề đã được viết bằng cú pháp Lean. Kiểu của biến, phạm vi, điều kiện và kết luận phải hiện rõ trong tệp. Tài liệu nhập môn về chứng minh định lý trong Lean 4 mô tả mục tiêu của kiểm chứng hình thức là đưa từng bước suy luận về định nghĩa, định lý, quy tắc hoặc tiên đề đã được khai báo.

Lớp thứ ba là proof term được kernel chấp nhận. Kết quả này cho biết proof term phù hợp với các định nghĩa, định lý, imports và tiên đề trong môi trường hiện tại. Tài liệu chính thức về kiểm chứng một chứng minh Lean cũng nhấn mạnh rằng người dùng vẫn phải xác nhận statement có đúng với ý định ban đầu hay không.

AI chuyển đề bài thành proof term như thế nào

Quy trình thường gồm bốn phần. Trước hết, đề bài tự nhiên được chuyển thành statement; tiếp theo, AI hoặc người dùng tìm các bước chứng minh; Lean tạo proof term từ các tactic; cuối cùng kernel kiểm tra proof term theo logic của Lean.

AlphaProof là ví dụ được công bố rõ. Mô tả của Google DeepMind về AlphaProof và AlphaGeometry 2 cho biết hệ thống chuyển đề bài sang Lean, tìm chứng minh trong môi trường hình thức rồi giao kết quả cho Lean xác nhận. Bài viết này ghi nhận hai hệ thống đã giải bốn trong sáu bài của Olympic Toán quốc tế năm 2024, đạt 28 điểm.

1. Viết statement không làm mất điều kiện

Đề toán thường để một số điều kiện trong ngữ cảnh. Lean yêu cầu kiểu dữ liệu, biến, giả định và kết luận được viết rõ. Sai lầm nguy hiểm nhất xảy ra trước khi kernel bắt đầu: bỏ sót một giả định, đổi phạm vi của biến hoặc thay “với mọi” bằng “tồn tại một” khiến bài toán dễ hơn nhưng không còn là bài toán cũ.

2. Tactic tạo ra sản phẩm mà kernel đọc được

Tactic giúp mở rộng các chi tiết trong proof, nhưng không phải một lối tắt ra ngoài kernel. Tài liệu tham chiếu ngôn ngữ Lean trình bày cách ngôn ngữ, tactic và hệ thống kiểu phối hợp. Khi tactic chạy xong, sản phẩm vẫn phải được kiểm tra theo quy tắc của Lean.

3. Kernel kiểm tra chuỗi logic

Kernel đối chiếu proof term với statement, định nghĩa, imports và tiên đề đã dùng. Nó bắt được proof còn thiếu bước hoặc tactic tạo ra sản phẩm sai kiểu. Kernel không đọc lại đề bài tự nhiên để xác nhận người viết đã formalize đúng ý.

4. Lake tái dựng toàn bộ dự án

Một tệp chứng minh chạy được trên máy cá nhân chưa đủ làm bằng chứng tái lập. Sổ tay cài đặt Lean hướng dẫn tạo dự án bằng Lake, khai báo toolchain và chạy lake build. Đối với dự án dùng thư viện toán, trang này cũng chỉ cách tạo dự án phụ thuộc Mathlib.

Qua được kernel vẫn cần kiểm tra ba điểm

Mệnh đề có đúng với đề bài không

Đây là lớp kiểm tra của con người. Hãy viết lại đề bài bằng ngôn ngữ tự nhiên, đối chiếu từng giả định với statement và thử tìm trường hợp biên. Dấu kiểm tra trong trình soạn thảo chỉ nói rằng Lean chấp nhận mệnh đề đã nhập, không nói rằng mệnh đề ấy là bản dịch trung thành.

Proof có để lại sorryAx không

sorry thường được dùng để tạm lấp phần chứng minh còn thiếu. Lean phát cảnh báo và ghi lại phụ thuộc sorryAx. Khi nghiệm thu, chạy #print axioms theoremName sau định lý. Tài liệu chính thức về các tiên đề giải thích cách đọc các phụ thuộc; nếu thấy sorryAx, proof chưa hoàn tất.

Phiên bản và thư viện có được cố định không

Mathlib là thư viện toán học do cộng đồng Lean duy trì, gồm nội dung toán học và công cụ hỗ trợ lập trình. Dự án cần lưu lean-toolchain, tệp khai báo phụ thuộc, commit thư viện và kết quả build. Cùng một proof có thể cần chỉnh sửa khi Lean, Mathlib hoặc một gói phụ thuộc đổi phiên bản.

Tại Đài Loan, lối vào hiện nằm ở giáo dục và nghiên cứu

Những nguồn công khai được kiểm tra cho thấy Lean tại Đài Loan đã xuất hiện trong hoạt động giảng dạy và nghiên cứu. Trang hoạt động của Trung tâm Khoa học và Công nghệ lý thuyết Quốc gia Đài Loan ghi nhận một hội thảo học Lean tại Đại học Quốc gia Đài Loan, với nội dung về chứng minh định lý tương tác, nghiên cứu toán học và kiểm chứng hình thức.

Tóm tắt seminar của Viện Khoa học Thông tin, Academia Sinica giới thiệu nghiên cứu Lean-QEC về hình thức hóa mã sửa lỗi lượng tử. Đây là một ví dụ nghiên cứu dùng Lean 4 để tạo chứng minh mà máy có thể kiểm tra, nhưng một dự án nghiên cứu riêng lẻ không đủ làm căn cứ suy ra tỷ lệ doanh nghiệp Đài Loan đã áp dụng.

Người học tại Đài Loan có thể bắt đầu bằng Lean 4, tiện ích Lean cho VS Code và Mathlib, sau đó tái dựng một mệnh đề nhỏ. Nhóm làm bán dẫn, firmware hoặc phần mềm yêu cầu độ tin cậy cao có thể xem proof như một sản phẩm cần tái lập: hồ sơ phải gắn mệnh đề, phiên bản, thư viện, lệnh build và người duyệt với nhau.

Tại Việt Nam thì sao

Ở Việt Nam, Lean nên được xem trước hết là một công cụ phát triển và kiểm chứng cần gắn với dự án cụ thể, không phải một nhãn bảo đảm cho mọi câu trả lời của AI. Người học, nhóm nghiên cứu và doanh nghiệp cần phân biệt ba lớp: dịch vụ AI đang bán tại Việt Nam, khả năng cài đặt Lean trên máy của mình và mức sẵn có của người có kinh nghiệm formalize. Ba lớp này không tự động trùng nhau.

Về giá, các trang chính thức của Lean và Mathlib được dùng trong bài không công bố một bảng giá giấy phép cho Lean hay Mathlib. Lean được phát hành theo giấy phép Apache 2.0 theo tài liệu nhập môn, còn Mathlib là dự án mã nguồn mở trên GitHub. Chi phí thực tế của một nhóm ở Việt Nam vì vậy thường nằm ở máy tính, thời gian học, đào tạo, tư vấn, hạ tầng CI và công sức chuyển đổi đề bài thành statement. Không nên ghi một mức giá cố định nếu chưa có báo giá áp dụng cho đúng tổ chức và phạm vi công việc.

Với nhóm muốn bắt đầu, trang cài đặt Lean hướng dẫn dùng elan để quản lý toolchain, VS Code và Lake để tạo dự án. Quy trình này phù hợp cho sinh viên, nhóm nghiên cứu hoặc kỹ sư muốn thử một mệnh đề nhỏ bằng tiếng Anh và ký hiệu toán học. Sau khi tạo dự án, nhóm cần ghi lại phiên bản Lean, phiên bản Mathlib, nội dung lakefile và lệnh lake build; nếu chỉ gửi ảnh chụp dấu kiểm tra, người khác khó tái dựng kết quả.

Về quy định tại Việt Nam, một proof Lean không thay thế các yêu cầu dành cho phần mềm, dữ liệu hoặc sản phẩm thuộc ngành có điều kiện. Nếu AI được dùng trong tuyển dụng, tín dụng, giáo dục, y tế hoặc hệ thống vận hành quan trọng, hồ sơ cần tách rõ mệnh đề toán học khỏi yêu cầu pháp lý và yêu cầu nghiệp vụ. Bộ phận phụ trách nên kiểm tra Cổng thông tin điện tử Chính phủ, cơ quan quản lý chuyên ngành và hợp đồng nhà cung cấp vào thời điểm triển khai; bài viết này không có cơ sở để khẳng định một bộ hồ sơ Lean duy nhất đang bắt buộc cho mọi doanh nghiệp Việt Nam.

Ví dụ thực tế ở Việt Nam có thể bắt đầu từ một hàm nhỏ trong phần mềm, một bất biến của cấu trúc dữ liệu hoặc một phép biến đổi đại số không chứa dữ liệu cá nhân. Nhóm viết yêu cầu bằng tiếng Việt, chuyển thành statement, nhờ AI đề xuất proof, rồi yêu cầu người khác kiểm tra lại ý nghĩa của statement trước khi chạy kernel. Với phần mềm liên quan đến chip, firmware hoặc tính toán tài chính, hồ sơ nên lưu cả ca kiểm thử thất bại, thay đổi toolchain và lý do chấp nhận từng tiên đề.

Mức độ sẵn có của người hỗ trợ Lean tại Việt Nam cần được kiểm tra theo từng nhóm, trường đại học hoặc nhà cung cấp; chúng tôi chưa tìm thấy số liệu chính thức để mô tả quy mô thị trường. Khi hỏi dịch vụ, nên yêu cầu bên cung cấp nêu rõ họ hỗ trợ Lean phiên bản nào, dùng Mathlib ở commit nào, có bàn giao mã nguồn .lean hay không, proof có chạy được bằng lake build trên môi trường sạch hay không và ai chịu trách nhiệm khi thư viện thay đổi. Những câu hỏi này giúp phân biệt đào tạo, tư vấn formalization và việc chỉ cung cấp một câu trả lời do AI sinh ra.

Với cá nhân tại Việt Nam, lộ trình ít rủi ro là học Lean từ tài liệu chính thức, dựng dự án nhỏ, đọc statement trước khi đọc proof, chạy build rồi kiểm tra #print axioms. Với doanh nghiệp, hồ sơ nghiệm thu nên có đối chiếu đề bài với statement, toolchain và phụ thuộc, log build sạch, danh sách tiên đề, người phê duyệt và cách xử lý khi proof không còn dựng lại được. Cách làm này tạo ra bằng chứng kỹ thuật cụ thể mà không cần phỏng đoán về giá hay mức phổ biến của thị trường.

Trình tự kiểm tra cho cá nhân và doanh nghiệp

Khi cá nhân nhận một proof do AI tạo

Trước hết, yêu cầu tệp .lean, phiên bản Lean và Mathlib, tệp cấu hình dự án cùng lệnh tái dựng. Đọc theorem statement trước khi đọc tactic, chạy lake build trong dự án sạch, sau đó dùng #print axioms theoremName. Nếu thiếu tệp, thiếu phiên bản hoặc còn sorryAx, kết quả chưa đủ điều kiện để gọi là một proof hoàn chỉnh.

Khi doanh nghiệp đưa AI vào quy trình kiểm chứng

Bảng nghiệm thu tối thiểu nên có bốn nhóm: đối chiếu yêu cầu với statement, toolchain và phụ thuộc, kết quả lake build, cùng danh sách từ #print axioms. Với chip, firmware hoặc phần mềm an toàn, cần lưu thêm người duyệt, trường hợp biên và kế hoạch quay về phiên bản trước. Kernel kiểm tra chuỗi logic; nhóm kỹ thuật vẫn chịu trách nhiệm xác nhận yêu cầu đã được viết đúng.

Giá trị của AI trong chứng minh định lý nằm ở khả năng đề xuất và tìm kiếm, còn giá trị của Lean nằm ở việc kiểm tra proof term trong một môi trường xác định. Sản phẩm nên là một dự án có thể tái dựng, không chỉ là đoạn văn nghe thuyết phục. Statement, giả định, phiên bản, tiên đề và bối cảnh sử dụng vẫn cần con người chịu trách nhiệm.

Câu hỏi thường gặp

Thấy dấu kiểm tra của Lean là đã tin được proof do AI tạo chưa?
Dấu kiểm tra cho biết kernel chấp nhận proof của statement hiện tại. Người dùng vẫn phải đối chiếu statement với đề bài, kiểm tra giả định, imports, phiên bản và sorryAx; tài liệu kiểm chứng chính thức của Lean nêu rõ ranh giới này.

Người mới nên bắt đầu kiểm tra như thế nào?
Cài Lean 4 theo sổ tay cài đặt, tạo một dự án Lake, đọc statement, chạy lake build và dùng #print axioms theoremName. Hãy bắt đầu bằng mệnh đề nhỏ để hiểu từng lớp kiểm tra.

Tại Việt Nam có bảng giá hoặc chuẩn áp dụng Lean chung không?
Các nguồn Lean và Mathlib được kiểm tra trong bài không đưa ra một bảng giá dịch vụ hay số liệu chính thức về mức độ phổ biến tại Việt Nam. Khi thuê đào tạo hoặc tư vấn, cần hỏi rõ phiên bản, phụ thuộc, mã nguồn bàn giao, lệnh tái dựng và phạm vi hỗ trợ thay vì suy ra chất lượng từ một bản demo.