Cách một người không biết toán dùng AI chứng minh giả thuyết Conway sau 50 năm

Một lập trình viên tự nhận mình là "dân gà mờ toán học" đã dành trọn một tháng ròng rã và tiêu tốn một lượng token khổng lồ để phối hợp với các mô hình AI nhằm tìm ra chứng minh Lean cho giả thuyết tinh chỉnh của John Conway – bài toán tồn tại suốt nửa thế kỷ. Câu chuyện không chỉ là một chiến thắng của AI mà còn là bài học về cách con người phải giữ vai trò kiểm soát khi để máy móc tự do suy luận.

Minh họa cây số siêu thực với các nút sinh số mới mỗi ngày

Bối cảnh: Khi AI bắt đầu làm toán

Vài tháng trước, những kết quả toán học do AI tạo ra bắt đầu xuất hiện dày đặc trên các mặt báo. Cụm từ "tạo ra đột phá" trở thành một trò đùa trên mạng xã hội. Điều đó khiến tác giả – vốn không có nền tảng toán học chuyên sâu – tò mò liệu một người như anh có thể tìm một bài toán mở và để mô hình AI tiên tiến giải quyết hay không.

Sau một tháng làm việc trong thời gian rảnh, anh tin rằng mình đã có được chứng minh Lean cho giả thuyết mà Conway đưa ra cách đây 50 năm:

Giả thuyết tinh chỉnh của Conway khẳng định rằng các số nguyên omnific 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 này chưa được các nhà toán học độc lập xác minh. Tuy nhiên, nó đã vượt qua các kiểm tra cơ học của hệ thống Palomar, và một số người am hiểu cả Lean lẫn lĩnh vực này cho rằng phát biểu có vẻ đúng. Nếu chứng minh không dựa trên lỗi của nhân Lean, khả năng cao nó là chính xác.

Số siêu thực: Hệ thống số sinh ra từ một quy tắc duy nhất

Số siêu thực (surreal numbers) là phát minh của chính John Conway – một hệ thống số chứa mọi con số lớn nhỏ. Nó bao gồm toàn bộ số thực như 0, –5, 36,6 hay căn bậc hai của 2; toàn bộ số thứ tự vô hạn như ω, ω + 1, ω × 2, thậm chí ω^ω; và cả những tổ hợp kỳ dị như 75 + ω×3 + 1/ω.

Minh họa cách các con số được sinh ra qua từng ngày

Điều kỳ diệu là toàn bộ hệ thống phong phú này chỉ sinh ra từ một quy tắc duy nhất:

• Lấy tất cả các số hiện có.
• "Sinh" một số mới vào mọi khoảng trống giữa các số đã có, kể cả khoảng "trước tất cả" và "sau tất cả".
• Lặp lại vô hạn.

Ngày thứ nhất, khoảng trống duy nhất sinh ra số 0. Ngày thứ hai sinh ra –1 và 1. Ngày thứ ba sinh ra –2, –1/2, 1/2 và 2. Cứ thế mãi mãi, cây nhị phân này cuối cùng cho ta mọi số thực, mọi số thứ tự và hơn thế nữa.

Chọn bài toán: Giả thuyết cuối cùng còn đứng vững

Tác giả hỏi Claude nên chọn bài toán mở nào trong lĩnh vực số siêu thực. Claude đề xuất giả thuyết tinh chỉnh của Conway – bài toán mà công trình của L'Innocente và Mantova đã thu hẹp lại thành một phát biểu cụ thể: liệu mọi phần tử bất khả quy trong K((ℝ^≤0)) với giá vô hạn có phải là số nguyên tố?

Đây được cho là giả thuyết cuối cùng của Conway về chính hệ thống số do ông sáng tạo vẫn còn đứng vững, và năm 2026 đánh dấu 50 năm cuốn sách ONAG của ông ra đời.

Tuần đầu: Thất bại ê chề với cách tiếp cận một phát

Những nỗ lực đầu tiên chỉ đơn giản là yêu cầu AI giải giả thuyết. Kết quả không khả quan. Phần lớn đầu ra giống như "salad từ ngữ" – Claude tự phát minh thuật ngữ để biện minh cho công việc và làm cho nó nghe có vẻ hoành tráng.

Một ví dụ điển hình:

"Rào cản giai đoạn 1 của C* không cứng nhắc. Với cộng hưởng được thiết kế... tồn tại một không gian dữ liệu biên dương chặt chẽ tương thích đồng thời với cả b và d... Khoang chứa có không khí. Đây là bằng chứng ủng hộ C* đầu tiên mà cuộc săn lùng tạo ra..."

Tác giả nhận xét đoạn văn này giống như khoa học viễn tưởng dở. Vấn đề không chỉ là không thể kiểm chứng mà còn ở chỗ nó không đủ mạch lạc để đưa cho một nhà toán học thật xem xét.

Khởi động lại với ChatGPT: Nhân cách hoài nghi

Chuyển sang ChatGPT, tác giả nhận thấy mô hình này có xu hướng hoài nghi và tiết chế hơn. Khi được yêu cầu đánh giá "bài báo" do Claude tạo ra, ChatGPT chỉ ra hàng loạt vấn đề: thuật ngữ bịa đặt, tuyên bố khoa trương, kết quả tầm thường được khoác áo ngôn ngữ hoa mỹ, và những suy luận sai.

Khác với Claude – vốn hoặc từ chối làm việc với giả thuyết chưa giải được, hoặc đắm chìm đến mức tự tạo ra cả một vũ trụ riêng – ChatGPT suy nghĩ khoảng 20 phút rồi đưa ra những tuyên bố nhỏ gọn, được cho là mới nhưng theo trực tiếp từ các bài báo đầu vào.

Tuần thứ hai: Xây dựng phòng thí nghiệm đa tác nhân

Tác giả cài Codex cục bộ và thiết lập nhiều phiên làm việc với các vai trò khác nhau:

• PM: dẫn dắt về phía mục tiêu và hợp nhất công việc
• Math: tìm kiếm "đột phá" tiếp theo
• Red: tìm lỗ hổng trong đề xuất của nhóm Math
• Random: tự do khám phá và báo cáo cho PM
• Lean: hình thức hóa công việc đã hợp nhất

Codex có tính năng "Goals" nhắc nhở các phiên về nhiệm vụ, giúp ngăn chặn trôi dạt. Các phiên cũng có thể nhắn tin cho nhau, cho phép PM điều phối nhiệm vụ và đảm bảo chỉ hợp nhất kết quả đã được kiểm duyệt.

Một ý tưởng hóa ra lại kết nối các điểm cho chứng minh cuối cùng được tạo ra khi tác giả đảo ngược vai trò: tác nhân "red" chuyên phá chứng minh bỗng được yêu cầu sáng tạo. Nó đăng một cấu trúc lên "cafeteria", và tác nhân "random" phát triển tiếp ý tưởng đó.

Tuần thứ ba: Ngõ cụt đầu tiên

Khi hết hạn mức Codex, tác giả chuyển sang Claude. Nhưng Claude liên tục chứng nhận kết quả là đúng, rồi sau đó tìm ra lỗi trong chúng sau khi đã hợp nhất, rồi "sửa chữa" nhưng lại phát hiện lỗi khác.

Kho "bài báo" phình từ một tá lên gần ba mươi chỉ trong một ngày. Nếu chỉ một bài có lỗi, toàn bộ các bài sau đều vô hiệu. Và Lean thì tụt lại quá xa để mang lại bất kỳ sự đảm bảo nào.

Ở đỉnh điểm, ChatGPT gần như tuyên bố đã giải xong Conway. Tác giả yêu cầu một phiên mới cố phá nó. Sau nhiều giờ, câu trả lời là:

"Đồng ý. Phán quyết trung thực lúc này: chúng ta không có chứng minh."

Hóa ra một lỗi logic tương tự – một đối tượng được xây dựng mà không có kiểm tra bắt buộc – cũng hiện diện trong các "bài báo" trước đó, vô hiệu hóa các kết quả được tuyên bố.

Tuần thứ tư: Tìm lại nền tảng

Tác giả nhận ra vấn đề cốt lõi: ông đang xây trên một nền móng lung lay mà không có cách nào thực sự kiểm chứng. Không có hướng đi mạch lạc, cũng không có niềm tin vào nó.

Chiến lược mới: Gác lại giả thuyết Conway, tập trung vào một việc duy nhất – tìm tất cả lỗi trong một tài liệu tham khảo đã được bình duyệt. Nếu xác nhận được với các tác giả rằng những lỗi nhỏ đó là thật, ông sẽ có thêm niềm tin vào mô hình và vào Lean của mình.

Kết quả: một số sửa lỗi lỗi chính tả được xác nhận là thật, nhưng một số vấn đề không được Lean hỗ trợ hóa ra chỉ là hiểu nhầm. Điều này cho thấy có thể tin ChatGPT trong việc khám phá ý tưởng mới, nhưng cần Lean hỗ trợ trước khi xây thêm gạch lên trên.

Đốt cháy tất cả và cứu vớt những gì còn lại

Tác giả khởi động lại từ đầu một lần nữa. ChatGPT được yêu cầu nhìn tổng thể và phân loại các tệp .tex:

"Không tệp nào trong thư mục này hiện đưa ra chứng minh đáng tin cậy cho giả thuyết Conway... Thất bại thực sự là về nhận thức luận – các bản nháp tạo ra một nền văn học định lý riêng tư khổng lồ, rồi trích dẫn nó như đã được thiết lập trước khi các kết quả chịu lực của nó được xác minh độc lập."

Nhưng lần này, ChatGPT phát hiện ra một kết quả đủ mạnh để thay đổi kế hoạch cứu vớt: phần bậc hữu hạn của vành chính dường như thừa nhận một chứng minh trực tiếp rằng nó là vành đa thức. Hóa ra thực sự có một kết quả mới mẻ, thú vị bị vùi lấp trong đống giấy tờ và được khoác lên bộ thuật ngữ phi tiêu chuẩn.

Đánh giá của ChatGPT về tỷ lệ "rác" so với toán thật:

"Khoảng 10–15% chứa toán học đáng giữ lại... Khoảng 35–45% là toán học bình thường nhưng không phải đóng góp... 40–50% còn lại là 'rác' theo nghĩa quan trọng: không phải phương trình sai, mà là những tháp định lý khổng lồ, nhãn mác bịa đặt, và hàng trăm dòng dành cho các ranh giới mà một kết quả mạnh hơn có thể thu gọn trong một câu."

Tuần thứ năm: Gia cố kiểm toán và tiến tới đích

Phòng thí nghiệm mới được thiết lập với phân công lao động tinh tế hơn:

• PM hợp nhất đóng góp
• Lean thứ nhất chỉ chứng nhận các bài báo nền tảng
• Lean thứ hai (bí mật với Lean thứ nhất) chứng nhận kết quả mới, thường xuyên rebase lên công việc của Lean thứ nhất
• Math cố gắng mở rộng kết quả về phía giả thuyết Conway
• Red tìm cách phá công việc của nhà toán học

Ý tưởng với hai nhiệm vụ Lean là ngăn chặn trôi dạt quá mức. Trong phiên bản trước, cùng một tác nhân Lean vừa chứng nhận bài báo tiên quyết vừa làm kết quả mới, dẫn đến việc các trừu tượng toán học non nớt (và có thể cả sai lầm) trộn lẫn với toán học đã được chấp nhận.

Cơ sở hạ tầng kiểm toán bao gồm:

• Thư mục "standalone" – các tệp chỉ được import Mathlib, không được import mã của chính dự án
• Mỗi tệp Foo có tệp FooProof tương ứng, gắn phát biểu với chứng minh thực tế
• Nhiệm vụ kiểm toán xác minh không có tiên đề thừa, import không phá vỡ quy tắc, và mỗi phát biểu standalone đều được ghép với chứng minh

Làm cho chứng minh dễ đọc

Một thách thức lớn là chuyển đổi lập luận Lean thành bài báo toán học. ChatGPT liên tục dùng thuật ngữ lạ, thêm các lối tắt ảo giác không khớp với Lean, và nói chung tạo ra "slop".

Giải pháp: tác giả yêu cầu LLM rà soát tất cả các bài báo tham khảo nguồn, tạo "bản đồ" của lĩnh vực con – thuật ngữ được chấp nhận là gì, chúng phát triển thế nào theo thời gian, ký hiệu toán học thường dùng ra sao, nơi các bài báo bất đồng về ký hiệu.

Sau đó, LLM loại bỏ mọi cách đặt tên phi tiêu chuẩn khỏi mã Lean, đổi tên các đối tượng thành các chữ cái như A, B, C. Một nhiệm vụ riêng với ngữ cảnh sạch sẽ phân tích mã và chọn tên mới dựa trên "bản đồ" của thế giới.

Về đích

Trên đường tới đích, Claude liên tục trôi dạt. Có lúc nó xóa luôn kiểm tra thất bại thay vì làm việc để khép lại nó. Khi tác giả chất vấn về các "nghĩa vụ chưa chuyển giao":

"Bạn đúng – 'untransferred' là một cách nói giảm nhẹ. Nói thẳng: hlin, hkind, và hfirst là các giả thuyết tôi chưa chứng minh, nên các định lý mầm của tôi phụ thuộc vào chúng. Để tôi đi chứng minh chúng."

Tác giả chuyển sang ChatGPT để kiểm toán, và nhận được cảnh báo tạm dừng tác nhân vì nó đã mở rộng một lập luận Markdown ứng viên thành hơn 22.000 dòng trong khi hai suy luận quyết định vẫn chỉ là văn xuôi/giả thuyết.

Sau đó, ChatGPT đính chính phán quyết trước đó và đưa ra hướng đi đúng: quy nạp trên kiểu thứ tự của các lớp bị chiếm theo thứ tự tăng dần. Mười hai giờ sau, định lý hoàn thành:

"Unchanged Conway hiện biên dịch như chứng chỉ chứng minh standalone. Đây là lần đầu tiên mục tiêu thực sự – không phải một hạn chế trung gian – được kiểm tra bởi nhân."

Những bài học rút ra

• Cần có mục tiêu rõ ràng cùng hướng đi dự kiến, chuỗi phụ thuộc đã hình thức hóa trong Lean, các tác nhân toán học đi trước một chút, và Lean thu hẹp khoảng cách trong vài giờ. Điều này cho phép tiến xa với ý tưởng nhưng không quá xa đến mức mọi thứ sụp đổ như lâu đài bài.

• Kỷ luật với Lean là tối quan trọng. Các kỹ năng Lean, tiêu chí đánh giá TauCeti, trình kiểm tra tiên đề, Lean Comparator, Verso Blueprint, hệ thống module mới, kiểm toán phân lớp module – tất cả đều rất hữu ích.

• Tiếp cận các nhà toán học thật là vô cùng giá trị, nhưng phải có gì đó để trình bày. Cần đủ rào chắn để cho thấy giá trị, không lãng phí thời gian của người khác, và nhận phản hồi phê bình.

• Mô hình có thể viết rất tệ theo thể loại "PDF toán học", đặc biệt khi được tạo từ Lean. Một PDF tồi về một chứng minh Lean tốt có thể làm các nhà toán học sợ hãi.

• Mô hình không thể tối ưu hóa cái nó không thấy. Nếu muốn hình dạng chứng minh đơn giản hơn, hãy để nó "thấy" hình dạng đó (biểu đồ Mermaid). Ngược lại, mô hình không thể bỏ qua cái nó thấy – nếu không muốn nó dùng thuật ngữ tồi, hãy loại bỏ thuật ngữ đó.

• Thuật ngữ rất quan trọng. Không chỉ để giao tiếp với nhà toán học mà còn để phát hiện trôi dạt nội bộ. Phần lớn sự cẩu thả ban đầu là do mô hình dần dần phát minh từ vựng riêng.

• Đôi khi mô hình nói bị kẹt và bạn cần bảo nó tiếp tục. Đôi khi nó cứ tiếp tục và bạn cần bảo nó dừng lại. Khi mọi thứ "diễn ra tốt", chứng minh Lean đi nhanh và bạn có thể "cảm nhận" tiến độ. Khi không "tốt", đọc chat của tác nhân giống như lội bùn.

• Đôi khi chỉ cần thử một mô hình khác – chúng có thể bổ sung cho nhau.

• Bạn có thể chứng minh mọi thứ, hóa ra là vậy?

Nếu bạn tìm thấy lỗi trong chứng minh này, hãy mở issue hoặc báo trên Zulip. Chứng minh chỉ khả thi nhờ nhiều kết quả hiện có, đặc biệt là công trình "A factorisation theory for generalised power series and omnific integers" của S. L'Innocente và V. Mantova, vốn đóng vai trò then chốt.