ChatGPT bác bỏ giả thuyết khoảng cách đơn vị của Erdős, AI tự động hóa chứng minh toán học

Vài tuần vừa qua là một khoảng thời gian thú vị đối với các phản ví dụ. Bài viết này về cơ bản là góc nhìn của tôi về những gì đang diễn ra trong thế giới của việc hình thức hóa (formalization), các công cụ AI và đặc biệt là các phản ví dụ.

Khoảng cách đơn vị (Unit distance)

Đúng hai tháng trước (ngày 20 tháng 5 năm 2026), ChatGPT đã bác bỏ giả thuyết Khoảng cách đơn vị của Erdős trong hình học rời rạc. Đây giờ đã là tin cũ nhưng tôi phải bắt đầu từ đâu đó. Thông báo này đi kèm với lời xác nhận từ các nhà toán học con người, nhiều người trong số họ tôi quen biết và một vài người tôi tin tưởng, nói rằng họ tin vào lập luận đó (họ đã được cấp quyền truy cập sớm và đã kiểm tra nó). Cấu trúc cơ bản của chứng minh là một định lý sâu sắc trong lý thuyết số của Golod và Shafarevich từ những năm 1960 có thể được sử dụng để xây dựng một phản ví dụ cho giả thuyết này.

Đã 9 năm kể từ khi tôi trải qua cuộc khủng hoảng tuổi trung niên, nhận ra mình không còn tin tưởng nhiều nhà toán học con người khi nói đến các chi tiết kỹ thuật, khám phá ra Lean và bắt đầu lập luận rằng các trình chứng minh định lý tương tác (interactive theorem provers) nên đóng một vai trò quan trọng trong tương lai của toán học. Vì vậy, tất nhiên câu hỏi đầu tiên của tôi là "phản ví dụ này có được hình thức hóa trong Lean không". Câu trả lời là "không".

Nhưng chưa đầy một tuần sau (ngày 26 tháng 5 năm 2026), tôi nhận được email từ người đạt huy chương Fields, Mike Freedman. Mike hiện là Giám đốc Khoa học của Logical Intelligence, một công ty do người chiến thắng giải thưởng Turing và là "cha đẻ của AI" Yann LeCun đồng sáng lập. Mike thông báo với tôi rằng hệ thống của họ đã tự động hình thức hóa toàn bộ bài báo do ChatGPT tạo ra trong Lean và liệu tôi có thể xem qua không. Tôi đã xem, và nghiên cứu sinh sau tiến sĩ Thomas Browning của tôi cũng xem. Và quả thực đây chính là điều mà Logical Intelligence đã làm: họ đã hình thức hóa chính xác tuyên bố rằng định lý sâu sắc của lý thuyết số đã dẫn đến phản ví dụ của Erdős. Toán học đột phá do LLM tạo ra đang được hình thức hóa trong thời gian thực. Một dữ liệu thú vị.

Tất nhiên, có một vấn đề lớn ở đây, đó là định lý sâu sắc của lý thuyết số vốn cần hơn 100 trang để chứng minh (nó cần những phần khổng lồ của lý thuyết trường lớp toàn cục (global class field theory), một lý thuyết được phát triển vào đầu thế kỷ 20 và vẫn chưa có chứng minh ngắn gọn nào; việc nén nó lại đang tỏ ra khó khăn). Năm 2025, tôi đã tổ chức một khóa học mùa hè Clay cùng với Richard Hill về việc hình thức hóa lý thuyết trường lớp, và một năm sau chúng tôi gần như đã hoàn thành trường hợp địa phương (đây là dự án tiến sĩ hiện tại của sinh viên tôi, Edison Xie); trường hợp toàn cục vẫn còn bỏ ngỏ, và thực tế vào năm 2025, việc hình thức hóa lý thuyết trường lớp toàn cục dường như là một điều viển vông.

Một tháng sau, vào ngày 26 tháng 6 năm 2026, nhận thức của tôi về những gì có thể thực hiện được lại thay đổi. Boris Alexeev thông báo trên Lean Zulip rằng anh ấy đã điều hướng ChatGPT đến một sự hình thức hóa hoàn chỉnh phản ví dụ của Erdős, mà không giả định bất cứ điều gì ngoài các tiên đề của toán học. Boris làm việc tại OpenAI và đã sử dụng mô hình mới Sol của họ để thực hiện việc tự động hình thức hóa. Boris đã công khai mã nguồn và tôi không mất nhiều thời gian để nhận ra rằng ở đâu đó trong tất cả mã nguồn do AI tạo ra (đôi khi rất tệ, mặc dù đôi khi cũng khá ổn) thực sự là một chứng minh cho một số định lý rất khó trong lý thuyết trường lớp toàn cục. Điều thú vị đối với tôi là Sol đã tạo ra 1,2 triệu dòng mã Lean trong ba tuần làm việc với dự án. Thư viện toán học tuyệt vời mathlib của Lean (tuyên bố xung đột lợi ích: tôi là người bảo trì) chỉ có 2,3 triệu dòng mã và mất chín năm để viết. Có lẽ chính tại thời điểm này, tôi mới thực sự hiểu ra — những bước phát triển toán học quy mô lớn do AI tạo ra là điều không thể tránh khỏi. Người ta không thể tin tưởng mã do AI tạo ra nên tôi đã chạy nó trong một môi trường sandbox trên máy tính của mình (mã Lean độc hại có thể chạy các lệnh tùy ý trên máy tính của bạn — xét cho cùng, Lean là một ngôn ngữ lập trình). Quả thực, nó đang chứng minh các định lý không tầm thường về đối đồng điều (cohomology) của các trường số. Chà.

Các lược đồ nhóm bậc n

Một tuần sau tiết lộ của Boris, vào đầu tháng 7, tôi đang suy nghĩ kỹ về cách tổ chức hội thảo Formalizing Fermat của mình. Hội thảo này được tài trợ bởi Logos Research, những người giống như Logical Intelligence (và Harmonic, Axiom AI, Moonshot AI...) có một công cụ có thể tự động hình thức hóa toán học — dịch từ ngôn ngữ con người sang Lean — dựa trên mathlib. Logos nói với tôi rằng họ chỉ cho phép 5 người sử dụng hệ thống của họ cùng lúc trong hội thảo, và có 25 người tham dự, vì vậy tôi đã nói với tất cả những người tham dự rằng tôi sẽ mua cho họ gói đăng ký Claude Max trong một tháng, để họ có thứ gì đó để thử nghiệm khi chưa đến lượt dùng công cụ của Logos. Hội thảo diễn ra từ ngày 6 đến ngày 10 tháng 7, và gói đăng ký Claude Max sẽ cho phép người tham dự truy cập Claude Fable, ít nhất là cho đến thứ Ba ngày 7, khi nó bị tắt. Khi OpenAI biết được những gì tôi đang làm, họ cũng cung cấp cho tất cả người tham dự quyền truy cập ChatGPT Pro miễn phí trong một tháng; đây là một vấn đề lớn vì ChatGPT Sol sẽ ra mắt vào ngày 9. Vì vậy, về cơ bản tất cả người tham dự sẽ có quyền truy cập vào Sol và Fable trong 4 trên 5 ngày của hội thảo, và công cụ của Logos trong cả tuần. Trên thực tế, quyền truy cập Fable không bị xóa vào ngày 7 nên chúng tôi còn ở tình thế tốt hơn nữa.

Tôi không chắc công cụ của Logos sẽ tốt đến mức nào, nhưng tôi muốn có một sự phát triển của lý thuyết các lược đồ nhóm phẳng hữu hạn (finite flat group schemes) trong Lean cho chứng minh Định lý lớn Fermat đang thực hiện của mình, vì vậy tôi đã tải một số bài báo kinh điển trong lĩnh vực này lên Fable và ChatGPT, và yêu cầu chúng cùng viết một bài trình bày về lý thuyết này bằng ngôn ngữ tự nhiên. Tôi đã chuyển tài liệu pdf này cho Logos vào ngày trước hội thảo, và vào ngày đầu tiên của hội thảo, họ nói rằng một trong những tuyên bố trong pdf là sai và họ đã tìm thấy một phản ví dụ rõ ràng. Lại một phản ví dụ nữa! Tôi xem qua và quả thực tài liệu pdf do LLM tạo ra đã sai ở một điểm nào đó khi mô tả một cấu trúc tiêu chuẩn; báo động giả. Tuy nhiên, tôi đã bỏ lỡ điều này khi đọc qua pdf. Thật thú vị khi AI lại tìm thấy một phản ví dụ. Tôi đã sửa lại pdf. Tôi thấy thú vị là AI không chỉ nói "Tôi không hoàn toàn hiểu lập luận này", mà thay vào đó nó nói "đây là chứng minh cho thấy lập luận này hoàn toàn sai", một tuyên bố mạnh mẽ hơn nhiều.

Với việc phát triển lý thuyết các lược đồ nhóm phẳng hữu hạn đi đúng hướng, tôi có thể thư giãn trở lại với hội thảo FLT. Vào thứ Ba ngày 7 tháng 7, tôi ngồi đối diện với Akhil Mathew trong bữa trưa; Akhil là giáo sư toán học tại UChicago và anh ấy là một người tham dự đã thử nghiệm các công cụ có sẵn. Chúng tôi nói về các câu hỏi tiềm năng mà AI có thể giải quyết, và Akhil nêu ra câu hỏi cũ của Grothendieck về việc liệu mọi lược đồ nhóm tự do hữu hạn bậc n có bị triệt tiêu bởi n hay không. Deligne đã chứng minh kết quả này trong trường hợp giao hoán, và Grothendieck đã chứng minh nó khi cơ sở là rút gọn; Rene Schoof đã chứng minh nó trong nhiều trường hợp hơn, và thậm chí còn có một bài báo của Emiliano Torti được xuất bản năm ngoái, chứng minh nó ở mức độ tổng quát hơn nữa. Tôi nói rằng tôi nghĩ đây là một điều tuyệt vời để AI suy nghĩ.

Một ngày sau khi hội thảo kết thúc, vào thứ Bảy ngày 11 tháng 7, tôi nhận được tin nhắn từ Akhil nói rằng Sol đã tìm thấy một phản ví dụ. Anh ấy gửi cho tôi một tệp pdf dài 12 trang. Tôi trả lời ngay rằng tôi sẽ không đọc toán học không chính thức do AI tạo ra và liệu anh ấy có thể hình thức hóa toàn bộ mọi thứ trong Lean không. Bốn giờ sau, anh ấy trả lời lại, nói rằng Fable đã tự động hình thức hóa toàn bộ mọi thứ. Tôi quét qua tệp Lean dài 1076 dòng, kiểm tra xem mã đó không xóa tất cả các tệp trên ổ cứng của tôi (Lean là một ngôn ngữ lập trình, vì vậy nó có thể làm điều này). Tin rằng đó chỉ là các định lý, tôi đã biên dịch nó trên máy tính xách tay của mình và mất chưa đầy 5 phút để kiểm tra rằng (a) tuyên bố của định lý được khẳng định chỉ sử dụng các khái niệm trong mathlib (và do đó những thứ như HopfAlgebra có thể được tin tưởng là có nghĩa như những gì các nhà toán học nghĩ về đại số Hopf) (b) tuyên bố của định lý được khẳng định là có một phản ví dụ và (c) chứng minh đã biên dịch thành công. Tại thời điểm này, tôi biết rằng chúng tôi đã có một phản ví dụ — một lược đồ nhóm bậc 4 không bị triệt tiêu bởi 4. Tôi gợi ý Akhil thực hiện một PR (pull request) vào mathlib với phản ví dụ đó — và anh ấy đã làm. Tôi cũng đã gợi ý anh ấy soạn một thông cáo báo chí nói rằng một cỗ máy đã giải quyết được câu hỏi 60 năm tuổi của Grothendieck trong hình học đại số, nhưng bằng cách nào đó đến thời điểm này tôi gần như đã trở nên miễn nhiễm với tất cả những điều này. Tôi không rõ liệu giới truyền thông có thể phân biệt giữa "cỗ máy giải quyết câu hỏi của Erdős" và "cỗ máy giải quyết câu hỏi của Grothendieck" hay không, mặc dù cá nhân tôi thấy cái sau thú vị hơn nhiều. Tất nhiên, phản ví dụ của Grothendieck dễ hơn nhiều so với của Erdős (một nghìn dòng, không phải một triệu), tất cả những gì tôi muốn nói là đó là một lĩnh vực toán học mà cá nhân tôi thấy thú vị hơn. Tôi đã chỉ ra với Akhil rằng các cỗ máy dường như đang trở nên rất giỏi trong việc tìm kiếm các phản ví dụ và gợi ý anh ấy thử với giả thuyết Hodge tiếp theo.

Các định lý nâng mô-đun (Modularity lifting theorems)

Tôi nghĩ rằng cần phải lùi lại một bước tại thời điểm này và khảo sát thái độ của các chuyên gia con người đối với những điều này. Vào thứ Ba (14 tháng 7), tôi đến làm việc tại Imperial và phản ví dụ của Grothendieck là chủ đề bàn tán trong bữa trưa. Một thành viên trong khoa (tôi sẽ không nêu tên) nói với tôi rằng việc phản ví dụ quá dễ tìm chỉ cho thấy con người đã không dành đủ thời gian để suy nghĩ về vấn đề này, ngụ ý rằng một câu hỏi 60 năm tuổi của Grothendieck thực sự không thú vị để nghiên cứu. Tôi không nói với ông ấy rằng vào một thời điểm nào đó trước đây trong sự nghiệp, tôi đã dành cả tuần để làm việc cật lực với vấn đề này. Trong tâm trí tôi, đồng nghiệp của tôi chỉ đang trải qua năm giai đoạn của sự đau buồn; ngay bây giờ họ dường như đang ở giai đoạn phủ nhận.

Sau bữa trưa, tôi gặp nghiên cứu sinh tiến sĩ Andrew Yang của mình, người đã làm việc về việc hình thức hóa một định lý nâng mô-đun trong Lean, một điều rất quan trọng đối với công việc FLT của tôi. Andrew đã đến hội thảo FLT của Logos và hiện có quyền truy cập vào cả Sol và Fable. Anh ấy nói với tôi rằng sử dụng các công cụ này, anh ấy đã viết 250 nghìn dòng mã Lean, về cơ bản đã hoàn thành dự án trong khoảng thời gian mà tôi đoán là 2 tuần.

Vài ngày trước, tôi nhận được email từ một giáo sư trong khoa toán tại Imperial, bày tỏ sự ngạc nhiên rằng một số sinh viên tốt nghiệp của chúng tôi đang trả 200 đô la mỗi tháng để truy cập các mô hình như Sol và Fable. Ông ấy nói rằng ông ấy nghĩ những người này bị điên. Tôi không trả lời ngay. Nhưng sau khi gặp Andrew, tôi đã gửi email lại cho vị giáo sư đó và nói với ông ấy rằng theo ý kiến của tôi, bất kỳ sinh viên tiến sĩ nào không trả 200 đô la mỗi tháng để truy cập các công cụ này mới là người điên. Trên thực tế, trong hội thảo, tôi biết được từ sinh viên tiến sĩ Bryan Wang của Harvard rằng Harvard đã cung cấp quyền truy cập Fable miễn phí cho tất cả sinh viên tiến sĩ, nghiên cứu sinh sau tiến sĩ và giảng viên tại Harvard.

Giả thuyết Jacobian

Nhưng quay lại với Akhil. Tôi không chắc liệu anh ấy có coi ý tưởng bác bỏ giả thuyết Hodge của tôi là nghiêm túc hay không. Nhưng có vẻ như anh ấy đã hiểu sâu sắc rằng, với những công cụ AI mới phi thường này, các phản ví dụ có thể là những quả ngọt dễ hái ngay lúc này. Anh ấy đã thảo luận với Levent Alpöge về ý tưởng tìm thêm các phản ví dụ trong hình học đại số, và 12 giờ trước, Levent đã đăng trên X rằng Fable đã tìm thấy một phản ví dụ cho Giả thuyết Jacobian. Đây là một vấn đề lớn — đây là một câu hỏi nổi tiếng trong hình học đại số đã tồn tại 100 năm và nhiều người đã suy nghĩ về nó. Nó dường như đã được giải quyết trong trận Chung kết World Cup 2026.

Tôi thức dậy hôm nay với một tin nhắn từ Akhil nói rằng "tôi có nên thực hiện một PR khác không?" nhưng lần này anh ấy đã quá muộn — Paul Lezeau đã hình thức hóa phản ví dụ theo cách thủ công và đã thực hiện một PR vào kho lưu trữ Formal Conjectures của DeepMind. Mathlib không chứa một danh sách lớn các giả thuyết trong toán học, nhưng kho lưu trữ của DeepMind thì có. Tầm quan trọng của việc hình thức hóa các giả thuyết bởi con người là nếu con người đồng ý rằng một tuyên bố Lean nắm bắt trung thực ý tưởng đằng sau một giả thuyết, thì việc kiểm tra xem mã Lean (có thể do AI tạo ra) có bao gồm một chứng minh hoặc bác bỏ giả thuyết đó hay không là một việc tầm thường. Xin chúc mừng Levent, cảm ơn Akhil vì đã gợi ý vấn đề cho anh ấy, và cảm ơn DeepMind vì đã hình thức hóa tuyên bố đó và do đó làm cho việc xác minh chính thức phản ví dụ trở nên tầm thường.

Giả thuyết Jacobian đã được giải quyết! Chà! Bước tiếp theo trong công việc đó là con người cần hiểu chính xác điều gì đang xảy ra với ví dụ này. Vì giá trị thực sự của công việc như thế này là mang lại cho con người sự hiểu biết tốt hơn về toán học. Quả thực, Akhil đã làm việc để cố gắng hiểu phản ví dụ của Grothendieck theo cách sâu sắc hơn nhiều so với việc "đây là một cách trình bày ngẫu nhiên của một vành ngẫu nhiên và một phép tính ngẫu nhiên cho thấy điều gì đó không hoạt động". Điều chúng ta cần tiếp theo là sự hiểu biết sâu sắc có thể rút ra từ những ví dụ phi thường này.

Thật là một thời đại tuyệt vời để được sống.