Theo truyền thống, toán học là một ngành khoa học đơn độc. Năm 1986, Andrew Wiles đã lui về nghiên cứu độc lập trong bảy năm để chứng minh Định lý (lớn) Fermat. Các kết quả trong chứng minh của ông vẫn khiến một số đồng nghiệp thấy khó hiểu và một số hiện vẫn đang trong vòng tranh cãi. Nhưng trong những năm gần đây ngày càng nhiều những địa hạt của toán học bị chia nhỏ thực sự thành những thành phần cấu tạo riêng lẻ (hình thức) nhờ đó các máy tính có thể kiểm tra và xác nhận các phép chứng minh.

Terrence Tao ở Đại học California, Los Angeles, bị thuyết phục rằng những phương pháp này mở ra những khả năng hợp tác hoàn toàn mới trong toán học. Và nếu những tiến bộ mới nhất trong ngành Trí tuệ nhân tạo được kết hợp vào, thì toán học sẽ thiết lập được những cách làm việc hoàn toàn mới trong những năm tới. Với sự giúp đỡ của máy tính, những vấn đề mở, lớn, sẽ được giải quyết. Tao đã cho biết quan điểm của mình về những gì sắp xảy ra trong một cuộc phỏng vấn với Specktrum der Wissenschaft, ấn phẩm chị em tiếng Đức của Scientific American.

Terrence Tao được trao huy chương Fields năm 2006, được coi là Mozart của toán học

Trong một bài nói chuyện của anh ở Joint Mathematics Meetings tại San Francisco, dường như anh đã ngụ ý rằng các nhà toán học không tin tưởng nhau. Ý anh là gì?

Tôi cho là, chúng tôi có tin tưởng nhau, nhưng phải quen biết nhau cơ. Thật khó để hợp tác với người mà anh chưa từng gặp trừ phi anh có thể kiểm tra từng dòng nghiên cứu của họ. Thường thì số lượng [cộng tác viên] lớn nhất là 5.

Chuyện thay đổi ra sao trước sự xuất hiện của phần mềm kiểm tra chứng minh tự động?

Giờ đây anh có thể thực sự cộng tác với hàng trăm người mà anh chưa từng gặp trước đây. Và anh không cần phải tin tưởng họ, vì họ sẽ tải mã lên và trình biên dịch Lean sẽ kiểm tra nó. Anh có thể nghiên cứu toán học ở quy mô lớn hơn rất nhiều so với bình thường. Khi hình thức hóa những kết quả mới nhất của chúng tôi về cái gọi là giả thuyết đa thức Freiman-Ruzsa (PFR), tôi đã làm việc với hơn 20 người. Chúng tôi đã chia phép chứng minh thành rất nhiều các bước nhỏ và mỗi người đóng góp một phép chứng minh cho mỗi bước nhỏ ấy. Và tôi không cần kiểm tra từng dòng để biết rằng mỗi đóng góp đều đúng. Kiểu như tôi chỉ cần quản lý toàn bộ quá trình và đảm bảo rằng mọi thứ diễn ra theo đúng hướng. Đó là một cách làm toán khác, hiện đại hơn.

Nhà toán học được trao huy chương Fields người Đức, Peter Scholze đã cộng tác trong một dự án Lean – tuy không biết nhiều về máy tính, anh ấy đã kể với tôi như vậy.

Không phải ai cũng cần trở thành một lập trình viên trong những dự án hình thức hóa như vậy. Một số người có thể chỉ cần tập trung vào hướng toán học; anh đang chia nhỏ một nhiệm vụ toán học lớn thành rất nhiều vấn đề nhỏ hơn. Và rồi có những người là chuyên gia trong việc ghép những mảnh nhỏ hơn này thành các chứng minh hình thức. Ta không cần tất cả mọi người trở thành lập trình viên; chỉ cần một số mà thôi. Đó là sự phân công lao động.

Tôi đã nghe về phép chứng minh dựa trên sự hỗ trợ của máy tính 20 năm trước, khi ấy nó còn là một ngành rất lý thuyết. Mọi người nghĩ rằng các anh phải bắt đầu từ điểm khởi đầu – hình thức hóa các tiên đề, sau đó xử lý hình học hay đại số cơ bản – và đi đến toán học cao cấp thì vượt quá sự hình dung của con người. Điều gì đã thay đổi khiến cho toán học hình thức trở nên thực tiễn đến thế?

Một thứ đã thay đổi đó là sự phát triển của các thư viện toán học chuẩn. Nói riêng, Lean có một dự án khổng lồ gọi là mathlib. Tất cả những định lý cơ bản của chương trình toán đại học, như phép tính vi tích phân và tôpô, v.v đã được đưa vào thư viện này, lần lượt. Nên người ta đã nỗi lực để đi từ các tiên đề tới ngưỡng khá cao. Và giấc mơ là thực sự đưa chúng [các thư viện] tới trình độ giáo dục sau đại học. Khi đó sẽ dễ dàng hình thức hóa các ngành mới [của toán học] hơn rất nhiều. Cũng có những cách tìm kiếm tốt hơn để tìm kiếm bởi vì muốn chứng minh thứ gì đó, anh phải có khả năng tìm kiếm những thứ đã được xác nhận là đúng. Thế nên sự phát triển của những công cụ tìm kiếm thực sự thông minh thì cũng là một phát triển lớn mới mẻ.

Vậy đây không phải là một câu hỏi về sức mạnh tính toán?

Không, một khi đã hình thức hóa toàn bộ dự án PFR, chỉ cần mất nửa giờ biên dịch rồi kiểm chứng. Đó không phải là nút cổ chai – vấn đề nằm ở chỗ làm sao cho người ta sử dụng nó, tính khả dụng, tính thân thiện với người dùng. Hiện nay có một cộng đồng hàng nghìn người và có một diễn đàn trực tuyến sôi nổi để thảo luận về cách giúp cho ngôn ngữ này hiệu quả hơn.

Lean có phải là tiến bộ mới nhất, hay còn có các hệ thống cạnh tranh khác?

Lean có lẽ là cộng đồng tích cực nhất. Với các dự án chỉ có một tác giả, có thể có các ngôn ngữ khác tốt hơn đôi chút, nhưng nhìn chung Lean vẫn dễ tiếp cận hơn. Và nó có một thư viện và cộng đồng rất tốt. Có thể trong tương lai sẽ có một giải pháp thay thế khác cho nó, nhưng hiện nay nó là ngôn ngữ hình thức vượt trội nhất.

Khi anh nói chuyện về một dự án toán học khác, ai đó đã hỏi liệu anh có muốn hình thức nó, và về cơ bản anh đáp rằng thế thì mất thời gian lắm.

Tôi có thể hình thức hóa nó, nhưng sẽ mất một tháng của tôi mất. Giờ thì tôi nghĩ ta vẫn chưa đến mức thường xuyên hình thức hóa mọi thứ. Anh phải lựa ra và chọn. Anh chỉ muốn hình thức hóa những thứ thực sự cần thiết với mình, ví như dạy anh làm việc với Lean, hay nếu người khác thực sự quan tâm đến việc kết quả này đúng hay không. Nhưng công nghệ này đang trở nên tốt hơn. Nên tôi nghĩ điều khôn ngoan nên làm trong nhiều trường hợp chỉ là đợi đến khi mọi việc dễ dàng hơn. Thay vì mất thời gian gấp 10 lần để hình thức hóa một thứ, thì chỉ mất gấp đôi thời gian thông thường.

Thậm chí anh đã nói về việc giảm hệ số đó xuống nhỏ hơn 1.

Với AI, thực sự có tiềm năng để làm việc đó. Tôi nghĩ trong tương lai thay vì mất thời gian viết lại chứng minh, ta sẽ giải thích chúng cho một GPT nào đó. Và GPT này sẽ thử hình thức nó trong Lean cùng anh. Nếu mọi chuyện đều ổn, GPT [cơ bản] sẽ nói, “Đây là bài báo của bạn ở dạng LaTex; chứng minh Lean thì đây. Nếu bạn muốn, tôi có thể nhấn nút này và gửi nó cho một tạp chí giúp bạn.” Đây có thể là một trợ lý tuyệt với trong tương lai.

Cho đến nay, ý tưởng chứng minh vẫn phải xuất phát từ nhà toán học, phải không?

Đúng vậy, cách nhanh nhất để hình thức hóa là trước tiên, tìm một phép chứng minh của con người. Con người đưa ra các ý tưởng, bản nháp đầu tiên cho phép chứng minh. Sau đó anh chuyển nó thành một chứng minh hình thức. Trong tương lai, có thể chuyện sẽ tiến triển khác đi. Có thể có những dự án hợp tác mà ta không biết làm thế nào để chứng minh toàn bộ vấn đề. Nhưng người ta có những ý tưởng về cách chứng minh những phần nhỏ, và họ hình thức hóa chúng rồi cố gắng ghép chúng lại với nhau. Trong tương lai, tôi có thể hình dung một định lý lớn được chứng minh nhờ sự kết hợp của 20 người và một nhóm AI, mỗi tổ hợp lại chứng minh những phần nhỏ. Và theo thời gian, chúng được kết nối lại với nhau, và anh có thể tạo ra một thứ hay ho nào đó. Chuyện đó thật tuyệt. Sẽ mất thêm nhiều năm nữa trước khi điều đó thành hiện thực. Công nghệ hiện tại vẫn chưa đạt đến mức đó, một phần vì việc hình thức hoá hiện vẫn rất khó khăn.

Tôi đã nói chuyện với những người cố gắng sử dụng các mô hình ngôn ngữ lớn hoặc các công nghệ máy học tương tự để tạo ra những chứng minh mới. Tony Wu và Christian Szegedy, những người gần đây đồng sáng lập công ty xAI cùng với Elon Musk và cộng sự, đã nói với tôi rằng trong vòng hai đến ba năm, toán học sẽ được “giải quyết” theo cách tương tự như cờ vua đã được giải quyết – rằng các cỗ máy sẽ giỏi hơn bất cứ con người nào trong việc tìm ra lời giải.

Tôi nghĩ rằng trong ba năm tới, AI sẽ trở nên hữu ích cho các nhà toán học. Nó sẽ là một bạn đồng hành tuyệt vời. Anh đang cố gắng chứng minh một định lý, và có một bước mà anh nghĩ là đúng, nhưng anh không hoàn toàn hiểu vì sao lại thế. Và anh có thể bảo, “AI, mày có thể làm việc này cho tao không?” Rồi nó có thể đáp, “Tôi nghĩ tôi có thể chứng minh đấy." Tôi không nghĩ rằng toán học sẽ hoàn toàn được giải quyết. Nếu có một đột phá lớn khác trong AI thì chuyện ấy có thể khả dĩ, nhưng tôi nghĩ rằng trong 3 năm tới anh sẽ sẽ thấy có tiến bộ đáng kể, và việc thực sự sử dụng AI sẽ ngày càng dễ quản lý hơn. Ngay cả khi AI có thể làm thứ toán học mà chúng ta đang làm bây giờ, thì cũng có nghĩa là ta sẽ chuyển sang một kiểu toán học cao cấp hơn. Nên hiện tại, chẳng hạn, ta chứng minh từng kết quả một. Giống như các nghệ nhân thủ công làm một con búp bê gỗ hay gì đó. Anh lấy một con búp bê và rất cẩn thận sơn mọi thứ, và rồi anh làm con khác. Cách chúng ta làm toán chưa thay đổi nhiều đến thế. Nhưng ở trong tất cả những lĩnh vực khác, chúng ta đã có sản xuất hàng loạt. Và với AI, ta có thể bắt đầu chứng minh hàng trăm hoặc hàng nghìn định lý cùng một lúc. Các nhà toán học con người sẽ chỉ đạo AI làm các việc khác nhau. Vì vậy, tôi nghĩ rằng cách ta làm toán sẽ thay đổi, nhưng khoảng thời gian mà họ đề xuất có lẽ hơi quá đà.

Tôi đã phỏng vấn Peter Scholze khi cậu ấy giành Huy chương Fields vào năm 2018. Tôi đã hỏi cậu ấy, có bao nhiêu người hiểu những gì cậu đang làm? Và cậu ấy nói rằng có khoảng 10 người.

Với những dự án hình thức hóa, cái chúng tôi nhận thấy là bạn có thể hợp tác với những người không hiểu toàn bộ mà chỉ hiểu một phần nhỏ toán học của toàn bộ dự án. Giống như bất cứ thiết bị hiện đại nào vậy. Không một người đơn lẻ nào có thể tự dựng được một chiếc máy tính, khai thác quặng kim loại và tinh luyện chúng, rồi tạo ra các phần cứng và phần mềm. Chúng ta có tất cả các chuyên gia như vậy, có những chuỗi cung ứng hậu cần lớn, rồi cuối cùng ta có thể tạo ra một chiếc điện thoại thông minh hay bất cứ thứ gì. Hiện tại, trong một mối hợp tác toán học, mọi người phải biết hầu hết trọn vẹn vấn đề, và đó là một trở ngại, như Scholze đã đề cập. Nhưng với các dự án hình thức thức hóa này, người ta có thể phân chia công việc và đóng góp vào một dự án mà chỉ cần biết một phần của nó. Tôi cũng nghĩ rằng chúng ta nên bắt đầu hình thức hóa các sách giáo khoa. Nếu một cuốn sách giáo khoa được hình thức hóa, anh có thể tạo ra những cuốn sách giáo khoa tương tác, nơi anh có thể mô tả chứng minh của một kết quả một cách rất tổng quát, giả định nhiều kiến thức. Nhưng nếu có các bước không hiểu, anh có thể mở rộng chúng và đi vào chi tiết – tới tận các tiên đề nếu muốn. Không ai làm như vậy ngay bây giờ cho sách giáo khoa vì vẫn cần rất nhiều công sức. Nhưng nếu đã hình thức hóa xong thì máy tính có thể tạo ra những cuốn sách giáo khoa tương tác này cho anh. Nó sẽ giúp một nhà toán học trong một lĩnh vực có thể bắt đầu đóng góp vào một lĩnh vực khác vì anh có thể xác định chính xác các công việc nhỏ của một nhiệm vụ lớn mà không cần phải hiểu mọi thứ.

Một chứng minh toán học không chỉ là việc kiểm tra cái gì đó là đúng. Một chứng minh cũng là để hiểu một điều gì đó, đúng không? Có những chứng minh đẹp và có những chứng minh xấu xí rất kỹ thuật. Một chứng minh tốt giúp anh hiểu vấn đề sâu hơn. Vậy, nếu giao việc đó cho máy móc, chúng ta có thể vẫn hiểu được những gì chúng đã tìm ra không?

Những gì các nhà toán học đang làm là khám phá không gian của những gì là đúng và những gì là sai và tại sao mọi thứ là đúng. Và chúng ta làm việc đó thông qua các chứng minh. Mọi người đều biết rằng khi điều gì đó là đúng thì ta phải cố gắng chứng minh hoặc bác bỏ nó. Và chuyện đó mất rất nhiều thời gian. Nó tẻ nhạt. Nhưng trong tương lai, có thể ta chỉ cần hỏi một AI, “Kết quả này có đúng hay không?” Rồi chúng ta có thể khám phá không gian kia hiệu quả hơn nhiều, và có thể cố gắng tập trung vào những gì chúng ta thực sự quan tâm. AI sẽ giúp ta rất nhiều bằng cách tăng tốc quá trình này. Chúng ta sẽ vẫn là người dẫn dắt, ít nhất là bây giờ. Có thể trong 50 năm nữa mọi thứ sẽ khác. Nhưng trong tương lai gần, AI sẽ tự động hóa những thứ nhàm chán, tầm thường trước tiên.

AI sẽ giúp chúng ta giải quyết những vấn đề lớn, chưa có lời giải trong toán học chứ?

Nếu muốn chứng minh một giả thuyết chưa có lời giải, một trong những điều đầu tiên anh cần làm là chia nó thành các phần nhỏ hơn, mà cơ hội chứng minh được mỗi phần lớn hơn. Nhưng người ta thường chia một vấn đề thành những vấn đề khó hơn. Rất dễ để biến một vấn đề trở nên khó hơn thay vì đơn giản hơn. Và về mặt này thì AI chưa thể hiện được khả năng tốt hơn con người.

Quá trình phân tích và khám phá vấn đề cũng giúp anh học được nhiều điều mới mẻ. Ví dụ, Định lý cuối cùng của Fermat là một giả thuyết đơn giản về các số tự nhiên, nhưng toán học được phát triển để chứng minh nó không nhất thiết phải liên quan đến các số tự nhiên nữa. Vì vậy, giải quyết một bài toán chứng minh thì ý nghĩa hơn nhiều việc chứng minh chỉ một trường hợp.

Giả sử AI đưa ra một chứng minh khó hiểu và phức tạp. Sau đó, anh có thể nghiên cứu và phân tích nó. Chẳng hạn, chứng minh này sử dụng 10 giả thiết để đi đến một kết luận - nếu tôi xóa một giả thiết, chứng minh này còn đúng hay không? Đó là một ngành khoa học hiện vẫn chưa tồn tại vì chúng ta vẫn chưa có quá nhiều chứng minh do AI tạo ra, nhưng tôi nghĩ sẽ có một kiểu nhà toán học mới, những người có thể tiếp nhận toán học do AI tạo ra và giúp chúng trở nên dễ hiểu hơn. Giống như chúng ta có khoa học thực nghiệm và lý thuyết vậy. Có rất nhiều thứ chúng ta khám phá ra nhờ thực nghiệm, sau đó chúng ta làm thêm nhiều thí nghiệm và khám phá ra các định luật của tự nhiên. Hiện tại, chúng ta chưa làm vậy trong toán học. Nhưng tôi nghĩ sẽ có một ngành công nghiệp gồm những người cố gắng trích xuất thông tin ý nghĩa từ các chứng minh do AI tạo ra mà ban đầu không có mấy ý nghĩa.

Vậy thay vì là kết thúc thì đây có phải một tương lai tươi sáng cho toán học?

Tôi nghĩ sẽ có những cách làm toán khác nhau mà hiện tại chưa tồn tại. Tôi có thể thấy những nhà toán học quản lý dự án có thể tổ chức các dự án rất phức tạp – họ không hiểu tất cả toán học, nhưng họ có thể chia nhỏ mọi thứ thành các phần nhỏ hơn và phân công chúng cho người khác, và họ có kỹ năng giao tiếp tốt. Sau đó, có những chuyên gia làm việc trong các lĩnh vực con. Có những người giỏi huấn luyện AI trong các loại toán học cụ thể, và sau đó có những người có thể chuyển đổi các chứng minh của AI thành thứ gì đó mà con người có thể đọc được. Chuyện sẽ trở nên rất giống với cách hoạt động của hầu hết các ngành công nghiệp hiện đại khác. Chẳng hạn như trong báo chí, không phải ai cũng có cùng bộ kỹ năng. Bạn có biên tập viên, bạn có nhà báo, và bạn có doanh nhân, v.v. – cuối cùng chúng ta sẽ có những thứ tương tự trong toán học.

Toán học chúng ta làm là loại toán học phù hợp với bộ não của chúng ta, đúng không? Và nếu đến một lúc nào đó AI thông minh hơn rất nhiều, nó có thể đi vào những vùng mà chúng ta khó có thể hiểu được.

Toán học vốn đã lớn hơn bất cứ bộ óc con người nào. Các nhà toán học thường xuyên dựa vào các kết quả mà những người khác đã chứng minh. Họ biết đại khái tại sao nó đúng, họ có một số trực giác, nhưng họ không thể chia nó ra tất cả các chi tiết đến các tiên đề. Nhưng họ biết nơi để tìm, hoặc có thể họ biết ai đó có thể làm điều đó. Chúng ta đã có rất nhiều định lý chỉ được kiểm chứng bởi máy tính, trong đó một số tính toán lớn trên máy tính đã kiểm tra hàng triệu trường hợp. Anh có thể xác minh nó bằng tay, nhưng không ai có thời gian để làm điều đó, và không đáng để làm như vậy. Vì vậy, tôi nghĩ chúng ta sẽ thích nghi. Không cần thiết để một người kiểm tra mọi thứ. Để máy tính làm việc kiểm tra cho chúng ta, với tôi, cũng ổn.

Ở tiền tuyến của toán học, có rất nhiều thứ đang diễn ra kéo mọi thứ lại với nhau từ các lĩnh vực dường như không liên quan, và theo hiểu biết ngây thơ của tôi, một AI biết tất cả các lĩnh vực này có thể cho bạn một gợi ý và nói, "Tại sao bạn không nhìn vào đó? Nơi đó có thể giúp bạn giải quyết vấn đề của mình."

Tạo ra các kết nối hoặc ít nhất chỉ ra các kết nối có thể có quả là một tiềm năng rất thú vị của AI. Hiện tại, nó có tỷ lệ thành công rất thấp. Nó có thể cho bạn 10 gợi ý mà trong đó có 1 gợi ý thú vị và 9 gợi ý là rác. Thực tế là nó gần như tệ hơn cả ngẫu nhiên. Nhưng điều này có thể thay đổi trong tương lai.

Những vấn đề gì đang cản trở việc huấn luyện một AI toán học?

Một phần của vấn đề là không có đủ dữ liệu để huấn luyện nó. Anh có thể huấn luyện nó bằng các bài báo đã công bố trực tuyến. Nhưng tôi nghĩ rất nhiều trực giác không được nắm bắt trong các bài báo in trên các tạp chí mà nằm trong các cuộc trò chuyện với các nhà toán học, trong các bài giảng và trong cách chúng tôi hướng dẫn sinh viên. Đôi khi tôi đùa rằng điều chúng ta cần làm là để GPT tham gia một khóa học sau đại học tiêu chuẩn, ngồi trong các lớp học, đặt câu hỏi như một sinh viên và học như con người học toán.

Phiên bản đã công bố của một chứng minh luôn được cô đọng. Và ngay cả khi anh lấy tất cả toán học đã được công bố trong lịch sử loài người, thì nó vẫn nhỏ so với những gì các mô hình này được huấn luyện.

Và mọi người chỉ công bố những câu chuyện thành công. Dữ liệu thực sự quý giá là khi một người thử nghiệm một cái gì đó, và nó không hoàn toàn hoạt động, nhưng họ biết cách sửa nó. Nhưng họ chỉ công bố những thứ thành công, không phải là quá trình.

Có thể anh nên đăng ký những nỗ lực chứng minh điều gì đó, giống như trong các nghiên cứu y tế. Các nhà nghiên cứu sẽ đăng ký nó, và sau đó họ sẽ phải công bố nó ngay cả khi nó không thành công.

Chúng tôi không có văn hóa đó. Có thể trong tương lai hình thức hóa sẽ trở nên rất hiệu quả và anh có thể hình thức hóa nhiều thứ theo thời gian thực. Và có thể nếu anh muốn sử dụng một AI Lean giả tưởng nào đó của năm 2040 trong một dự án nghiên cứu và muốn được tài trợ để sử dụng AI giả tưởng này, anh sẽ phải chấp nhận rằng quá trình thử nghiệm và thất bại của anh sẽ được lưu lại. Và sau đó người ta sẽ sử dụng nó để huấn luyện các AI tương lai. Hoặc có thể một nhóm khác đang làm việc với một vấn đề tương tự và họ có thể thấy, “ồ nhóm này đang thử cùng vấn đề này và đã thất bại”, nên anh không phải mất thời gian lặp lại đúng những sai lầm ấy.

Các nhà toán học có đang lãng phí nhiều thời gian không?

Ồ, rất nhiều. Vì lý do nào đó mà rất nhiều kiến thức bị mắc kẹt trong đầu của mỗi nhà toán học. Và chỉ một phần nhỏ được làm rõ ràng. Nhưng càng hình thức hóa, càng có nhiều kiến thức ẩn của chúng ta trở nên hiển hiện. Vì vậy, sẽ có những lợi ích bất ngờ từ điều đó.

Nguồn: Scientific American, bản dịch đã đăng một phần trên tạp chí Tia Sáng. Bản quyền bản dịch trọn vẹn thuộc Tomoblog.