Palomar: Kho lưu trữ toán học kiểm chứng bằng Lean mở cửa đón nhận hồ sơ

Trong vài tháng gần đây, chúng ta chứng kiến sự bùng nổ của các bằng chứng toán học do AI tạo ra, nhiều trong số đó đã được hình thức hóa trong ngôn ngữ trợ lý chứng minh Lean. Tuy nhiên, việc kiểm tra xem một kho lưu trữ Lean cụ thể có thực sự chứng minh được tuyên bố hay không là một thách thức không nhỏ, đặc biệt với những người không chuyên sâu về Lean.

Vấn đề xác minh và giải pháp Palomar

Để kiểm chứng một chứng minh Lean, người ta phải đối mặt với nhiều khó khăn: từ việc xác nhận các tuyên bố hình thức, kiểm tra mã nguồn không chứa "gian lận" như thêm tiên đề bổ sung, cho đến đối chiếu ngữ nghĩa giữa mô tả hình thức và mô tả thông thường của kết quả.

Palomar ra đời như một giải pháp cho vấn đề này. Đây là cơ quan đăng ký các kho lưu trữ GitHub bên ngoài (chính xác hơn là các "bản snapshot" của các kho đó, đại diện bởi một commit GitHub cụ thể) chứa mã Lean tuân thủ các thực hành tốt nhất hiện tại, nhằm mang lại sự rõ ràng và tin cậy cho các chứng minh hình thức.

Cơ chế hoạt động của Palomar

Theo công bố từ Terry Tao, một trong những nhà toán học nổi tiếng nhất thế giới hiện nay, Palomar được ấp ủ bởi Lean FRO và ICARM. Một hồ sơ dự thi cần bao gồm ba phần chính:

• Tệp thử thách: chứa mô tả ngắn gọn, dễ đọc bằng Lean về kết quả được tuyên bố
• Mô-đun giải pháp: chứa bằng chứng (có thể dài tùy ý) cho các kết quả đó
• Tệp formalization.yaml: mô tả kết quả bằng ngôn ngữ thông thường, kèm theo siêu dữ liệu và khai báo liên quan

Quy trình xét duyệt gồm hai bước kiểm tra:

1. Kiểm tra cơ học: xác nhận mô-đun giải pháp typecheck và chứng minh chính xác những gì tệp thử thách tuyên bố, sử dụng công cụ Comparator của Lean
2. Kiểm tra phi xác định: xác nhận sự khớp nhau giữa mô tả thông thường trong formalization.yaml và nội dung trong tệp thử thách, thực hiện bởi một mô hình ngôn ngữ lớn (LLM)

Điều quan trọng cần nhấn mạnh: Palomar không phải là một tạp chí được bình duyệt. Các bước kiểm tra trên còn xa mới đạt tới tiêu chuẩn của một bài phản biện chuyên sâu của con người về tính mới, sự thú vị và độ chính xác của một hồ sơ.

Cột mốc quan trọng cho toán học hình thức

Terry Tao, người đang phục vụ trong hội đồng cố vấn khoa học của Palomar cùng với nhiều nhà toán học danh tiếng khác như Jeremy Avigad, Akshay Venkatesh hay Ravi Vakil, đã thử nghiệm thành công quy trình này bằng chính bản formalization của mình cho chứng minh giả thuyết Sendov.

Điểm đáng chú ý là Palomar chấp nhận cả chứng minh do con người tạo ra, do AI tạo ra, hoặc kết hợp cả hai. Điều này phản ánh một thực tế mới trong ngành toán học: các tác nhân AI hiện đại rất hữu ích trong việc hỗ trợ các chi tiết kỹ thuật của quá trình nộp hồ sơ, mặc dù việc xem xét của con người vẫn được khuyến khích mạnh mẽ.

Palomar được đặt tên theo đài thiên văn nổi tiếng, có tham vọng trở thành "máy chủ preprint" cho các chứng minh Lean — một vai trò cực kỳ quan trọng trong bối cảnh AI đang tạo ra một lượng lớn các kết quả toán học với chất lượng và độ tin cậy khó kiểm soát. Sáng kiến này có thể xem như một bước tiến lớn trong việc xây dựng lòng tin và sự minh bạch cho toán học hình thức trong kỷ nguyên AI.