Star Fleet Math: Một Hệ Thống AI Thực Sự Đang Giải Các Bài Toán Mở

Star Fleet Math là một hệ thống AI mới giải quyết những bài toán mở khó nhất thế giới bằng Lean 4. Đây là ứng dụng desktop Mac điều phối tới 20 bộ điều khiển tác nhân song song—gọi là "starships"—mỗi bộ chạy một phiên bản GPT-5.6 chuyên dụng trên máy chủ 60 vCPU. Toàn bộ hệ thống được xây dựng từ đầu bằng TypeScript và Bun.

Mỗi starship có quyền truy cập vào một kho vũ khí nghiêm túc: CPU burst lên tới 2.000 vCPU cho tìm kiếm phân mảnh, GPU H100 burst cho tìm kiếm song song quy mô lớn, kho lớn các tiền đề Lean 4 có thể tìm kiếm qua Gemini embeddings và Chroma vector DB, chỉ mục Firecrawl của arXiv và GitHub, bộ điều khiển tác nhân xác minh chứng minh sử dụng Claude Fable, và hệ thống bộ nhớ dài hạn cục bộ gọi là Ton 618 xây dựng đồ thị phụ thuộc của các định lý đã được xác minh. Sandbox được nạp sẵn các bộ giải SAT/SMT (CaDiCaL, kissat, Z3), CP-SAT của Google, các hệ thống đại số máy tính (SageMath, PARI/GP, GAP, Macaulay2), và toàn bộ toolchain Rust, CUDA C++, và Lean 4.

Star Fleet đã đề xuất một lời giải cho Bài toán Erdős #123, một bài toán lý thuyết số với giải thưởng 250 đô la. Bài toán yêu cầu: với các số nguyên đôi một nguyên tố cùng nhau a,b,c≥1, liệu mọi số nguyên lớn có thể biểu diễn thành tổng các số phân biệt có dạng a^k b^l c^m (k,l,m≥0), với điều kiện bổ sung là không có số hạng nào được chọn chia hết cho số hạng khác?

Khó khăn cốt lõi và đột phá

Điều kiện chia hết là thứ làm bài toán này trở nên khó. Các lập luận đầy đủ thông thường sụp đổ vì các số hạng từ các thang đo khác nhau thường có thể so sánh được bằng tính chia hết, trong khi một phản xích chia hết có thể quá thưa để lấp đầy các số nguyên liên tiếp. Công trình trước đó đã phát triển một sơ đồ rút gọn sử dụng hiệu chỉnh và quy nạp, nhưng nó để lại một bài toán hạt giống hữu hạn cứng đầu: trước tiên bạn cần biểu diễn mọi số nguyên trong một khoảng nhân rộng [N, CN], và quy nạp chỉ lan truyền khoảng đó, chứ không xây dựng nó.

Hiểu biết chính là làm việc trên một mức số mũ thuần nhất duy nhất (i+j+k = D). Trên cùng một mức, hai đơn thức phân biệt không bao giờ có thể chia hết cho nhau, vì vậy mọi tập con đều tự động là nguyên thủy. Điều này biến bài toán thành một câu hỏi cộng tính về tổng tập con, khiến tính nguyên thủy trở nên miễn phí miễn là tất cả các mảnh đều ở cùng một bậc. Nhóm nghiên cứu sau đó sử dụng một cấu trúc mã cạnh để thu được c^n tổng tập con nguyên thủy với các số dư phân biệt modulo c^n và carry bị chặn, sau đó áp dụng van der Waerden hữu hạn (từ định lý Hales-Jewett của Mathlib) để thu được các cấp số cộng chính xác dài tùy ý của các tổng tập con thuần nhất nguyên thủy.

Đột phá thực sự đến từ việc khai thác các đơn thức chưa sử dụng trên cùng một mức số mũ thuần nhất—một "lớp vỏ bên trong tùy chọn"—để biến một cấp số cộng thành một khoảng lưới lớn, sau đó lấp đầy các số dư bằng các hiệu chỉnh mặt. Kết quả cuối cùng: với mọi bộ ba đôi một nguyên tố cùng nhau a,b,c>1, mọi số nguyên đủ lớn đều là tổng các số hạng phân biệt a^i b^j c^k sao cho không có số hạng nào được chọn chia hết cho số hạng khác. Định lý được hình thức hóa trong Lean 4 dưới dạng Erdos123.erdos_123 : Erdos123.IntendedStatement.

Star Fleet hiện đang làm việc trên 27 bài toán Erdős, 630 bài toán Frontier Math, và 14 bài toán Thiên niên kỷ. Kiến trúc của hệ thống—kết hợp tính toán song song quy mô lớn, xác minh hình thức trong Lean 4, và đồ thị phụ thuộc ngày càng lớn của các định lý đã được chứng minh—là một cái nhìn thoáng qua về cách toán học hỗ trợ AI có thể hoạt động ở quy mô lớn.