Nguồn: Lawrence C. Paulson
Tóm tắt
Nhà khoa học máy tính Lawrence C. Paulson viết về câu hỏi thường gặp khi đề xuất hình thức hóa toán học ngày nay: “Tại sao không dùng Lean?” Tác giả, người đã làm việc trong lĩnh vực proof assistant từ những ngày đầu, bày tỏ sự phê phán nhẹ nhàng về “văn hóa bầy đàn” xung quanh Lean, đồng thời nhắc nhở về lịch sử dài của lĩnh vực hình thức hóa toán học.
Bài viết nhấn mạnh rằng hình thức hóa toán học không bắt đầu với Lean — nó đã bắt đầu từ năm 1968 với hệ thống AUTOMATH của NG de Bruijn. Năm 1977, Jutting đã sử dụng AUTOMATH để hình thức hóa “Foundations of Analysis” của Landau, bao gồm cả việc xây dựng số phức từ logic thuần túy và chứng minh tính đầy đủ Dedekind của đường số thực.
Tác giả cũng nhắc đến công trình của Boyer và Moore (1973) và hệ thống LCF, HOL Light, Isabelle — những hệ thống proof assistant khác đã có những đóng góp lịch sử quan trọng. Lean là một ngôn ngữ tuyệt vời với thư viện lớn và cộng đồng nhiệt huyết, nhưng sự tiến bộ trong hình thức hóa toán học đến từ nhiều hướng và nhiều người không đi theo đám đông.
Điểm mấu chốt của bài là: lịch sử khoa học cho thấy những đột phá thường đến từ những người sẵn sàng đi con đường riêng thay vì chạy theo xu hướng nhất thời, cho dù đó là Lean hay bất kỳ công cụ nào khác đang được ưa chuộng.