Dùng AI và Lean chứng minh giả thuyết Conway: Hành trình 1 tháng đầy tham vọng

Vài tháng trước, các kết quả toán học từ AI bắt đầu xuất hiện trên các tiêu đề báo chí. Cụm từ “tạo ra một bước đột phá” (do a breakthrough) đã trở thành một meme trên Twitter. Đương nhiên, tôi trở nên tò mò liệu bản thân mình, một “tay mơ” về toán học, có thể tìm ra một bài toán mở nào đó rồi nhờ một mô hình AI tiên tiến (frontier model) giải nó hay không.

Tôi đã mất trọn vẹn một tháng thời gian rảnh rỗi và tiêu tốn một lượng khổng lồ token, nhưng tôi tin rằng mình đã thu được một chứng minh bằng Lean cho giả thuyết này, vốn được John Conway đặt ra từ 50 năm trước:

Giả thuyết tinh chỉnh (refinement conjecture) của Conway cho rằng các số nguyên omnific (omnific integers) có tính chất tinh chỉnh: nếu ab = cd, thì tồn tại các số nguyên e, f, g, h sao cho a = ef, b = gh, c = eg, d = fh.

Chứng minh của tôi chưa được các nhà toán học kiểm chứng độc lập. Tuy nhiên, tôi có những lý do xác đáng để tin rằng chứng minh này đúng, và tôi thực sự hoan nghênh mọi phản biện.

Chứng minh đã vượt qua các bước kiểm tra máy móc từ hệ thống đăng ký Palomar, và một vài người am hiểu cả Lean lẫn lĩnh vực này đều cho rằng phát biểu đó có vẻ đúng. Vì vậy, giả sử chứng minh của tôi không dựa trên lỗi kernel của Lean, thì khả năng cao nó cũng là hợp lệ.

Trong bài viết này, tôi sẽ mô tả phương pháp của mình và một vài điều tôi đã học được trong suốt quá trình thực hiện.

Ngày đầu tiên

Tôi từng nghĩ ý tưởng “giải” một bài toán toán học mà không hiểu bản chất của nó là khá vô lý, điều này tất nhiên lại càng làm nó trở nên hấp dẫn hơn.

Tuy nhiên, tôi không chỉ muốn bất kỳ kết quả nào; tôi muốn một thứ gì đó thực sự lôi cuốn mình.

Chọn lĩnh vực

Tôi đã yêu cầu Claude chọn một bài toán mở trong lĩnh vực số siêu thực (surreal numbers). Nếu bạn chưa biết, số siêu thực là phát minh—hay là một khám phá?—của John Conway về một hệ thống số chưa từng được biết đến trước đó, bao gồm tất cả các số từ lớn đến nhỏ:

Điều đặc biệt kỳ diệu về số siêu thực (và lý do tôi cho rằng chúng có thể hấp dẫn một lập trình viên) là hệ thống phong phú này được sinh ra từ một quy tắc duy nhất.

Hãy lấy tất cả các số bạn có cho đến thời điểm hiện tại. Sau đó, “sinh ra” một số mới vào mọi khoảng trống giữa các số bạn đã có (điều quan trọng là “bên trái của tất cả” và “bên phải của tất cả” cũng được tính là các “khoảng trống”). Áp dụng bước này mãi mãi, bạn sẽ có được các số siêu thực.

Hãy thử suy ngẫm về điều đó.

Vào ngày đầu tiên, khoảng trống là “giữa không có gì và không có gì”. Số 0 ra đời.

đầu tiên, chúng ta cắt giữa không có gì và không có gì. điều này cho chúng ta 0

Vào ngày thứ hai, có hai khoảng trống: “giữa không có gì và số 0” và “giữa số 0 và không có gì”. Hai số được sinh ra trong hai khoảng trống đó. Hãy gọi chúng là –1 và 1.

bây giờ chúng ta có hai vị trí khác nhau có thể cắt. điều này cho chúng ta -1 và +1

Vào ngày thứ ba, có bốn khoảng trống: một khoảng “giữa không có gì và –1”, một khoảng “giữa –1 và 0”, một khoảng “giữa 0 và 1”, và một khoảng “giữa 1 và không có gì”. Đặt một số vào mỗi khoảng trống đó và đặt tên cho chúng: –2, –1/2, 1/2, và 2.

bây giờ chúng ta có bốn vị trí để thực hiện cắt. điều này cho chúng ta –2, –1/2, +1/2, +2

Vào ngày thứ tư, chúng ta lấp đầy tám khoảng trống với –3 và 3 ở các cạnh, cùng với –3/4, –3/2, 3/2, và 3/4 ở các khoảng trống còn lại:

bây giờ chúng ta có tám vị trí để thực hiện cắt. điều này cho chúng ta –3, –3/2, –3/4, –1/4, 1/4, 3/2, 3/2, 3

Giả sử chúng ta thực hiện việc này mãi mãi (vô hạn các bước), rồi tiếp tục mãi mãi (vô hạn của vô hạn các bước), và cứ thế tiếp diễn, không bao giờ ngừng sinh ra các số mới. Hóa ra, cây nhị phân dựa trên quy tắc duy nhất này cuối cùng sẽ cho chúng ta mọi số thực, mọi số thứ tự (ordinal), và nhiều hơn thế nữa, với các phép toán nhất quán trên chúng:

(Minh họa bởi Joel David Hamkins. Hãy đọc các bài viết của ông ấy và mua sách của ông ấy!)

Số siêu thực rất đẹp, và đó là lý do tại sao tôi yêu cầu Claude làm việc trong lĩnh vực đó.

Chọn bài toán

Ban đầu, tôi hỏi Claude:

Tôi: những bài toán chưa có lời giải nào trong chương trình nghiên cứu về Số siêu thực lôi cuốn bạn nhất và tại sao?

Nó gợi ý một vài vấn đề nhưng lưu ý rằng một số đã có tiến triển gần đây. Tôi hỏi:

Tôi: hãy cập nhật thông tin về những khía cạnh mà bạn muốn biết thêm. hãy làm theo sự tò mò của bạn. bạn cũng có thể tìm kiếm những thứ cũ hơn.

Sau đó, tôi yêu cầu nó thu hẹp lựa chọn xuống một thứ gì đó cụ thể:

Tôi: hướng nào lôi cuốn bạn nhất? tôi muốn bạn chọn một bài toán để thực hiện. hãy mạnh dạn lên!

Claude trả lời:

Claude: Tôi chọn số học của Conway. Cụ thể là câu hỏi mà bộ máy L’Innocente–Mantova vừa làm rõ — liệu mọi phần tử bất khả quy trong K((ℝ^≤0)) với giá trị hỗ trợ vô hạn có phải là số nguyên tố không? — điều này, theo sự rút gọn của họ, hiện tương đương chính xác với giả thuyết năm 1976 của Conway rằng bất kỳ hai cách phân tích thừa số nào của một số nguyên omnific đều thừa nhận một sự tinh chỉnh chung. Đó là giả thuyết cuối cùng của Conway về các con số của chính ông vẫn còn tồn tại, và năm 2026 là kỷ niệm 50 năm cuốn ONAG ra đời. Đó là bài toán tôi sẽ thực hiện.

Tôi vẫn không biết liệu đây có thực sự là giả thuyết cuối cùng còn tồn tại của Conway về số siêu thực hay không (hãy cho tôi biết nếu bạn biết!), nhưng việc năm nay là kỷ niệm 50 năm cuốn sách của ông đã thuyết phục tôi chọn bài toán này vì lý do tình cảm.

Đây là toàn bộ bản ghi từ phiên làm việc đó. Câu hỏi cuối cùng của tôi trong phiên đó là liệu chúng ta có cơ hội chính thức hóa phát biểu của giả thuyết trong Lean một cách tương đối ngắn gọn hay không—nếu không có điều đó, ngay cả khi tôi tìm ra chứng minh, cũng sẽ không có cách nào để tôi thuyết phục người khác xem xét nó. Claude nói rằng nó có thể được phát biểu mà không gặp nhiều khó khăn trong Lean, và câu trả lời đó có vẻ đúng, vì vậy tôi quyết định thực hiện dự án này.

(Lưu ý: Lúc đó tôi không biết, nhưng khẳng định của Claude về việc bài toán đã được rút gọn hoàn hảo là sai; thực tế việc chứng minh giả thuyết đòi hỏi nhiều hơn thế.)

Phát biểu bài toán

Mặc dù có lẽ bạn ở đây để tìm hiểu thêm về quy trình làm việc Lean/AI của tôi, tôi sẽ giải thích ngắn gọn về chính giả thuyết này, vì bạn đã biết đủ để hiểu nó rồi.