Nhà toán học chia sẻ cảm xúc khi AI giải Giả thuyết Barnette sau 24 năm

Nhà lý thuyết đồ thị Jake Boggan đã chia sẻ những cảm xúc sâu sắc trên Hacker News sau khi một hệ thống AI xuất bản bản chứng minh được xác minh bằng ngôn ngữ Lean cho Giả thuyết Barnette trong kho lưu trữ toán học của OpenAI. Boggan đã dành 24 năm rải rác trong đời để tìm cách giải bài toán mở kéo dài nhiều thập kỷ này. Khi các hệ thống AI đạt bước tiến lớn trong việc tự động chứng minh định lý, chúng bắt đầu giải được những bài toán mở mà giới nghiên cứu mất nhiều thập kỷ theo đuổi. Sự chuyển dịch này vừa đánh dấu một cột mốc kỹ thuật trong kiểm chứng hình thức, vừa mang lại tác động cảm xúc sâu sắc tới các chuyên gia khi mục tiêu cả đời của họ bị tự động hóa. Bản chứng minh được ghi nhận trong kho lưu trữ GitHub `openai/math` của OpenAI ở bài toán số 180, xác minh hình thức lời giải bằng trợ lý chứng minh Lean. Giả thuyết Barnette khẳng định rằng mọi đồ thị phẳng tam liên thông, nhị phân, cấp 3 đều chứa một chu trình Hamiltonian.