Lỗi nào là một sai sót nhỏ nhặt

Lỗi nào là một sai sót nhỏ nhặt

Điểm chính

1. Nếu một lỗi trong định nghĩa hay chứng minh tuy dễ sửa nhưng khó nhận ra, thì sai sót đó không hề nhỏ nhặt.
2. Có những lỗi chỉ có thể được phát hiện với sự trợ giúp của proof assistant.

Nội dung tóm lược

• Từ tháng 12 năm ngoái đến ngày 16 tháng 4 năm nay, tôi đã dành khoảng 170 giờ để chứng minh định lý chuỗi String.splitOn_of_valid trong thư viện chuẩn của proof assistant Lean.
• Trong quá trình chứng minh định lý này, tôi đã phát hiện một bug trong định nghĩa của hàm String.splitOn.
• Việc sửa bug này không quá khó. Chỉ cần thay i bằng i - j trong định nghĩa đó là xong.
• Tuy vậy, tôi không cho rằng đây là một sai sót nhỏ nhặt. Theo định nghĩa này, hàm splitOn thường hoạt động đúng, nhưng trong những trường hợp đặc biệt lại cho ra kết quả sai.
• Nếu không sử dụng proof assistant như Lean, tôi chắc chắn đã không thể tìm ra một lỗi tinh vi như thế này.