Phát hiện lỗi logic trong sách giáo khoa Đại số trừu tượng của Dummit và Foote nhờ công cụ kiểm chứng hình thức

Một lập trình viên tại Recurse Center đã tình cờ phát hiện một lỗi logic trong bài tập chứng minh đầu tiên của cuốn sách giáo khoa kinh điển "Abstract Algebra" của Dummit và Foote. Điều thú vị là lỗi này chỉ lộ ra khi anh cố gắng hình thức hóa bài tập bằng công cụ chứng minh định lý Rocq (trước đây gọi là Coq), một quá trình mà tư duy trên giấy thông thường khó có thể nhận ra.

Vấn đề nằm ở đâu?

Bài tập yêu cầu chứng minh rằng một hàm số là đơn ánh (injective) khi và chỉ khi nó có nghịch đảo trái (left inverse). Theo định nghĩa trong sách, hàm f: A → B được gọi là đơn ánh nếu không có hai đầu vào phân biệt nào cho cùng một đầu ra. Hàm f có nghịch đảo trái nếu tồn tại hàm g: B → A sao cho với mọi a thuộc A, ta có g(f(a)) = a.

Mệnh đề trên nghe có vẻ hiển nhiên và đúng trong hầu hết các trường hợp. Tuy nhiên, nó sai trong một trường hợp đặc biệt: khi tập hợp A rỗng.

Trường hợp phản ví dụ đơn giản

Hãy xem xét A = {} (tập rỗng) và B = {1}. Khi đó hàm f: A → B là hàm rỗng, không có bất kỳ cặp (a, b) nào.

Hàm f này vẫn được coi là một hàm hợp lệ vì nó thỏa mãn tất cả các tiêu chí của định nghĩa hàm số. Và theo logic toán học, f là đơn ánh vì mệnh đề "không có hai đầu vào phân biệt nào cho cùng một đầu ra" đúng một cách hiển nhiên (vacuously true), bởi vì không tồn tại bất kỳ đầu vào nào.

Tuy nhiên, f không có nghịch đảo trái, bởi vì không tồn tại hàm nào từ B (có một phần tử) đến A (rỗng). Điều này vi phạm chiều "nếu đơn ánh thì có nghịch đảo trái" của mệnh đề.

Giá trị của việc dùng công cụ kiểm chứng hình thức

Tác giả bài viết chia sẻ rằng anh "chắc chắn đã không nghĩ đến trường hợp biên này nếu làm bài tập trên giấy". Khi dùng Rocq, anh liên tục gặp bế tắc khi cố chứng minh mệnh đề như được phát biểu. Mọi cách tiếp cận đều đòi hỏi thêm giả định rằng tập A phải có ít nhất một phần tử (inhabited) hoặc tập B phải rỗng.

Sau một thời gian dài vật lộn, anh bắt đầu nghi ngờ rằng mệnh đề này thực chất không đúng, và cuối cùng đã tìm ra phản ví dụ. Trớ trêu thay, khi viết bài blog, anh phát hiện ra rằng lỗi này đã được ghi trong phần errata (danh sách lỗi) của cuốn sách.

Bài học cho cộng đồng lập trình và toán học

Câu chuyện này là một minh chứng tuyệt vời cho sức mạnh của các công cụ kiểm chứng hình thức như Rocq/Coq, Lean, hoặc Isabelle. Những công cụ này buộc người dùng phải xem xét mọi trường hợp một cách chặt chẽ, bao gồm cả những trường hợp biên dễ bị bỏ qua trong suy luận thông thường. Điều này đặc biệt hữu ích không chỉ trong toán học thuần túy mà còn trong việc phát triển phần mềm an toàn, nơi những lỗi logic tinh vi có thể dẫn đến hậu quả nghiêm trọng.

Đối với các bạn sinh viên công nghệ thông tin tại Việt Nam đang học toán rời rạc hay đại số tuyến tính, câu chuyện này nhắc nhở rằng việc kết hợp học lý thuyết với thực hành trên các công cụ máy tính có thể giúp hiểu sâu hơn và tránh những sai lầm tiềm ẩn. Mặc dù không phải lúc nào cũng cần đến công cụ hình thức, nhưng việc rèn luyện tư duy phản biện và luôn đặt câu hỏi "điều gì xảy ra trong trường hợp đặc biệt?" là kỹ năng quan trọng trong cả toán học lẫn lập trình.