Đoạn Video
Ảnh
Chi Le
Thành viên nổi tiếng
Claude của Anthropic vừa đạt một cột mốc đáng chú ý trong lĩnh vực toán học khi chỉ mất 11 ngày để hoàn thành việc hình thức hóa Định lý cuối cùng của Fermat bằng Lean, tạo ra một hệ thống chứng minh khổng lồ mà máy tính có thể kiểm tra từng bước về mặt logic. Đứng sau dự án là Tianyi Peng (Peng Tianyi), cựu sinh viên lớp Yao danh tiếng của Đại học Thanh Hoa, sau đó lấy bằng tiến sĩ tại MIT và hiện là trợ lý giáo sư tại Columbia Business School, đồng thời tham gia nghiên cứu tại Anthropic. Thành tựu này đang gây chú ý lớn, song cần hiểu đúng rằng Claude không phải là AI đầu tiên tìm ra lời giải cho Định lý cuối cùng của Fermat, bởi bài toán đã được nhà toán học người Anh Andrew Wiles chứng minh từ hơn 30 năm trước. Điểm đặc biệt của dự án lần này là Claude đã giúp chuyển một khối lượng toán học cực kỳ phức tạp thành chứng minh hình thức bằng Lean, cho phép máy tính kiểm tra chặt chẽ từng định nghĩa, giả thiết và bước suy luận...
Đọc bài gốc tại đây
