Aleph Prover đã chính thức hóa lời giải bác bỏ bài toán "planar unit" của Paul Erdős, một kết quả quan trọng ban đầu được OpenAI thực hiện. Điểm đặc biệt là toàn bộ quá trình này được thực hiện bằng Lean 4 và được phát hành dưới dạng mã nguồn mở.
Diễn biến
Dự án Aleph Prover cho biết việc hình thức hóa này nhằm mục đích cho phép các nhà nghiên cứu khác kiểm tra, mở rộng và xác thực độc lập kết quả của OpenAI. Đây là một minh chứng cho thấy sự kết hợp giữa các phương pháp hình thức (formal methods) và trí tuệ nhân tạo trong việc giải quyết các bài toán toán học phức tạp.
Vì sao đáng chú ý
Việc sử dụng Lean 4 để xác thực các khám phá toán học của AI (như disproof của OpenAI) giúp xóa bỏ nghi ngờ về tính chính xác của các kết quả do máy tính tạo ra. Đối với cộng đồng nghiên cứu AI và Toán học tại Việt Nam, đây là nguồn tài liệu quý giá để tìm hiểu về ứng dụng của Formal Methods trong việc đảm bảo độ tin cậy của các hệ thống AI thế hệ mới.