Lean báo proof hợp lệ chưa đủ: vẫn phải kiểm tra định lý và tiên đề
Lean chấp nhận một proof chưa đồng nghĩa với việc toàn bộ tuyên bố toán học đã được xác minh. Quy trình đầy đủ cần kiểm tra định lý trong editor, bảo đảm module thật sự được build, rà soát các tiên đề phụ thuộc, kiểm tra lại artifact bằng lean4checker, rồi đối chiếu phát biểu hình thức với điều được tuyên bố bằng ngôn ngữ tự nhiên.
Các bước này trả lời những câu hỏi khác nhau: kernel có chấp nhận proof hay không; dự án có thực sự kiểm tra tệp chứa kết quả hay không; proof dựa vào giả định nào; artifact đã biên dịch có vượt qua lần kiểm tra lại hay không; và quan trọng nhất, định lý Lean có diễn đạt đúng bài toán dự kiến hay không. Vì vậy, không một dấu xác nhận hoặc lệnh đơn lẻ nào bao quát toàn bộ quy trình.
Bốn cấp kỹ thuật trước khi xét ý nghĩa toán học
Trước khi chạy lệnh, hãy xác định tên đầy đủ của định lý, module chứa nó, target cần build và phiên bản toolchain của dự án. Một tệp Lean đứng riêng có thể chạy trong môi trường của tác giả nhưng không cung cấp đủ thông tin để người khác tái lập dependency và cấu hình đã dùng.
- Dấu xác nhận trong editor: phát biểu đã được elaboration và kernel chấp nhận proof trong môi trường hiện tại.
- Build dự án: module chứa định lý nằm trong build graph và được biên dịch không lỗi.
- Danh sách tiên đề: các phụ thuộc gián tiếp không chứa sorryAx hoặc tiên đề ngoài dự kiến.
- Kiểm tra artifact: lean4checker --fresh đọc module đã build và hoàn tất mà không báo lỗi.
Hướng dẫn xác minh của Lean trình bày các lớp kiểm tra tăng dần này và nhấn mạnh sự khác biệt giữa “định lý có proof hợp lệ” với “phát biểu định lý có nghĩa gì”. Tài liệu cũng coi proof hoặc chương trình do AI tạo nhưng chưa được rà soát là mã có khả năng đánh lừa, nên trường hợp rủi ro cao cần biện pháp mạnh hơn việc build thông thường.
Kiểm tra module có thật sự được lake build
Dấu tích xanh trong editor có phạm vi cụ thể: phát biểu được hiểu theo cú pháp, type class, định nghĩa, tiên đề và import hiện hành; kernel đã chấp nhận một proof của chính phát biểu đó. Nó phát hiện goal còn mở, lỗi tactic và việc dùng sorry trực tiếp trong định lý hiện tại, nhưng không loại trừ sorry hoặc proof chưa hoàn chỉnh nằm trong dependency.
Tại thư mục gốc của dự án, chạy lake build và kiểm tra xem target mặc định có kéo module chứa định lý vào build graph hay không. Nếu chỉ muốn kiểm tra một module, có thể build module đó một cách tường minh; điều cốt yếu là log phải cho thấy đúng tệp chứa kết quả đã được xử lý. Build thành công nhưng bỏ qua tệp proof không phải là bằng chứng cho proof ấy.
Kết quả mong đợi là tiến trình kết thúc không có lỗi hoặc cảnh báo liên quan đến module cần xác minh. Dự án cũng nên giữ tệp lean-toolchain cùng manifest hoặc lockfile tương ứng, để người kiểm tra dùng đúng phiên bản Lean và dependency thay vì vô tình dựng một môi trường khác.
In tiên đề để phát hiện sorry và giả định bổ sung
Đặt #print axioms TenDinhLy sau khai báo, thay TenDinhLy bằng tên đầy đủ nếu định lý nằm trong namespace, rồi bảo đảm tệp này được chạy hoặc build. Lệnh không chỉ nhìn vào thân proof hiện tại mà truy vết các tiên đề được dùng trực tiếp và gián tiếp qua những định lý phụ thuộc.
Theo tham chiếu về tiên đề của Lean, sorry được hiện thực bằng sorryAx và không dành cho proof hoàn chỉnh; Lean cũng không thể tự kiểm tra một tiên đề mới có đúng và nhất quán với các tiên đề khác hay không. Trong quy trình xác minh toán học thông thường, đầu ra rỗng hoặc chỉ gồm propext, Classical.choice và Quot.sound là trường hợp được chấp nhận; sorryAx cho biết proof hoặc dependency chưa hoàn chỉnh.
Một tên khác trong danh sách không nhất thiết chứng minh có gian lận, nhưng phải được giải thích. Định lý khi đó chỉ đúng tương đối với giả định bổ sung ấy. Các phụ thuộc liên quan đến tính toán native hoặc compiler cũng làm thay đổi phần mềm phải được tin cậy, nên không được gộp chúng một cách máy móc với ba tiên đề toán học chuẩn.
Kiểm tra lại artifact bằng lean4checker
Sau khi build thành công, chạy lean4checker --fresh TenModule với tên module chứa định lý. Công cụ đọc các khai báo và proof trong tệp .olean rồi phát lại chúng qua kernel; tùy chọn --fresh tránh việc coi một số module là đã được kiểm tra sẵn. Kết quả cần thấy là tiến trình hoàn tất không lỗi.
Nếu công cụ không tìm được module hoặc dependency, đó là lỗi môi trường, đường dẫn hay cách gọi lệnh, không phải một lần kiểm tra đạt. Cần dùng đúng toolchain và các artifact vừa được tạo. lean4checker giúp bắt thêm một số lỗi trong việc quản lý trạng thái kernel hoặc cách meta-code đưa khai báo vào môi trường, nhưng nó vẫn tin cấu trúc của tệp .olean.
Với mã có khả năng chủ động độc hại, việc chạy build đã mang rủi ro vì tactic và meta-code có thể thực hiện hành động tùy ý. Khi mức đe dọa cao, cần một phát biểu thử thách được tạo trong môi trường tin cậy, sandbox cho bước build và checker bên ngoài; lean4checker một mình không tạo thành ranh giới cách ly đó.
Đối chiếu định lý với tuyên bố toán học
Bước cuối cùng là đọc type của định lý như một đặc tả. Hãy đối chiếu miền của biến, lượng từ, giả thiết, kết luận, điều kiện biên, khái niệm bằng nhau và các định nghĩa tự tạo. Notation, coercion hoặc instance cũng cần được mở ra khi chúng có thể khiến biểu thức quen thuộc mang nghĩa khác.
Checklist của cộng đồng Lean lưu ý rằng tên gọi nổi tiếng không khiến một phát biểu trở thành định lý tương ứng; nếu phát biểu chưa có trong Mathlib, một chuyên gia Lean phải xác nhận bản hình thức phù hợp với tuyên bố toán học. Một proof hoàn chỉnh của mệnh đề yếu hơn, khác miền hoặc có giả thiết làm kết luận trở nên hiển nhiên vẫn không chứng minh điều được quảng bố.
Cách rà soát rõ nhất là lập từng cặp tương ứng: câu tự nhiên nào được mã hóa bởi đoạn nào trong type; giả thiết nào được thêm hoặc bỏ; định nghĩa nào lấy từ thư viện và định nghĩa nào do tác giả cung cấp. Chỉ nên chấp nhận tuyên bố cuối cùng khi cả hai điều cùng đúng: Lean xác nhận proof của phát biểu hình thức, còn người có chuyên môn xác nhận phát biểu ấy chính là bài toán dự kiến.
Đọc thêm:
Đăng ký bản tin
Nhận tin Web3, AI và tiền mã hóa mới nhất ngay trong hộp thư.