AI của Axiom Math Xác Minh Định Lý Khoảng Cách Nguyên Tố 246 trong Lean

Axiom Math cho biết hệ thống AxiomProver của họ đã tạo ra một bằng chứng Lean 4 được máy kiểm tra cho kết quả mạnh nhất hiện nay về khoảng cách giữa các số nguyên tố: định lý rằng vô hạn cặp số nguyên tố có hiệu không vượt quá 246. Công ty công bố kết quả vào ngày 17 tháng 8 năm 2026 dưới dạng bản thiết kế hình thức tương tác, ghi công cho 41 người đóng góp có tên trong lĩnh vực toán học, kỹ thuật và nhà nghiên cứu chính, với IEEE Spectrum là nguồn đưa tin đầu tiên.

Giới hạn 246 là rìa hiện tại của kiến thức con người trong cuộc tấn công lâu dài vào giả thuyết số nguyên tố sinh đôi, giả thuyết thế kỷ 19 cho rằng các số nguyên tố cách nhau đúng hai sẽ xuất hiện vô hạn. Trang dự án của Axiom Math mô tả công việc như một sự hình thức thống nhất của bài báo năm 2013 của James Maynard “Small gaps between primes” cùng với phần mở rộng của dự án hợp tác Polymath8b đã thu hẹp giới hạn 600 của Maynard xuống còn 246. Các bằng chứng được máy kiểm tra được tổ chức thành một thư viện Lean công cộng, PrimeGapsLib, với định lý 246 là kết quả tiêu biểu của nó.

“Định lý này hiện đang đại diện cho ngưỡng của kiến thức con người về các số nguyên tố,” Ken Ono, nhà toán học sáng lập của Axiom Math, nói.

Kiểm chứng hình thức có nghĩa là chuyển một bằng chứng sang một ngôn ngữ mà một chương trình nhỏ, đáng tin cậy gọi là kernel có thể kiểm tra từng dòng. Kết quả không phải là một sự đảm bảo tuyệt đối — phát biểu phải được dịch chính xác, và trình kiểm tra phải đáng tin — nhưng nó loại bỏ tính dễ sai của con người trong chuỗi kiểm tra. Cho đến nay, các hệ thống AI tham gia các chuẩn đoán toán học chủ yếu được đánh giá trên các bài thi có bằng chứng ngắn, tự chứa; khoảng cách giữa những kết quả đó và việc hình thức ở mức nghiên cứu đã rất lớn, một mô hình thấy được ở các hệ thống trước đây xuất sắc trong hình học Olympic trong khi để lại lĩnh vực toán học nghiên cứu gần như không chạm tới.

Từ 70 Triệu Đến 246

Giả thuyết này, được Alphonse de Polignac định dạng chính xác vào thế kỷ 19, vẫn chưa được chứng minh. Giới hạn hữu hạn đầu tiên xuất hiện vào năm 2013, khi Yitang Zhang chứng minh rằng vô hạn cặp số nguyên tố nằm trong khoảng 70 triệu nhau. Vài tháng sau, Maynard giới thiệu một phương pháp sàng lọc tinh chỉnh và giảm giới hạn xuống 600 — công trình này góp phần vào Huy chương Fields năm 2022 của ông — và sự hợp tác Polymath8b, bao gồm Maynard và Terence Tao, đã đẩy nó xuống 246. Bản thiết kế của Axiom Math trình bày tiến trình này như dự án mà họ định hình thành hình thức.

Quá trình hình thức tuân theo một quy trình mà công ty mô tả thành ba giai đoạn. Các nhà nghiên cứu đầu tiên viết bằng chứng dưới dạng bản thiết kế — mỗi định nghĩa, bổ đề và định lý được gắn nhãn, một phát biểu chính xác và danh sách các kết quả mà nó phụ thuộc — tạo ra một đồ thị phụ thuộc sắp xếp công việc. AxiomProver, hệ thống đa tác nhân của công ty cho nghiên cứu toán học thông qua bằng chứng hình thức, sau đó tạo ra các bằng chứng Lean 4 có thể kiểm tra bằng máy, dựa trên Mathlib, thư viện toán học cộng đồng, và trên PrimeNumberTheoremAnd, dự án hình thức hiện có do Alex Kontorovich và Tao dẫn đầu. Đội ngũ Axiom sau đó xem xét mã đã tạo và tổ chức nó thành PrimeGapsLib.

Các kết quả chính được thư viện nêu ra hơi vượt qua định lý tiêu đề. Bên cạnh giới hạn 246, nó hình thức hoá giới hạn 600 của Maynard, và bao gồm một thử thách xác minh tự chứa — chỉ dựa trên Mathlib, với vị trí bằng chứng để trống — cho phép bất kỳ ai có công cụ so sánh Lean có thể độc lập xác nhận rằng các bằng chứng của thư viện khớp với các định lý đã nêu. Công ty cảnh báo rằng việc kiểm tra đầy đủ có thể mất hàng giờ; phiên bản rút gọn bao phủ hai kết quả còn lại chỉ mất vài phút.

Vị Trí Của Điều Này Trong Các Khiếu Nại Hình Thức AI

Kết quả này xuất hiện trong một năm các khiếu nại ngày càng tăng về việc các hệ thống AI thực hiện toán học cấp nghiên cứu, hầu hết dựa trên điểm số cuộc thi hoặc bằng chứng ngắn. Axiom Math là một trong những người khiếu nại mạnh mẽ hơn: AxiomProver được ghi công đã giải quyết các vấn đề mở trước đây, bao gồm công trình mà công ty đã công bố trong các tạp chí được bình duyệt, và các hệ thống AI hiện đã giải quyết một số vấn đề lâu đời của Erdős. Sự hình thức hoá 246 là một loại kết quả khác — không phải một định lý mới, mà là một tái cấu trúc được máy kiểm tra của một trong những bằng chứng đòi hỏi kỹ thuật cao nhất trong lý thuyết số hiện đại.

So sánh gần nhất là đầu năm nay, khi Math, Inc. sử dụng tác nhân Gauss của mình để hoàn thành bằng chứng hình thức của các kết quả đóng gói hình cầu đoạt Huy chương Fields của Maryna Viazovska trong các chiều 8 và 24. Sidharth Hariharan, sinh viên tiến sĩ Carnegie Mellon người đã dẫn dắt nỗ lực bản thiết kế con người cho việc hình thức hoá đó và hiện là thực tập sinh tại Axiom Math và là người đóng góp toán học được ghi danh trong dự án 246, cho rằng kết quả mới là thành tựu toàn diện hơn. Lý luận của anh, như anh mô tả, là Axiom được xây dựng để tái sử dụng: thay vì một hình thức hoá một lần cho một bằng chứng duy nhất, PrimeGapsLib là một thư viện được duy trì các kết quả khoảng cách nguyên tố, nhằm hỗ trợ công việc và nghiên cứu hình thức hoá trong tương lai.

Sự khác biệt này quan trọng đối với cách đọc kết quả. Một lần xác minh duy nhất chứng minh rằng một hệ thống có thể chịu đựng một bằng chứng khó. Một thư viện lại chứng minh điều gì đó gần hơn với cơ sở hạ tầng — cơ chế hình thức tái sử dụng mà các kết quả khác có thể dựa trên — đây là hướng mà các hệ thống chứng minh hình thức đang tiến tới khi chúng chuyển từ giải bài tập sang kiểm tra toán học thực tế. Yêu cầu về khả năng ở đây dựa trên các hiện vật công khai và có thể chạy lại thay vì dựa vào điểm số chuẩn đoán: bản thiết kế, mã Lean, và một thử thách so sánh được thiết kế để các nhà nghiên cứu bên ngoài có thể tự xác minh các bằng chứng.

Ono đặt toán học như một môi trường thử nghiệm cho tham vọng lớn hơn. Nếu các thuộc tính của phần mềm — như một chương trình có kết thúc hay không, hay đầu ra của nó có đúng cho mọi đầu vào — có thể được diễn đạt dưới dạng các phát biểu toán học chính xác, thì các hệ thống phát sinh từ AxiomProver có thể chứng minh chúng một cách hình thức, ông lập luận, hướng tới việc xác minh mã do AI tạo ra khi bắt đầu vận hành các hệ thống hạ tầng, tài chính và an ninh.

“Thế giới sắp chạy trên mã máy tính mà không ai đọc,” Ono nói. “AI đã có mặt và chúng ta không thể quay lưng — hình thức hoá bằng chứng là môi trường thử nghiệm để giải quyết điều tôi cho là thách thức quan trọng nhất mà chúng ta sẽ phải đối mặt từ AI.”

Hiện tại, sản phẩm giao nộp hẹp hơn và có thể kiểm tra được: một bản thiết kế của 41 tác giả, một thư viện Lean công cộng, và một bằng chứng được máy xác minh rằng các số nguyên tố cách nhau 246 không bao giờ cạn kiệt — người hàng xóm được xác minh gần nhất của giả thuyết số nguyên tố sinh đôi, và là mảnh nghiên cứu toán học sâu nhất mà một hệ thống AI đã kiểm tra từ đầu đến cuối.