Trên blog cá nhân của giáo sư toán học Terence Tao, nhà toán học Thomas Hales đã có bài viết phân tích sâu sắc về tầm quan trọng của hệ thống kiểm chứng định lý Lean Theorem Prover đối với tính tin cậy của toán học hiện đại, đồng thời mở ra góc nhìn về sự kết hợp giữa Lean và công nghệ AI.
Được phát triển bởi Leo de Moura tại Microsoft từ năm 2013 dưới dạng mã nguồn mở, Lean đã trở thành hệ thống hỗ trợ chứng minh phổ biến nhất trong giới toán học. Thư viện toán học hình thức mathlib của Lean hiện sở hữu gần 300.000 định lý, hơn 100.000 định nghĩa và 2,5 triệu dòng code với sự đóng góp từ hơn 700 nhà nghiên cứu. Nếu như trước đây, việc hình thức hóa bản chứng minh giả thuyết Kepler mất tới 20 năm công sức của con người với 500.000 dòng script, thì gần đây các bài toán lớn như định lý Fermat cuối cùng hay Navier-Stokes đã liên tiếp được hình thức hóa thành công.
Điểm nhấn đáng chú ý là sự trỗi dậy của khái niệm autoformalization – năng lực AI tự đọc các bài báo toán học (file PDF hoặc LaTeX) và tự động xuất ra bản chứng minh dạng mã Lean. Việc tích hợp các mô hình AI tiên tiến giúp tự động hóa khâu chuyển đổi vốn tốn hàng nghìn giờ lao động thủ công của các nhà toán học.
Sự kết hợp giữa AI và các công cụ như Lean mang lại gợi ý quan trọng cho cộng đồng AI và toán học tại Việt Nam. Việc làm chủ các công cụ hỗ trợ kiểm chứng tự động sẽ giúp các nhà nghiên cứu Việt Nam tiệm cận với dòng chảy công nghệ thế giới, đồng thời nâng cao độ chính xác tuyệt đối cho các phần mềm đòi hỏi độ an toàn cao.
Nguồn: Hacker News — Biên dịch & tổng hợp: danhbaai.com