NĂM VẬT THỂ, MỘT SỐ HỮU HẠN ĐIỆU NHẢY HOÀN HẢO

Hãy hình dung vài ngôi sao hay hành tinh được sắp xếp chính xác đến mức cả nhóm có thể quay như một vật rắn mà không thay đổi hình dạng. Để điều đó xảy ra, lực hấp dẫn tác dụng lên mỗi vật thể phải hướng đúng về khối tâm của nhóm, với cường độ tỉ lệ với khoảng cách tới khối tâm. Những cách sắp xếp như vậy được gọi là cấu hình trung tâm (central configuration). Chúng là hình dạng của các nghiệm đặc biệt của bài toán n vật thể, trong đó các vật thể giữ nguyên hình mẫu tương đối, bao gồm cả các cân bằng tương đối quay như vật rắn.

Nếu một hình mẫu thỏa mãn, mọi bản sao được xoay, phóng to hay dịch chuyển của nó cũng thỏa mãn, nên các nhà toán học đếm chúng “sai khác một phép đồng dạng”.

Bài toán thứ sáu của Smale

Câu hỏi được phát biểu đơn giản: với mọi lựa chọn các khối lượng dương, số cấu hình trung tâm có hữu hạn không? Đây là bài toán thứ sáu trong danh sách các bài toán mở do nhà toán học Smale soạn ra.

Theo bài báo, tình hình trước đây như sau:

• Ba vật thể: đúng năm — hai tam giác đều của Lagrange và ba đường thẳng của Euler.
• Bốn vật thể: tính hữu hạn đã được Hampton và Moeckel chứng minh, với mọi khối lượng dương.
• Năm vật thể trên một mặt phẳng: Albouy và Kaloshin chứng minh tính hữu hạn năm 2012, nhưng chỉ cho các khối lượng nằm ngoài một tập ngoại lệ — một họ mỏng các tổ hợp khối lượng xác định bởi các phương trình đa thức, nơi lập luận của họ không còn đứng vững.

Đóng lại tập ngoại lệ

Tejasvi Singh Tomar loại bỏ tập ngoại lệ đó. Định lý chính: với mọi lựa chọn năm khối lượng dương, bài toán năm vật thể phẳng có hữu hạn cấu hình trung tâm, sai khác một phép đồng dạng.

Chiến lược đi theo Albouy và Kaloshin. Nếu có vô hạn cấu hình, chúng sẽ tạo thành một đường cong liên tục các nghiệm khi các phương trình được mở rộng sang số phức. Đi theo đường cong đó “ra vô cực”, khoảng cách giữa các vật thể phải biến đổi sao cho triệt tiêu nhau trong một thế cân bằng chính xác. Các vật thể tiến dần tới một trong mười sáu sơ đồ giới hạn mà Albouy và Kaloshin đã xác định, mỗi sơ đồ áp đặt các điều kiện lên khối lượng.

Công trình mới làm các điều kiện này trở nên chặt chẽ với mọi khối lượng dương, và loại bỏ từng trường hợp rắc rối một:

• các cấu hình trong đó bốn vật thể tạo thành một cụm chặt mà vật thể thứ năm tiến lại gần bị loại trừ bằng cách khai triển thế năng — đại lượng giữ không đổi dọc theo đường cong — tới các bậc ngày càng cao; với khối lượng dương, các điều kiện thu được mâu thuẫn nhau;
• hai sơ đồ khác được chứng minh là không bao giờ xảy ra;
• với mọi trường hợp còn lại, tác giả mô tả tất cả các điều kiện khối lượng tương thích bằng đại số máy tính chính xác — 2.206 hệ đại số — và với mỗi hệ, tạo ra một chứng chỉ số: một danh sách các số hữu tỉ mà các tính chất của chúng, khi được kiểm tra bằng số học chính xác, chứng minh rằng thế cân bằng là bất khả.

Cái bẫy do khối lượng âm giăng ra

Có một điểm vướng mà đại số thuần túy không thể lách qua. Một nhà toán học khác, Roberts, đã tìm ra vô hạn cấu hình trung tâm cho các khối lượng (1, 1, 1, 1, −¼) — với một khối lượng âm. Đổi dấu một số chỗ biến chúng thành vô hạn nghiệm của các phương trình phức hóa với khối lượng (4, 4, 4, 4, 1). Chúng không phải cấu hình thực, nhưng một lập luận chỉ nhìn vào các phương trình phức không thể phân biệt được.

Vì vậy, tại các khối lượng đó, và tại tỉ lệ liên quan (1, 1, 4, 4, 4), tác giả đếm trực tiếp các cấu hình thực, bằng một cuộc tìm kiếm trên máy tính dùng số học khoảng có bảo đảm:

• với khối lượng (1, 4, 4, 4, 4): 306 cấu hình sai khác phép quay và phép co giãn — 60 nằm trên một đường thẳng, 24 tạo thành ngũ giác lồi, số còn lại có một hoặc hai vật thể nằm bên trong;
• với (1, 1, 4, 4, 4): 294.

60 cấu hình thẳng hàng khớp với một lần đếm trước đây của Moulton.

Được máy kiểm tra

Một chứng minh dựa trên nhiều phép tính như vậy cần được kiểm chứng chặt chẽ. Mỗi chứng chỉ được kiểm tra lại bằng một chương trình riêng viết từ các định nghĩa trong bài báo. Trên hết, định lý được chứng minh trong trợ lý chứng minh Lean 4, một chương trình kiểm tra mọi bước logic. Chứng minh hình thức thậm chí không giả định các kết quả của Albouy và Kaloshin: nó tự suy ra lại những gì cần, tìm kiếm ra 1.376 sơ đồ có gắn nhãn thỏa mãn các quy tắc của họ. Nó còn được hai trình kiểm tra độc lập khác dành cho chứng minh Lean chấp nhận. Dựng nó từ đầu mất khoảng 860 giờ CPU.

Bài báo kết thúc bằng một tuyên bố ngắn: các công cụ AI tạo sinh đã được dùng để tìm ra và chứng minh các kết quả, viết các chương trình và bản hình thức hóa Lean, và soạn thảo văn bản. Các công cụ không được nêu tên.

Điều nó nói và không nói

Kết quả này liên quan tới năm vật thể trên một mặt phẳng. Nó chứng minh rằng số cấu hình là hữu hạn với mọi bộ khối lượng dương, nhưng chỉ đưa ra con số chính xác tại một vài tỉ lệ khối lượng được nghiên cứu.