7 tháng vượt 15 nhà toán học làm việc trong 6 năm, AI viết hơn triệu dòng code thử thách xác minh siêu lớn công trình chứng minh toán học
**AI Phá Vỡ Thách Thức Kiểm Chứng Chứng Minh Toán Học Quy Mô Lớn: 7 Tháng Tạo Hơn 990,000 Dòng Mã**
Phân loại nhóm đơn hữu hạn (CFSG) là một trong những chứng minh toán học đồ sộ nhất, trải dài gần 20,000 trang qua hàng trăm công trình. Việc kiểm tra lại toàn bộ chứng minh này vượt quá khả năng của một cá nhân hay nhóm nghiên cứu.
Để giải quyết thách thức này, nhóm nghiên cứu từ Đại học Thanh Hoa và Đại học Warwick đã phát triển **FormaTheoria**, một quy trình làm việc AI hỗ trợ nghiên cứu toán học. Hệ thống này tự động phân tích tài liệu toán học gốc, xây dựng lý thuyết hình thức và sử dụng trợ lý chứng minh Lean để kiểm tra từng bước.
Chỉ trong **7 tháng** (từ tháng 1 đến tháng 8/2026), FormaTheoria đã đạt được cột mốc quan trọng:
* Hoàn thành việc hình thức hóa chứng minh cho **4 định lý then chốt** (Feit–Thompson, Glauberman Z*, Brauer–Suzuki, Bender–Suzuki) trên con đường tiến tới CFSG.
* Tạo ra một mạng lưới chứng minh với **hơn 990,000 dòng mã Lean** có thể kiểm chứng, liên kết hơn 30,000 khẳng định toán học.
* Tham khảo và tích hợp kiến thức từ **15 sách/bài báo (1037 trang)**.
* **Vượt xa hiệu suất thủ công**: Công việc tương đương với dự án hình thức hóa Feit–Thompson trước đây do khoảng 15 nhà toán học thực hiện trong **6 năm**.
FormaTheoria không chỉ chứng minh mà còn **phát hiện và sửa lỗi** trong tài liệu gốc, như định nghĩa không nhất quán, điều kiện bị thiếu hay lỗi đánh máy, nhờ quy trình kiểm tra nghiêm ngặt và có cơ chế rà soát độc lập. Nó cho thấy AI có khả năng duy trì và mở rộng môi trường toán học quy mô lớn, quản lý các phụ thuộc phức tạp xuyên nhiều tài liệu.
Nghiên cứu này hướng tới một mô hình **hợp tác người-máy mới**: con người đưa ra phán đoán và vấn đề then chốt, AI đảm nhận tìm kiếm và suy luận quy mô lớn, còn hệ thống hình thức đảm bảo mọi bước có thể được kiểm tra lại. Đây có thể là con đường mới để quản lý tri thức toán học siêu lớn trong tương lai.
marsbit27 phút trước