Bài viết của giáo sư Lawrence C. Paulson trên blog cá nhân đã gây chú ý khi chỉ ra rằng cộng đồng formalised mathematics (toán học hình thức) hiện nay đang quá tôn sùng Lean, quên đi những người tiên phong cách đây gần 60 năm. Theo ông, AUTOMATH do nhà toán học Hà Lan N.G. de Bruijn tạo ra từ năm 1968 mới thực sự là người mở đường. AUTOMATH đã có hầu hết các thành phần cần thiết để chứng minh toán học bằng máy tính, dù ký hiệu rất tệ và hoàn toàn thiếu tự động hóa.

AUTOMATH chứng minh được nhiều hơn bạn nghĩ

Năm 1977, Jutting dùng AUTOMATH để formalise toàn bộ cuốn 'Foundations of Analysis' của Landau, bao gồm xây dựng số phức từ logic thuần túy và chứng minh tính đầy đủ Dedekind của trục số thực. Kỳ tích này phải mất 20 năm sau mới có người lặp lại, khi John Harrison (HOL Light) và Jacques Fleuriot (Isabelle/HOL) formalise lại số thực. Paulson cho rằng hầu hết mọi thứ formalised hôm nay đều có thể làm được trên AUTOMATH, nhưng nó thua kém vì notation (ký hiệu) cực kỳ khó đọc và chứng minh dài dòng, không thể đọc được. Bài viết cũng nhắc đến Boyer và Moore với hệ thống ACL2 dùng cho hardware verification (xác minh phần cứng), chứng minh được Định lý bất toàn Gödel, tính tương hỗ bậc hai và định lý Banach–Tarski.

Paulson kết luận rằng sự phát triển của formalised mathematics không đến từ việc chạy theo đám đông, mà từ những tư duy khác biệt như AUTOMATH, LCF, HOL hay Isabelle. Đây là lời nhắc nhở cho cộng đồng công nghệ và AI rằng đừng quên lịch sử khi chạy theo xu hướng mới.