Đại học Hồ Nam dùng OpenAI Codex chứng minh giả thuyết Hadwiger: Bước ngoặt mới cho toán học

Cùng tuần mà Claude hoàn thành việc chính thức hóa chứng minh Định lý cuối cùng của Fermat trong Lean, một bài báo đã xuất hiện trong hộp thư của tôi với tiêu đề: The Spherical Hadwiger Theorem (Định lý Hadwiger cầu). Giả thuyết Spherical Hadwiger, vốn là một bài toán mở từ khoảng năm 1974, mô tả một phần quan trọng nhưng chuyên biệt của cơ chế hình học tích phân. Tôi sẽ không đi sâu vào chi tiết của giả thuyết này ở đây; nếu quan tâm, bạn có thể xem phần thảo luận trong bài viết trước của tôi, nơi định lý này (khi đó vẫn là một giả thuyết) đã giúp đơn giản hóa đáng kể chứng minh cho một bổ đề nhỏ của tôi từ thời cao học.

Nhưng đi thẳng vào vấn đề: bản thảo mới này của Wang & Wu từ Đại học Hồ Nam dường như đã chứng minh được giả thuyết trên với sự hỗ trợ của AI. Phần cuối của bài báo có chứa tuyên bố từ chối trách nhiệm:

Trong quá trình chuẩn bị bản thảo này, OpenAI Codex đã được sử dụng để hỗ trợ phát triển các chi tiết chứng minh, xác định các lỗ hổng và những điểm cần làm rõ, tổ chức và trình bày bản thảo, cũng như biên tập tiếng Anh. Các tác giả đã xem xét và xác minh tất cả nội dung toán học có sự hỗ trợ của AI, đề xuất các thay đổi, đưa ra mọi quyết định cuối cùng về toán học và biên tập, đồng thời chịu hoàn toàn trách nhiệm về bản thảo.

Tuyên bố từ chối trách nhiệm này để ngỏ khả năng rằng Codex đã thực hiện một phần đáng kể công việc mà cho đến gần đây vẫn đòi hỏi một nhà toán học cấp nghiên cứu: phát triển các chi tiết chứng minh, tìm kiếm và sửa chữa các lỗ hổng, và dường như là cả viết bài báo. Hơn nữa, tác phẩm này rất chỉn chu và dễ đọc (nếu bạn là một nhà toán học nghiên cứu trong lĩnh vực này).

Cần nói rõ rằng, tôi chưa xác minh đầy đủ chứng minh này; tôi đã xem qua nó với Claude Fable và nó vượt qua được bước kiểm tra sơ bộ, nhưng để hiểu thấu đáo hoàn toàn thì cần nhiều năng lượng hơn mức tôi có lúc này. Không có ý nào ở đây là chỉ trích Wang & Wu—đây dường như là một bài báo tuyệt vời và rất đáng để nghiên cứu. Họ thậm chí đã tuân thủ tất cả các nguyên tắc sử dụng AI được nêu trong Tuyên ngôn Leiden.

Một cột mốc, gần gũi với bản thân

Đối với tôi, chứng minh của Định lý Spherical Hadwiger rất gần gũi. Tôi đã cố gắng chứng minh nó khi còn học cao học và đã thử lại một cách nửa vời với sự hỗ trợ của AI vào đầu năm nay. Đó không phải là một định lý gây chấn động dư luận. Nhưng điều đó cũng không cứu được nó.

Tôi lẽ ra không nên ngạc nhiên. Khi GPT-4 ra mắt, OpenAI đã công bố một báo cáo về tác động tiềm tàng của LLM đối với thị trường lao động. Mức độ công việc của các nhà toán học bị ảnh hưởng bởi AI là cao nhất trong bất kỳ danh mục nào mà họ mô hình hóa; báo cáo ước tính rằng 100% công việc của một nhà toán học có nguy cơ bị ảnh hưởng bởi LLM, trên ba mô hình lao động khác nhau. Cao hơn cả nhà văn, biên dịch viên, nghệ sĩ và nhà thiết kế đồ họa. Sự khác biệt duy nhất là các nhà toán học mất nhiều thời gian hơn một chút để bắt đầu cảm nhận được nỗi đau này.

Thật hấp dẫn, dù có phần kiêu ngạo, khi cho rằng sự chậm trễ trong việc thống trị của LLM trong toán học nảy sinh vì toán học cấp nghiên cứu là một trong những nỗ lực khó khăn nhất của con người. Tôi nghi ngờ rằng sự chậm trễ này cũng xuất phát từ việc toán học nghiên cứu có ít giá trị kinh tế—và ít dữ liệu đào tạo hơn—so với các lĩnh vực sáng tạo khác.

Hãy xem xét nhạc cổ điển. Xã hội của chúng ta không hỗ trợ các nhạc sĩ cổ điển theo cách mà chúng ta hỗ trợ các nhạc sĩ 'đại chúng'. Nhạc cổ điển đã được thể chế hóa, được gửi vào nhạc viện như một di tích. Một bộ phận nhỏ trong xã hội đã quyết định rằng khả năng biểu diễn nó là điều đáng bảo tồn và dành một phần vốn nhỏ cho mục đích đó: đào tạo những người trẻ tuổi và trả lương cho một vài nghệ sĩ giỏi nhất ở các thành phố lớn để họ làm việc chuyên nghiệp.

Liệu mô hình này có hiệu quả với các nhà toán học? Thật dễ hình dung: vào thời Euclid, toán học chủ yếu tồn tại như một hoạt động trí tuệ xứng đáng với một vài người có thiên hướng. Một nhạc viện toán học có thể giúp toán học phát triển ngay cả khi việc tạo ra các kết quả mới không còn khó khăn, mà chỉ khó ở việc hiểu và truyền đạt tầm quan trọng của chúng.

Nhưng toán học thuần túy đã nằm trong một "nhạc viện" rồi, được biết đến nhiều hơn với cái tên học viện. Bên ngoài trường đại học, cơ hội việc làm cho các nhà toán học thuần túy vẫn rất hạn hẹp. Các kết quả chỉ được hiểu bởi một nhóm nhỏ. Liệu có quan trọng không khi tất cả các kết quả khó đều sẽ sớm được máy tính chứng minh?

Điểm mấu chốt

Rất đáng để hỗ trợ mọi người tiếp tục nỗ lực văn hóa mà chúng ta hiện gọi là "toán học nghiên cứu". Toán học, đặc biệt là toán học thuần túy, luôn là việc truyền đạt những câu chuyện giúp chúng ta hiểu thực tại sâu sắc hơn. Bằng cách đơn giản hóa và trừu tượng hóa, chúng ta bắt đầu nhìn thấy cấu trúc ẩn giấu: các đường thẳng song song không bao giờ cắt nhau, hình cầu trông giống nhau theo mọi hướng, các số nguyên tố không bao giờ kết thúc. Nhưng các hệ thống hỗ trợ hiện tại cho các nhà toán học, giống như rất nhiều lĩnh vực sáng tạo khác của con người, cần phải thay đổi quyết liệt để xử lý những thực tế mới của AI.

Tuy nhiên, các cấu trúc khuyến khích hỗ trợ công việc này, giống như trong rất nhiều lĩnh vực sáng tạo khác, lại không phù hợp với những gì AI mang lại. Những công cụ này khiến việc xác định xem một lập luận phức tạp có đúng hay không trở nên khó khăn hơn, chưa nói đến việc ai xứng đáng nhận tài trợ, biên chế và danh tiếng. Lựa chọn trước mắt chúng ta là làm thế nào để tiếp tục khiến con người trở nên quan trọng khi những nỗ lực trí tuệ của họ đơn giản là không thể so sánh với máy tính. Khi trí thông minh chỉ bị giới hạn bởi silicon và điện năng, liệu chúng ta có sẵn lòng tiếp tục hỗ trợ một nền văn hóa có các nhà toán học? Tôi thực sự hy vọng là có.

Nhận các bài viết mới qua email. Không spam, chỉ có bài viết.

Xem Bài toán 3 trong luận án của Glasauer. ↩︎

Thực tế, chỉ sau khi tôi viết bài blog ban đầu, Giáo sư Rolf Schneider mới nhắc tôi rằng giả thuyết này vẫn còn là bài toán mở vào thời điểm đó. ↩︎

Tôi tự hỏi, đó là những chi tiết chứng minh nào? Tôi rất muốn xem toàn bộ bản ghi cuộc trò chuyện. Mặc dù chứng minh tuân theo cách tiếp cận sơ bộ trong Klain và Rota cho định lý Euclid, nhưng các chi tiết đòi hỏi phải vượt qua một vài trở ngại lớn, và tôi tò mò không biết bao nhiêu trong số đó đã được GPT 5.6 xác định và giải quyết. ↩︎