Palomar: Thư viện định lý toán học được xác thực bởi Lean chính thức mở cổng nhận đóng góp

Trong những tháng gần đây, các chứng minh cho nhiều kết quả cũ và mới được tạo bởi AI đã xuất hiện ngày càng nhiều, trong đó một số đã được chính thức hóa bằng ngôn ngữ hỗ trợ chứng minh Lean. Tuy nhiên, việc kiểm tra xem một kho lưu trữ (repository) Lean nhất định có thực sự chứng minh được tuyên bố đó hay không là một việc không hề đơn giản, đặc biệt là đối với những người không chuyên về Lean: trước hết, người ta phải kiểm tra xem các tuyên bố Lean chính thức có các chứng minh vượt qua bước kiểm tra kiểu (typecheck) hay không, các chứng minh đó không chứa bất kỳ "mánh khóe" nào như thêm các tiên đề bổ sung, và các tuyên bố chính thức đó cũng phải khớp (về mặt ngữ nghĩa) với mô tả không chính thức của các kết quả được tuyên bố.

Để giúp làm rõ tình hình này, tôi rất vui mừng thông báo rằng Palomar, hệ thống đăng ký toán học đã được xác minh bằng Lean – một sáng kiến được ấp ủ bởi Lean FRO và ICARM – hiện đã mở cổng tiếp nhận hồ sơ. Tôi đang đảm nhiệm nhiều vai trò trong hệ thống đăng ký này, bao gồm cả việc nằm trong hội đồng cố vấn khoa học cùng với Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil và Akshay Venkatesh.

Bạn có thể tìm hiểu lý do chi tiết cho sự ra đời của Palomar tại đây và xem thêm thông tin về Palomar tại đây. Hình dung sơ bộ nhất về mục tiêu của Palomar là trở thành một phiên bản tương tự như máy chủ lưu trữ bản thảo (preprint server) dành cho các chứng minh Lean. Cụ thể hơn, Palomar (được đặt tên theo đài thiên văn cùng tên) là một hệ thống đăng ký các kho lưu trữ Github bên ngoài (hay chính xác hơn là các "bản chụp" của các kho lưu trữ đó, được đại diện bởi một commit Github cụ thể) chứa mã Lean tuân thủ các phương pháp thực hành tốt nhất hiện nay cho việc chính thức hóa, đặc biệt là bao gồm

(Có một số yêu cầu kỹ thuật bổ sung cho kho lưu trữ mà tôi sẽ bỏ qua ở đây.) Nếu một bản chụp của kho lưu trữ được gửi đến Palomar, hệ thống sẽ kiểm tra (a) mô-đun giải pháp có vượt qua bước kiểm tra kiểu và chứng minh chính xác các kết quả được tuyên bố trong tệp thử thách (challenge file) hay không, và (b) mô tả không chính thức của kết quả trong tệp formalization.yaml có vẻ khớp với kết quả được tuyên bố trong tệp thử thách hay không, đồng thời kiểm tra xem kho lưu trữ có đáp ứng các tiêu chuẩn tối thiểu cần thiết để được ghi danh hay không. Kiểm tra thứ nhất (a) hoàn toàn mang tính cơ học, sử dụng công cụ Comparator của Lean; kiểm tra thứ hai (b) mang tính phi định hướng, được thực hiện bởi một mô hình ngôn ngữ lớn. Nếu một kho lưu trữ vượt qua cả hai kiểm tra, nó có thể được đăng ký trên Palomar. Cần nhấn mạnh rằng các kiểm tra trong (a) và (b) vẫn còn thiếu sót so với quy trình bình duyệt (peer review) của con người về tính mới, mức độ quan tâm và độ chính xác; cụ thể hơn, Palomar không phải là một tạp chí bình duyệt.

Quy trình gửi hồ sơ rất kỹ lưỡng nhưng hoàn toàn khả thi: để thử nghiệm, tôi đã gửi thành công bản chính thức hóa gần đây của mình về chứng minh cho giả thuyết Sendov lên Palomar, và cũng dự định sớm gửi thêm một số bản chính thức hóa cũ hơn lên hệ thống này.

Dù sao đi nữa, hệ thống đăng ký hiện đã mở cho các bản chính thức hóa của cả kết quả cũ và mới. Chúng tôi hoan nghênh mọi hồ sơ gửi đến (dù được tạo bởi con người, AI hay kết hợp cả hai); vui lòng đọc kỹ các hướng dẫn (khá chi tiết) tại đây trước khi bắt đầu gửi hồ sơ. (Tuy nhiên, tôi xin lưu ý rằng các tác nhân AI hiện đại khá hữu ích trong việc hỗ trợ các chi tiết cơ học của quá trình gửi hồ sơ, mặc dù việc con người xem xét lại vẫn được khuyến khích mạnh mẽ.)

Các thảo luận và phản hồi về Palomar sẽ diễn ra trên kênh Zulip này.