Tham vọng thay đổi toán học bằng AI của Terence Tao

Terence Tao chưa bao giờ e ngại những ý tưởng khác thường. Tháng 11 năm 2014, ông tham gia một buổi tọa đàm cùng bốn nhà toán học xuất chúng khác, tất cả đều là những người đầu tiên nhận Giải thưởng Đột phá về Toán học trị giá đến 3 triệu USD. Trong suốt 40 phút thảo luận, những phát biểu gây kinh ngạc nhất đến từ Tao.

Ông dự đoán rằng trong tương lai, thay vì làm việc độc lập hoặc trong các nhóm nhỏ hai ba người, các nhà toán học có thể sẽ tham gia vào các dự án cùng lúc với hàng trăm cộng sự. Và khi những màn hợp tác này kết thúc, ông nhận định, bằng phong thái khiêm tốn và chừng mực của mình, kết quả có thể sẽ không được thẩm định bởi con người mà bởi máy tính. "Một ngày nào đó, chúng ta sẽ không viết các bài báo khoa học bằng [hệ thống soạn thảo công thức toán học] LaTeX nữa, mà bằng một một ngôn ngữ để các phần mềm thông minh có thể hiểu. Thỉnh thoảng bạn sẽ nhận được thông báo lỗi biên dịch, máy tính không hiểu bạn đã suy luận bước này như thế nào," ông chia sẻ.

Lúc đó người ta nghĩ đó là một ý tưởng hoang đường đến mức, so với nó, giả thuyết chúng ta đang sống trong một thế giới mô phỏng dường như lại có lý hơn rất nhiều. Ngạc nhiên hơn cả là viễn cảnh hàng trăm nhà toán học có thể cùng làm việc với nhau lại hấp dẫn Tao. Bởi nếu như có ai trên thế giới này đặc biệt phù hợp việc nghiên cứu độc lập, người đó chính là thần đồng Tao.

Từ thần đồng toán học đến người thay đổi cách làm toán

Tao sinh năm 1975 tại Adelaide, Australia, ba năm sau khi cha mẹ ông di cư từ Hong Kong đến đất nước này. Khi Tao lên hai tuổi, trong một lần gia đình đến thăm bạn bè, cha mẹ Tao bắt gặp con mình đang ngồi cùng vài đứa trẻ sáu tuổi, hướng dẫn chúng đếm số bằng những khối gỗ. Khi được hỏi đã học đếm từ đâu, Tao trả lời rằng cậu xem được trên chương trình Sesame Street. Tao bắt đầu học giải tích khi lên bảy tuổi.

Mùa xuân năm 1985, cha mẹ đưa Tao đến Mỹ, nơi cậu gặp Julian Stanley, Giám đốc chương trình Nghiên cứu Thanh thiếu niên có Năng khiếu Toán học (Study of Mathematically Precocious Youth), khi đó đặt tại Đại học Johns Hopkins. Stanley miêu tả Tao là người có năng lực toán học xuất sắc nhất mà ông từng chứng kiến. Cùng năm đó, Tao gặp gỡ nhà toán học lừng danh Paul Erdős khi ông đến thăm Adelaide. Một bức ảnh nổi tiếng ghi lại cảnh Erdős, lúc đó 72 tuổi, với dáng vẻ như một người ông hiền từ, đang đọc tài liệu đặt trên đùi, trong khi Tao, cậu bé mười tuổi với mái tóc đen dày, chăm chú quan sát, những ngón tay đưa lên cằm đầy suy tư.

Danh tiếng thần đồng của Tao tiếp tục vang xa khi cậu tham dự Olympic Toán học Quốc tế năm 1986. Ngay lần đầu dự thi, Tao giành huy chương đồng và trở thành thí sinh trẻ nhất từng đạt thành tích này khi mới mười tuổi. Trong hai năm tiếp theo, cậu lần lượt trở thành người trẻ nhất giành huy chương bạc, rồi người trẻ nhất giành huy chương vàng. Con đường học tập của Tao cũng tiến nhanh không kém. Ông tốt nghiệp Đại học Flinders tại Adelaide khi mới 15 tuổi và vào mùa thu năm 1992, Tao cùng cha lên máy bay đến bang New Jersey, Mỹ, để bắt đầu chương trình tiến sĩ toán học tại Đại học Princeton. Trong thư giới thiệu cho Terence Tao, Erdős viết: "Tôi tin rằng cậu ấy sẽ trở thành một nhà toán học hàng đầu, thậm chí là một nhà toán học thực sự vĩ đại".

Erdős đã đúng. Khi mới 24 tuổi, Tao đã có đủ thành tựu để đảm nhận vị trí giảng viên cơ hữu tại nhiều trường đại học. Cuối cùng, ông quyết định gắn bó với Đại học California tại Los Angeles (UCLA). Trong thời gian này, ông gặp Ben Green, một nhà lý thuyết số trẻ tuổi người Anh. Hai nhà toán học trẻ bắt đầu hợp tác tìm cách chứng minh rằng những dạng quy luật nhất định, gọi là cấp số cộng (các số cách nhau cùng một khoảng, ví dụ 1, 4, 7, 10, cách nhau ba đơn vị) chắc chắn sẽ xuất hiện trong những tập hợp lớn các số nguyên tố, dù các số nguyên tố có vẻ phân bố ngẫu nhiên và khó đoán trên trục số. Chứng minh này trở thành thành tựu nổi bật trong giai đoạn đầu sự nghiệp của Tao, góp phần mang về cho ông Huy chương Fields năm 2006 và đưa ông vào hàng ngũ những nhà toán học hàng đầu thế giới.

Hoạt động nghiên cứu của Tao trải rộng trên một phạm vi đề tài lớn đến khó tin, từ lý thuyết số giải tích, bao gồm định lý Green–Tao về các số nguyên tố, đến ngành giải tích, nơi ông nghiên cứu các tính chất của hệ phương trình Navier–Stokes mô tả hành vi của chất lưu, rồi cả những thuật toán tái tạo hình ảnh cộng hưởng từ (MRI) từ dữ liệu số.

Khát khao khám phá thông qua hợp tác thúc đẩy Tao công khai phần lớn quá trình nghiên cứu của mình. Năm 2007, Tao lập một blog cá nhân [1], nơi ông bắt đầu thường xuyên đăng tải những cập nhật về công việc nghiên cứu và hy vọng những cuộc bình luận dưới các bài đăng có thể khơi nguồn cho các ý tưởng mới.

Timothy Gowers, một trong những nhà toán học danh tiếng cũng từng giành giải Fields và là blogger toán học đời đầu khác cũng có những suy nghĩ tương tự. Tháng 1/2009, Gowers đăng một bài viết bày tỏ mong muốn tạo điều kiện cho một hình thức "hợp tác toán học quy mô lớn" hoàn toàn mới. Ông sẽ đưa ra một bài toán trên diễn đàn trực tuyến mở, và "bất cứ ai có điều gì muốn nói về bài toán đó đều có thể đóng góp". Ông đặt tên sáng kiến là Dự án Polymath.

Tao ngay lập tức ủng hộ dự án này. Bằng cách chia các bài toán lớn thành những trường hợp riêng biệt, các nhóm hoặc cá nhân có thể làm việc độc lập, sau đó ghép kết quả của họ thành những mảnh của một bức tranh lớn hơn. Tao cũng biết rằng có lẽ thách thức lớn nhất của mô hình Polymath là khâu tổ chức: điều phối các đóng góp và kiểm tra để bảo đảm tất cả đều chính xác.

Trong dự án Polymath đầu tiên, Gowers đề xuất cải thiện một kết quả được gọi là định lý Hales–Jewett, liên quan đến những quy luật xuất hiện khi tô các ô trong một lưới bằng một trong hai màu khác nhau. Sau vài tháng làm việc, được điều phối thông qua hàng nghìn bình luận của hàng chục nhà toán học, cả nhóm đã chứng minh được một phát biểu chính xác hơn về cách những quy luật tô màu ấy xuất hiện. Mùa thu năm đó, họ công bố công trình dưới dạng một bài báo toán học chưa từng có tiền lệ với bằng bút danh chung "D.H.J. Polymath". Thử nghiệm của Gowers đã thành công rực rỡ. Nó cho phép nhiều nhà toán học, cả chuyên nghiệp lẫn nghiệp dư, cùng làm việc và cuối cùng đưa ra được một phép chứng minh.

Trong mười năm tiếp theo, có thêm 15 dự án Polymath ra đời, một số dự án trong này do Tao dẫn dắt. Dự án Polymath lại là một ý tưởng đi trước thời đại. Tao phấn khích khi được sống trong một bầu không khí hoạt động toán học sôi nổi, nhưng ông cũng nhận ra rằng phần bình luận của blog là một nền tảng hợp tác còn nhiều hạn chế. Hợp tác mở trên quy mô lớn làm tăng cơ hội xuất hiện những khám phá bất ngờ nhưng đồng thời cũng làm tăng khả năng một trong số đông đảo người tham gia mắc sai sót. Cách duy nhất để ngăn ngừa lỗi là phải có người điều phối kiểm tra toàn bộ công việc.

Chính nút thắt trong khâu kiểm tra ấy lại làm suy yếu tầm nhìn của Polymath.

Theo ông, để biến tầm nhìn ấy thành hiện thực, cần có một hình thức kiểm chứng bằng máy tính, giúp tự động kiểm tra các đóng góp thay vì làm thủ công. Với trình độ công nghệ trong những năm 2010, mong ước ấy giống như mơ đến dịch vụ chở hành khách lên sao Hỏa vậy.

Dẫu vậy, tiềm năng của nó vẫn khiến ông tò mò. Terence Tao có lẽ là trường hợp hiếm hoi trong giới toán học tinh hoa nhận thấy triển vọng của phương pháp nghiên cứu toán học mới này.

Tháng 7/2022, để thỏa mãn trí tò mò, ông tổ chức một hội thảo về những cách thức khác nhau mà máy tính đang hỗ trợ nghiên cứu toán học. Trong những thành viên tổ chức hội thảo có cả Kevin Buzzard, "nhà truyền giáo" nổi bật nhất của toán học hình thức (formal mathematics - phương pháp biểu diễn và chứng minh các định lý bằng ngôn ngữ logic chặt chẽ để máy tính có thể kiểm tra tính từng bước suy luận).

'Toán học hình thức' và máy tính thay người kiểm chứng chứng minh

Thời điểm đó, Tao vẫn đánh giá Lean, phần mềm cho phép viết và kiểm tra các chứng minh toán học dưới dạng mã máy tính, là một chương trình phức tạp mà ông sẽ phải mất nhiều tháng để học.

Ngày 9/10/2023, Tao chia sẻ trên mạng xã hội: "Cuối cùng tôi đã quyết định làm quen với hệ thống chứng minh tương tác #Lean4 (với sự hỗ trợ của AI khi cần thiết để giúp tôi sử dụng nó)".

Trên MathOverflow (một diễn đàn thảo luận trực tuyến phổ biến dành cho các nhà toán học), Tao bắt gặp một câu hỏi về một khái niệm gọi là bất đẳng thức Maclaurin. Đầu tiên, ông trình bày lời giải dưới dạng một bài báo toán học thông thường, sau đó, ông xem liệu mình có thể hình thức hóa chứng minh đơn giản ấy bằng phần mềm Lean hay không.

Ban đầu, Tao nghĩ mình có thể hoàn thành dự án trong một tuần nhưng ông nhanh chóng phải đối mặt với những khác biệt giữa việc viết toán bằng tay và nhập toán vào Lean. Những phần khó của chứng minh lại dễ hình thức hóa bằng Lean, trong khi những phần đơn giản đòi hỏi phải bỏ nhiều công sức.

Phải đến gần một tháng sau, Tao mới đăng bình luận trên blog: "Chỉ xin thông báo rằng tôi đã hình thức hóa được các kết quả của bài báo này bằng Lean4". Kết quả ấy không lớn, còn đoạn mã Lean ông viết để hình thức hóa chứng minh thì rất tệ. Tuy nhiên, đến giờ Tao đã chính thức trở thành một thành viên có đóng góp cho cộng đồng Lean.

Song song với học Lean, Tao vẫn tiếp tục hàng loạt dự án nghiên cứu khác. Trong số đó có một dự án hợp tác với những cộng sự lâu năm là Ben Green và Tim Gowers, cùng Freddie Manners, cựu nghiên cứu sinh của Green và hiện là giáo sư tại Đại học California ở San Diego. Đây thật sự là một nhóm cộng sự xuất chúng.

Nhóm tập trung vào một bài toán cụ thể, xoay quanh một đối tượng toán học gọi là tập tổng (sumset). Liệu cách sắp xếp các con số có liên quan đến kết quả thu được khi cộng chúng với nhau?

Hãy lấy các số từ 1 đến 10. Ghép từng cặp số khác nhau rồi cộng lại, ta thu được nhiều kết quả. Nhưng có những phép cộng cho cùng một đáp án: 1 + 6, 2 + 5 và 3 + 4 đều bằng 7. Vì vậy, dù có nhiều cách cộng, số kết quả khác nhau lại tương đối ít. Các nhà toán học muốn tìm hiểu mối liên hệ giữa đặc điểm này và những quy luật của tập hợp ban đầu.

Đầu những năm 2000, Gowers, Green và Tao đã đạt được một số tiến triển trong việc chứng minh mối liên hệ ấy, nhưng cuối cùng vẫn rơi vào bế tắc.

Đến năm 2023, Tao, Green và Manners quay lại bài toán, với ý định đưa vào những kỹ thuật của lý thuyết xác suất mà Manners đã phát triển.

Họ nhận ra rằng bằng cách kết hợp những kỹ thuật này với các ý tưởng trước đó của Gowers, họ có thể giải quyết toàn bộ bài toán này [2]. Họ mời Gowers tham gia trở lại, và nhóm bốn người đạt được những tiến triển đều đặn trong suốt mùa hè năm 2023. Đến cuối mùa thu, họ đã tìm ra lời giải [3].

Đang say mê Lean, Tao đề xuất với ba đồng tác giả rằng họ có thể thử giải toán với Lean. Có điều, Green, Gowers và Manners không mấy hứng thú với Lean nên Tao quyết định tự mình bắt đầu. Ông tin mình sẽ không đơn độc vì bất kỳ dự án nào do ông dẫn dắt đều có khả năng thu hút sự chú ý của cộng đồng.

Ngày 13/11/2023, Tao mở một kênh mới trong nhóm trò chuyện dành cho những người quan tâm đến phần mềm Lean và viết "rất vui được đón nhận các tình nguyện viên đóng góp cho dự án trong bất kỳ khả năng nào mà họ cảm thấy mình có thể đảm nhận".

Đây là sự tái khởi động của Dự án Polymath, chỉ khác rằng lần này toàn bộ công việc sẽ được máy kiểm chứng, đồng nghĩa Tao không phải tự mình kiểm tra.
AI xử lý các bài toán nhỏ, còn nhà toán học xuất sắc tập trung vào câu hỏi khó nhất

Yaël Dillies, một nghiên cứu sinh tại Đại học Cambridge, nhanh chóng thiết lập hạ tầng kỹ thuật cho dự án, chia chứng minh thành 13 phần. Trong mỗi phần, Tao sẽ xác định trình tự các bổ đề và định nghĩa cần được hình thức hóa cho máy hiểu.

Bên cạnh việc hình thức hóa toán học, Tao và những người khác còn dành cả tuần đầu tiên để tìm ra cách phối hợp với nhau. Ban đầu, cuộc trao đổi diễn ra khá tự do, Tao đăng những việc ông cho rằng cần làm, những người khác tham gia đề xuất cách thực hiện, tương tự cách các dự án Polymath từng diễn ra trước đây.

Ngày 22/11/2023, Tao đăng danh sách 22 bổ đề còn chưa được giải quyết và viết: "Nếu bạn muốn nhận thực hiện một hoặc nhiều bổ đề trong số này, hãy trả lời ngay trong chuỗi thảo luận này".

Các phản hồi lập tức đổ về. "Tôi muốn nhận phần entropy của một biến ngẫu nhiên phân phối đều :)", Paul Lezeau, nghiên cứu sinh tiến sĩ tại Trường Hình học và Lý thuyết số London, viết. "Tôi sẽ thử sức với đồng nhất thức phân thớ tổng quát", Aaron Anderson, nghiên cứu sinh tiến sĩ tại UCLA, trả lời.

Tiếng lành đồn xa, ngày càng nhiều nhà toán học tham gia. Đến cuối tháng 11/2023, Tao giống như một điều phối viên tình nguyện bận tối mắt, hầu như không còn tự viết mã Lean mà tập trung tìm việc để giao cho những người khác. Ngày 28/11, ông viết: "Do dự án đang gần hoàn thành và chúng ta có thể tạm thời có nhiều tình nguyện viên hơn số công việc hiện có, tôi nghĩ ra thêm một nhiệm vụ nhỏ mà có lẽ ai đó sẽ sẵn lòng thực hiện".

Bốn mươi sáu phút sau, Kim Morrison, một kỹ sư nghiên cứu cấp cao chuyên về Lean và toán học hình thức, trả lời rằng nhiệm vụ đã hoàn thành.

Cộng đồng Lean đã bắt đầu thảo luận về ý nghĩa của dự án này. Đặc biệt, họ tranh luận liệu hiệu quả của dự án có báo hiệu một kỷ nguyên mới của toán học hình thức hay phản ánh sức ảnh hưởng đặc biệt của Terence Tao.

Trong bài đăng tổng kết trên kênh thảo luận, Tao nhìn lại việc bản thân không trực tiếp viết nhiều mã. "Điều này thực sự khiến tôi rất phấn khởi, vì nó cho thấy các nhà toán học có thể dẫn dắt những dự án hình thức hóa bằng Lean mà không cần có kỹ năng lập trình Lean chuyên sâu (dù có lẽ họ vẫn cần đủ chuyên môn để phát biểu các bổ đề, nếu chưa thể tự chứng minh chúng)".

Commelin, nhà toán học tại Đại học Utrecht và Giám đốc sáng kiến Mathlib (thư viện toán học lớn được xây dựng cho Lean, chứa sẵn nhiều định nghĩa, định lý và chứng minh để người dùng tái sử dụng), cũng lưu ý thêm rằng dù những dự án như thế này rất thú vị và phấn khích khi tham gia, đóng góp cho chúng lại không phải loại thành tích giúp các nhà toán học trẻ được công nhận khi ứng tuyển vào các vị trí học thuật. "Hiện tại, vẫn chưa rõ cộng đồng toán học sẽ ghi nhận những người làm công việc hình thức hóa chứng minh (tạm gọi như vậy vì chưa có mô tả nghề nghiệp nào phù hợp hơn) ra sao, và những hoạt động này sẽ được đánh giá như thế nào trên thị trường lao động".

Công khai cổ vũ tiềm năng của máy

Đến năm 2024, Tao đã trở thành tiếng nói nổi bật nhất công khai cổ vũ tiềm năng của toán học có máy tính hỗ trợ. Ông đã tham gia Hội đồng Cố vấn Khoa học và Công nghệ của Tổng thống Joe Biden được ba năm và đồng thời trở thành đồng chủ tịch một nhóm công tác về AI tạo sinh. Trong hai bài phát biểu thu hút nhiều sự chú ý năm 2024, ông trình bày tầm nhìn về một hình thức hợp tác toán học mới: kết hợp trực giác của con người, khả năng sáng tạo của các mô hình ngôn ngữ lớn và sự bảo đảm về tính chính xác do các hệ thống máy kiểm chứng mang lại.

Một phần lý do khiến ông hình thành quan điểm này là vì ông nhận thấy rõ giới hạn của các công cụ AI hiện có. Chúng rất giỏi giải quyết những bài toán đơn giản hoặc các nhiệm vụ có nhiều dữ liệu sẵn có. Nhưng ở những lĩnh vực tiên phong, AI lại gặp khó khăn, vì các lĩnh vực này có rất ít kết quả được công bố và ít dữ liệu để huấn luyện. Trong những thử nghiệm ban đầu với các mô hình ngôn ngữ lớn (LLM), ông nhận thấy chúng hành xử giống những sinh viên đại học quá tự tin, liên tục đưa ra đề xuất nhưng không đủ chuyên môn để phân biệt ý tưởng hay với ý tưởng dở.

Dẫu vậy, Tao đã hình dung được một con đường phía trước. Ông không nghĩ AI sẽ sớm thay thế các nhà toán học, nhưng cho rằng nó đặc biệt phù hợp để hỗ trợ giải quyết một số dạng bài toán phức tạp: những bài toán có thể chia thành hàng nghìn bài toán con nhỏ, dễ xử lý, cơ bản đó chính là dạng bài toán phù hợp với dự án Polymath.

Ở quy mô đó, các nhà toán học có thể sử dụng AI để giải quyết phần lớn những bài toán con dễ nhất, với kết quả được xuất ra dưới dạng chứng minh hình thức để Lean kiểm tra, còn bản thân họ sẽ trực tiếp xử lý những câu hỏi khó nhất còn lại.

Trong năm 2024, Tao tích cực truyền bá tầm nhìn ấy đến bất kỳ ai sẵn lòng lắng nghe. Sau dự án ban đầu, ông nhận ra rằng nếu thực sự tin tưởng vào hướng đi này, ông cần chủ động đứng ra dẫn dắt. Trong đầu ông đã có bài toán tiếp theo cần phải giải quyết.

Trước đó, tháng 7/2023, Tao tình cờ đọc được một câu hỏi trên diễn đàn toán học MathOverflow về các quy luật của phép toán, chẳng hạn phép cộng có tính giao hoán (đổi chỗ các số mà kết quả không đổi) và tính kết hợp (thay đổi cách nhóm các số mà kết quả vẫn giữ nguyên).

Câu hỏi nhanh chóng có lời giải, nhưng Tao tò mò về một vấn đề lớn hơn: liệu có thể lập bản đồ cho thấy các quy luật toán học nào kéo theo những quy luật nào khác hay không?

Ông nhận ra rằng, ngay cả khi chỉ xét những đẳng thức mô tả quy luật của một phép toán nhận hai đầu vào và cho ra một kết quả, với tối đa bốn lần thực hiện phép toán ở hai vế, đã có tới 4.694 quy luật khác nhau. Muốn biết quy luật nào có thể suy ra quy luật nào, các nhà nghiên cứu phải kiểm tra hơn 22 triệu khả năng. Đây là bài toán đủ lớn để thử nghiệm một cách làm toán mới: huy động nhiều người cùng làm việc, sử dụng máy tính để kiểm chứng các chứng minh.

Tháng 9/2024, Tao khởi động dự án Equational Theories [4] (Lý thuyết phương trình), hy vọng các công cụ như Lean có thể giúp cộng đồng phối hợp và kiểm chứng hàng triệu mối quan hệ toán học. Mở đầu bài đăng cho dự án, ông liệt kê những lý do chủ yếu khiến các dự án hợp tác toán học công khai quy mô lớn trước đây gặp khó khăn, sau đó ông viết: "Những ngôn ngữ dành cho phần mềm trợ lý chứng minh, chẳng hạn Lean, mang lại một cách thức tiềm năng để vượt qua những trở ngại này".

Cuộc thử nghiệm với máy trên quy mô 22 triệu mối liên hệ trong toán học

Để bắt đầu, Tao và số lượng tình nguyện viên ngày càng đông tham gia cùng ông tiến hành kiểm tra hơn 4.000 quy luật trên những cấu trúc toán học đơn giản gọi là magma. Magma là một dạng cấu trúc đại số được giản lược đến mức tối thiểu, trở thành điểm khởi đầu hữu ích vì bất kỳ quy luật nào không đúng đối với magma đều không thể kéo theo những quy luật khác phức tạp hơn. Những người tham gia nhanh chóng kiểm tra hàng triệu hệ thống đơn giản hóa này bằng các đoạn mã Python đơn giản.

Chỉ trong vài ngày, họ đã giải quyết được hơn 99% trong tổng số 22 triệu hệ quả tiềm năng. Ngay ngày thứ hai của dự án, Tao đăng bài bày tỏ sự kinh ngạc trước tốc độ tiến triển của dự án nhanh và mở rộng quy mô "một cấp độ điên rồ".

Khi những hệ quả đơn giản nhất đã được giải quyết, các tình nguyện viên của Equational Theories đã chuyển sang phương thức phi tập trung, sử dụng các hệ thống chứng minh định lý tự động có khả năng tự mình tìm kiếm lời giải cho các bài toán mà không cần tương tác hướng dẫn. Các hệ thống chứng minh này, kết hợp cùng trí tuệ truyền thống của con người, đã lần lượt giải quyết từng câu hỏi đang còn bỏ ngỏ.

Giống như một nhà khoa học đang ngắm nhìn đứa con tinh thần của mình thành hình, Tao thích thú theo dõi những gì diễn ra. "Dự án dường như đang thành công trong việc phi tập trung hóa; đặc biệt, hiện có rất nhiều hoạt động đang diễn ra mà ngay cả tôi cũng không nắm được đầy đủ", ông viết.

Trong vòng một tháng, dự án Equational Theories đã thu hẹp 22 triệu câu hỏi xuống còn 238. Đến cuối tháng 11, con số chỉ còn 138. Nhưng khi họ tiếp tục giải quyết những trường hợp còn lại, tiến độ bắt đầu chậm lại. Khi năm 2025 bắt đầu, vẫn còn khoảng 30 hệ quả chưa được giải quyết, và tốc độ tiến triển càng chậm hơn nữa. Đến cuối tháng 3, họ đã mắc kẹt suốt nhiều tuần ở đúng bốn trường hợp cuối cùng. Những người đóng góp vẫn thử sức với các bài toán còn lại, nhưng vì chỉ còn rất ít trường hợp chưa được xử lý.

Một cỗ máy làm toán mới

Tuy nhiên, giải quyết trọn vẹn từng hệ quả trong số 22 triệu hệ quả này chưa bao giờ thực sự là mục tiêu của Equational Theories. Quan trọng hơn, Tao xem Equational Theories như một dự án thí điểm cho một phương thức làm toán mới. Và xét trên phương diện đó, dự án đã thành công rực rỡ. Theo Tao, Equational Theories mới chỉ là màn mở đầu cho điều ông hy vọng sẽ trở thành một kỷ nguyên mới của toán học "thực nghiệm" bằng máy tính. Ông hình dung đến một sự chuyển đổi tương tự với toán học giống như những gì đã diễn ra ngành vật lý.

Vật lý từng là một ngành khoa học thuần túy lý thuyết, nơi những nhà tư tưởng đơn độc hoặc các nhóm cộng tác nhỏ giải quyết một hoặc hai bài toán mỗi lần. Cụ thể, vật lý trước đây khá giống với toán học ngày nay. Nhưng cùng với những tiến bộ công nghệ, một nhánh thực nghiệm mới đã xuất hiện, với các dự án hợp tác khổng lồ tại những phòng thí nghiệm như Máy gia tốc hạt lớn (LHC) của CERN, nơi hàng trăm, thậm chí hàng nghìn nhà nghiên cứu có kỹ năng chuyên môn khác nhau cùng làm việc và tạo ra khối lượng dữ liệu khổng lồ. Những thí nghiệm này không thay thế lý thuyết mà bổ sung cho nó, với các kết quả mới liên tục được trao đổi qua lại giữa hai phương thức nghiên cứu.

Tao hình dung toán học cũng sẽ trải qua một quá trình phát triển tương tự. Ông tin rằng những hình thức tìm tòi mới chắc chắn sẽ dẫn đến những hiểu biết mới, như điều vẫn luôn diễn ra trong quá khứ.

Khi nhóm Equational Theories lần lượt đánh dấu những mối quan hệ kéo theo đã được giải quyết trong bảng dữ liệu khổng lồ, họ tình cờ phát hiện ra những cấu trúc toán học thực sự mới. Chẳng hạn "đối đồng điều magma" (magma cohomology), một dạng mở rộng mới của khái niệm đối đồng điều nhóm (group cohomology) - là một nhánh toán học giúp nghiên cứu cấu trúc của các nhóm và những cách có thể xây dựng một nhóm lớn hơn từ các nhóm đã biết, đồng thời vẫn bảo toàn những quy tắc toán học nhất định. Tao liên hệ với John Baez, người từng hoài nghi Equational Theories và cũng là chuyên gia về lý thuyết đối đồng điều, để hỏi liệu cấu trúc này từng được biết đến hay chưa. Baez thừa nhận ông chưa từng gặp nó.

Đó chính xác là điều Tao muốn chứng minh. Dự án cho thấy toán học có thể được thực hiện theo một cách khác, mang tính thực nghiệm và chính nhờ vậy, nó đã tìm ra một điều thực sự mới. Điều ông muốn là chứng minh hiệu quả của một kiểu cỗ máy làm toán mới. Và xét theo khía cạnh đó, cỗ máy đã hoạt động trơn tru.

Terence Tao đã khai phá một con đường làm toán mới, và dường như ông không có ý định quay trở lại con đường cũ nữa.

Việt Anh dịch