Hãng truyền thông công nghệ Gigazine hôm qua (3 tháng 8) đăng bài viết, cho biết một chứng minh hình thức trong Lean, được thực hiện với sự hỗ trợ của AI và tuyên bố bác bỏ giả thuyết Collatz, đã được xác nhận là không hợp lệ.
Ghi chú: Giả thuyết Collatz (còn gọi là giả thuyết quy về chẵn lẻ / giả thuyết 3n+1) do nhà toán học người Đức Lothar Collatz đề xuất vào năm 1937. Đây là một bài toán toán học có cách phát biểu cực kỳ đơn giản nhưng vẫn chưa được giải quyết, khẳng định rằng mọi số nguyên dương sau nhiều lần lặp theo một quy tắc nhất định cuối cùng đều sẽ trở về 1.
Quy tắc tính toán với một số nguyên dương bất kỳ n:
Nếu n là số chẵn, chia n cho 2 (n ÷ 2).
Nếu n là số lẻ, nhân n với 3 rồi cộng 1 (3n + 1).
Sau khi nhận được số mới, lặp lại các bước trên cho đến khi kết quả trở thành 1.
Lấy số 6 làm ví dụ:
6 là số chẵn, chia cho 2 được 3
3 là số lẻ, nhân với 3 rồi cộng 1 được 10
10 là số chẵn, chia cho 2 được 5
5 là số lẻ, nhân với 3 rồi cộng 1 được 16
16 lần lượt chia cho 2 để được 8, 4, 2, 1
Quỹ đạo cuối cùng là: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
Chuyên gia kiểm chứng hình thức Ramana Kumar đăng dự án lên GitHub vào ngày 25 tháng 7, ban đầu tuyên bố đã bác bỏ giả thuyết Collatz với sự hỗ trợ của AI. Dự án không đưa ra một số nguyên phản ví dụ cụ thể mà chỉ chứng minh trong Lean (hệ thống hỗ trợ chứng minh định lý) rằng “tồn tại một số không thể đi tới 1”.
Lean là một hệ thống hỗ trợ chứng minh định lý, cho phép người dùng viết công thức toán học và logic thành chương trình, sau đó để máy tính kiểm tra tính chính xác của chứng minh. Mã Lean do người dùng viết sẽ biểu diễn mệnh đề toán học và chứng minh dưới dạng chương trình có thể kiểm tra, trong đó kernel xác minh tính nhất quán của kiểu và logic.
Tuy nhiên, khi xem xét nội dung phản biện sau đó, ông phát hiện phương pháp liên quan thậm chí có thể khiến Lean vô điều kiện chấp nhận “False” (đại diện cho một mệnh đề sai). Vì vậy, mã liên quan hiện không thể bác bỏ giả thuyết Collatz.
Nhà nghiên cứu kiểm chứng hình thức Kiran Gopinathan đã rút gọn vấn đề thành một đoạn mã tái hiện nhỏ và báo cáo cho đội ngũ phát triển Lean vào ngày 28 tháng 7 năm 2026.
Lỗ hổng nằm ở phần kernel xử lý “kiểu quy nạp lồng nhau”, khiến hệ thống đôi khi bỏ qua “tham số kiểu ma” (tức tham số không xuất hiện trực tiếp trong các thành phần của cấu trúc dữ liệu), cho phép các tham số vốn phải bị xác định là không hợp lệ vượt qua bước kiểm tra. Nhà phát triển Lean Leonardo de Moura cho biết vấn đề nằm ở việc phần triển khai kernel chưa hoàn tất các bước kiểm tra cần thiết.
Khoảng 1 giờ sau khi nhận được báo cáo, đội ngũ Lean đã tạo yêu cầu kéo để sửa lỗi và phát hành Lean 4.32.2 vào ngày 28 tháng 7, khắc phục vấn đề này.