Learning to Discover Interesting Mathematics

Bài báo định nghĩa tính thú vị nội tại của một định lý toán học bằng tỷ lệ giữa độ dài chứng minh và độ dài phát biểu của nó, đồng thời cho thấy mối tương quan mạnh mẽ với tiện ích hạ nguồn. Nhóm tác giả huấn luyện một mô hình 27B để dự đoán độ khó của chứng minh một cách chính xác. Tối ưu hóa theo metric này giúp tạo ra các định lý thú vị hơn, đồng thời giảm độ trùng lặp với Mathlib từ 91.9% xuống còn 30.6%, chứng minh khả năng tạo ra toán học ngoài phân phối (out-of-distribution). Hệ thống có thể tự sinh ứng viên định lý, chọn ra định lý thú vị nhất và xây dựng thư viện toán học tự mở rộng.

Nhóm tác giả huấn luyện mô hình 27B để dự đoán độ khó chứng minh chính xác hơn các mô hình đa dụng biên.

Việc tối ưu hóa metric làm giảm độ trùng lặp với Mathlib từ 91.9% xuống 30.6%.