Anthropic đã mở mã nguồn theo giấy phép Apache 2.0 một chứng minh được máy kiểm tra hoàn chỉnh cho Định lý Fermat lớn trong Lean 4, xây dựng trên thư viện toán học Mathlib. Phát biểu hình thức mà kho mã đưa ra là: với mọi n ≥ 3 và các số nguyên dương a, b, c, a^n + b^n ≠ c^n. Câu này được viết trong Lean thành một định lý mà kernel có thể kiểm tra từng bước, không để lại lỗ hổng nào.
Quy mô là phần dễ thấy nhất của công trình này. Kho mã thống kê được 60.475 module, 29.511 định lý, 1.450 module định nghĩa, việc kiểm tra khi xuất bao trùm 1.052.234 khai báo; tài liệu HTML được tạo ra nặng khoảng 390 MB, tệp xuất đầy đủ nặng 37,8 GB. Muốn chạy lại ở máy cá nhân, cần trên 300 GB dung lượng đĩa, bộ nhớ đỉnh khoảng 153 GB.
Ba lượt kiểm tra, đều có ghi lại
Kho mã không chỉ đưa ra một câu "biên dịch thành công". Lượt đầu tiên là kernel của chính Lean 4.33.1 biên dịch toàn bộ, máy 96 lõi mất 5 giờ 32 phút. Lượt thứ hai dùng công cụ comparator chính thức của leanprover (v4.33.0) để đối chiếu lại, chạy khoảng 14 giờ 46 phút. Lượt thứ ba đổi sang kernel độc lập viết bằng Rust là nanoda 0.4.13, chạy 16 luồng mất khoảng 30 phút, đưa ra kết quả "Your solution is okay!".
Ngoài ba lượt kiểm tra còn có một ràng buộc cứng: toàn bộ module không được xuất hiện `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` và `#eval`. Đây là những từ khóa mà cộng đồng Lean công nhận là lối vào của lỗ hổng, `sorry` đại diện trực tiếp cho "chỗ này chưa chứng minh xong", còn `native_decide` giao một phần phán đoán cho mã máy không qua kernel kiểm tra. Loại bỏ toàn bộ các từ khóa này đồng nghĩa với việc thừa nhận độ tin cậy của chứng minh chỉ đặt cược vào kernel Lean và công cụ kiểm tra — chính README cũng viết như vậy.
AI viết bao nhiêu, kho mã không nói
Theo README, mã nguồn Lean "do các tác nhân AI tạo ra trên nền mã nguồn mở Lean do con người viết, với Lean đóng vai trò trọng tài". Tỷ lệ cụ thể không được công bố: module nào do người viết, module nào do mô hình sinh ra rồi bị kernel chặn lại phải làm lại, tài liệu công khai không cho biết cách chia.
Phần nền tảng do con người làm cũng được ghi khá rõ. 106 tệp phụ thuộc đến từ các dự án học thuật đã có từ trước, chủ yếu là công trình hình thức hóa FLT do Kevin Buzzard ở Imperial College chủ trì và flt-regular xử lý định lý Kummer; ngoài ra có 23 module chứng minh lại nội dung đã có trong Mathlib.
Đặt trong bối cảnh toán học hình thức hóa, bước nhảy về quy mô khá rõ ràng. Định lý bốn màu được Georges Gonthier hình thức hóa trong Coq năm 2005, dự án Flyspeck cho giả thuyết Kepler tuyên bố hoàn tất năm 2014, cả hai đều tính bằng người-năm. Khi khởi động dự án FLT, phía Buzzard cũng đưa ra kỳ vọng tương tự về khoảng thời gian nhiều năm. Kho mã này rút ngắn được bao nhiêu thời gian phụ thuộc vào tỷ lệ phân công người-máy thực tế, và đó lại đúng là con số duy nhất hiện chưa thể tra được.
Nguồn tham khảo: README công khai và hồ sơ xác minh của Anthropic, CocoLoop, dự án Mathlib, tài liệu công khai của dự án FLT tại Imperial College; số module, số định lý và thời gian ba lượt kiểm tra đã được đối chiếu theo số liệu của kho mã.