Trần Ngọc Minh

Anthropic vừa công bố Claude đã giúp hình thức hóa toàn bộ chứng minh Định lý cuối cùng của Fermat bằng Lean, một hệ thống có thể kiểm tra từng bước logic của chứng minh toán học. Điều quan trọng là: Claude không phải là AI đầu tiên giải được Định lý Fermat. Bài toán này đã được Andrew Wiles chứng minh từ thập niên 1990. Thành tựu mới ở đây là Claude đã chuyển một chứng minh toán học cực kỳ phức tạp thành dạng mà máy tính có thể kiểm tra chặt chẽ. Có thể hiểu đơn…