Thất bại bác bỏ giả thuyết Collatz bằng AI làm lộ lỗi hạt nhân Lean 4

Một nỗ lực sử dụng AI để bác bỏ giả thuyết Collatz thông qua hệ thống chứng minh định lý Lean đã thất bại, nhưng lại vô tình phát hiện ra một lỗ hổng nghiêm trọng về tính đúng đắn (soundness) trong hạt nhân của Lean. Đội ngũ phát triển Lean đã nhanh chóng khắc phục sự cố này thông qua việc phát hành phiên bản Lean 4.32.2. Các lỗi về tính đúng đắn trong các hệ thống chứng minh định lý lớn như Lean là cực kỳ hiếm gặp và nghiêm trọng, vì chúng làm suy giảm niềm tin nền tảng vào toán học được máy tính xác thực. Sự kiện này cho thấy cách các chứng minh do AI tạo ra có thể kiểm thử áp lực các hệ thống xác thực hình thức và phát hiện ra các lỗi ẩn trong trình biên dịch hoặc hạt nhân. Lỗ hổng nằm ở cách hạt nhân xử lý các kiểu quy nạp lồng nhau (nested inductive types), khi nó không kiểm tra các "phantom type parameters" (tham số kiểu bóng ma), cho phép hệ thống chấp nhận mệnh đề sai logic "False". Lỗi này được báo cáo bởi nhà nghiên cứu Kiran Gopinathan và được đội ngũ Lean vá chỉ trong vòng khoảng một giờ.