Bộ kiểm tra chứng minh và AI đồng hành toán học dưới góc nhìn của Terence Tao
(scientificamerican.com)- Khi các chứng minh toán học ngày càng được hình thức hóa chặt chẽ hơn, những công cụ như Lean đang thay đổi cách xác minh chứng minh của con người và nền tảng niềm tin cho các cộng tác quy mô lớn
- Khi các thư viện chuẩn như mathlib được tích lũy, rào cản để hình thức hóa từ các định lý bậc cử nhân đến những lĩnh vực mới đang dần thấp hơn
- Trong quá trình hình thức hóa giả thuyết PFR, hơn 20 người đã tham gia và chia nhau phụ trách các bước chứng minh nhỏ; Terence Tao tập trung quản lý định hướng tổng thể thay vì rà từng dòng
- AI hiện gần với vai trò copilot cho chứng minh hơn là ngay lập tức “giải quyết” toán học, bằng cách hỗ trợ hình thức hóa, kiểm chứng và các công việc lặp lại
- Nghiên cứu toán học có thể chuyển thành những công việc tường minh và phân chia hơn, như con người định hướng, chi tiết hóa hình thức, huấn luyện AI và diễn giải các chứng minh do AI tạo ra
Hình thức hóa đang thay đổi cộng tác trong toán học
- Nghiên cứu toán học truyền thống gần với mô hình cộng tác ít người, và Tao cho rằng thông thường khoảng 5 người đã gần với giới hạn trên của quy mô hợp tác
- Nếu có bộ kiểm tra chứng minh tự động (proof checker), có thể cộng tác với hàng trăm người không quen biết nhau
- Người đóng góp tải mã lên, và Lean compiler sẽ xác minh
- Không cần chỉ dựa vào quan hệ cá nhân để tạo niềm tin, mà có thể kiểm tra bằng kết quả xác minh hình thức
- Khi hình thức hóa kết quả gần đây về giả thuyết Polynomial Freiman-Ruzsa (PFR), đã có hơn 20 người tham gia
- Chứng minh được chia thành nhiều bước nhỏ
- Mỗi người tham gia phụ trách chứng minh một bước
- Tao quản lý hướng tiến triển tổng thể thay vì kiểm tra từng dòng của mọi đóng góp
Không phải mọi nhà toán học đều cần là lập trình viên
- Trong các dự án hình thức hóa, có thể phân chia vai trò
- Có người tập trung vào định hướng toán học
- Có người chuyên chuyển các mảnh toán học nhỏ thành chứng minh hình thức
- Những nhà toán học không quen với máy tính như Peter Scholze vẫn có thể tham gia dự án Lean
- Nếu chia một bài toán lớn thành các mảnh nhỏ, người tham gia có thể đóng góp cho các tác vụ con cụ thể mà không cần hiểu toàn bộ lý thuyết
Lean, mathlib và tìm kiếm tạo ra tính thực dụng
- Một trong những lý do lớn khiến toán học hình thức trở nên thực dụng là sự phát triển của các thư viện toán học chuẩn
- Lean có một dự án quy mô lớn tên là mathlib
- Các định lý nền tảng của toán bậc cử nhân như giải tích và tô-pô đang dần được đưa vào thư viện
- Mục tiêu là nâng thư viện lên đến trình độ sau đại học
- Khi đó sẽ dễ hình thức hóa các lĩnh vực toán học mới hơn
- Để xây dựng chứng minh, cần tìm các định lý đã được xác nhận là đúng, nên công cụ tìm kiếm thông minh hơn cũng trở nên quan trọng
- Sau khi hình thức hóa toàn bộ dự án PFR, việc biên dịch để xác minh chỉ mất khoảng 30 phút
- Nút thắt không nằm ở sức mạnh tính toán mà ở tính tiện dụng, mức độ thân thiện với người dùng và khả năng thích nghi của con người với công cụ
- Lean hiện được xem là ngôn ngữ hình thức có cộng đồng năng động nhất
- Với dự án tác giả đơn lẻ, các ngôn ngữ khác có thể phù hợp hơn
- Lean dễ học, có thư viện và cộng đồng tốt
- Về sau có thể bị thay thế bởi lựa chọn khác, nhưng hiện tại là ngôn ngữ hình thức chiếm ưu thế
Chi phí hình thức hóa vẫn còn cao
- Tao cho rằng ông có thể hình thức hóa một số dự án, nhưng hiện tại có thể phải dành một tháng thời gian của mình
- Đây vẫn chưa phải giai đoạn để mọi kết quả đều được hình thức hóa một cách thường nhật
- Những trường hợp việc học Lean mang lại ích lợi
- Những trường hợp có mức quan tâm cao đến độ chính xác của kết quả
- Cần chọn những dự án mà hình thức hóa đem lại giá trị thực sự
- Khi công nghệ tiến bộ, chi phí hình thức hóa có thể giảm
- Hiện tại có thể mất thời gian gấp 10 lần cách làm cũ
- Về sau có thể giảm xuống khoảng 2 lần, rồi thấp hơn cả 1 lần
AI có thể trở thành copilot của nhà toán học
- Tao hình dung rằng trong tương lai, thay vì tự gõ trực tiếp chứng minh, nhà toán học có thể mô tả cho một hệ thống như GPT, và AI sẽ thử hình thức hóa bằng Lean ngay trong quá trình làm việc
- Nếu việc xác minh thành công, có thể cung cấp đồng thời bài báo LaTeX và chứng minh Lean
- Nếu người dùng muốn, nó thậm chí có thể là trợ lý giúp nộp bài cho journal
- Hiện tại, con đường hình thức hóa nhanh nhất vẫn là để con người tạo ra ý tưởng và bản nháp chứng minh trước
- Về dài hạn, cũng có thể có những dự án mà con người không nắm toàn bộ chứng minh, chỉ hình thức hóa các mảnh nhỏ rồi cùng AI ghép lại để chứng minh một định lý lớn
- Tao cho rằng phải mất nhiều năm thì cách làm này mới khả thi
- Công nghệ hiện nay vẫn chưa đủ, và việc hình thức hóa vẫn còn rất vất vả
Khoảng cách với viễn cảnh “toán học được giải quyết”
- Tony Wu và Christian Szegedy từng nói rằng trong 2–3 năm tới, toán học sẽ được “giải quyết”, theo nghĩa máy móc sẽ tìm chứng minh tốt hơn con người
- Tao cho rằng trong vòng 3 năm, AI có thể trở nên hữu ích cho nhà toán học và tạo ra tiến bộ rõ rệt, nhưng không có nghĩa toán học sẽ được giải quyết
- AI có thể trở thành một copilot để nhờ hỗ trợ khi một bước trong chứng minh có vẻ đúng nhưng con người chưa nhìn ra ngay
- Ngay cả khi AI có thể làm toán ở trình độ hiện tại của con người, các nhà toán học vẫn có thể chuyển sang những tầng mức toán học cao hơn
- AI cũng có thể mở ra cách chứng minh hàng trăm hay hàng nghìn định lý cùng lúc
- Khi đó con người sẽ đảm nhiệm vai trò chỉ huy AI nên làm gì
- Tao cho rằng mốc thời gian 2–3 năm cho sự thay đổi này là hơi quá tham vọng
Hiểu chứng minh và các chứng minh do AI tạo ra
- Chứng minh toán học không chỉ là quy trình xác nhận điều gì đó là đúng, mà còn là quá trình hiểu vì sao nó đúng
- Trong tương lai gần, nhiều khả năng AI sẽ tự động hóa trước các công việc nhàm chán và vụn vặt, còn con người vẫn giữ vai trò định hướng
- Nếu AI đưa ra một chứng minh khó hiểu và xấu xí, con người vẫn có thể phân tích lại chứng minh đó
- Ví dụ, trong một chứng minh suy ra kết luận từ 10 giả thiết, có thể kiểm tra xem bỏ đi một giả thiết thì kết luận còn đúng không
- Có thể sẽ xuất hiện một kiểu nhà toán học mới chuyên rút ra insight từ các chứng minh do AI tạo ra
- Những chứng minh AI ban đầu có thể trông như không có insight
- Con người có thể làm cho chúng dễ hiểu hơn và tìm ra cấu trúc bên trong
Những bài toán chưa giải và giới hạn của AI
- Để chứng minh một giả thuyết chưa được giải, trước tiên cần chia nó thành các mảnh nhỏ hơn
- Việc biến một bài toán thành bài toán khó hơn dễ hơn rất nhiều so với biến nó thành bài toán dễ hơn
- Tao cho rằng AI vẫn chưa cho thấy nó giỏi hơn con người trong việc phân rã như vậy
- Việc dùng AI để gợi ý các khả năng kết nối giữa nhiều lĩnh vực là hướng đi thú vị
- Hiện tỷ lệ thành công còn thấp
- Trong 10 gợi ý có thể chỉ 1 cái thú vị và 9 cái vô dụng
- Tao cho rằng tương lai phần này có thể thay đổi
Bài toán dữ liệu của tri thức toán học
- Một trong những vấn đề khi huấn luyện AI cho toán học là không có đủ dữ liệu
- Các bài báo trực tuyến có thể dùng để huấn luyện, nhưng nhiều trực giác toán học lại không xuất hiện trong bài báo
- Các cuộc trò chuyện giữa các nhà toán học
- Các bài giảng
- Cách hướng dẫn sinh viên
- Những lần thử thất bại và quá trình chỉnh sửa
- Các chứng minh được xuất bản là sản phẩm đã được nén lại, và con người có xu hướng chỉ công bố các ca thành công
- Dữ liệu thực sự quý giá là quá trình thử một điều gì đó không hiệu quả, rồi sửa nó như thế nào
- Trong tương lai, quá trình thử nghiệm và thất bại trong nghiên cứu có thể được ghi lại để dùng cho huấn luyện AI hoặc giúp các nhà nghiên cứu khác tránh lặp lại cùng một thất bại
- Tao nêu ví dụ về việc đồng ý ghi lại quá trình nghiên cứu để dùng một hệ thống kiểu AI Lean tiên tiến của năm 2040
Sự chuyển dịch sang toán học tường minh hơn
- Rất nhiều tri thức toán học hiện bị giữ trong đầu từng nhà toán học riêng lẻ, và chỉ một phần rất nhỏ được ghi lại một cách tường minh
- Càng nhiều hình thức hóa, càng nhiều tri thức ngầm được chuyển thành tri thức tường minh
- Giáo trình được hình thức hóa có thể dẫn đến giáo trình tương tác
- Bắt đầu từ phần giải thích chứng minh ở mức cao
- Nếu có bước nào chưa hiểu, có thể mở rộng ra chi tiết hơn
- Nếu muốn, thậm chí có thể đi xuống đến mức tiên đề
- Cách làm này có thể giúp nhà toán học ở một lĩnh vực đóng góp dễ hơn cho lĩnh vực khác
- Có thể chỉ định chính xác các tác vụ con của một bài toán lớn
- Không cần hiểu toàn bộ vẫn có thể tham gia vào mảnh cần thiết
1 bình luận
Ý kiến trên Hacker News
https://archive.is/Idouw
Cụm từ project manager mathematicians gợi nhớ đến bài châm biếm “A letter to my old friend Jonathan” [1] mà Edsger Dijkstra viết năm 1975 và bài tiếp theo [2]
Đó là bài viết phê phán bằng cách cho thấy sẽ nực cười thế nào nếu cách làm phần mềm được áp dụng vào toán học, nhưng ở một vài khía cạnh lại khá có tính tiên đoán
Trọng tâm là phê phán sự phi lý khi áp dụng quyền sở hữu trí tuệ, đặc biệt là với chân lý toán học, và may mắn là trong làn sóng cơ giới hóa hiện nay thì phần đó dường như không phải mối lo lớn
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
Đây là bài viết có nhiều góc nhìn sắc sảo, nhưng theo tôi phần còn thiếu là việc LLM đang ngày càng trừu tượng hóa theo cách siêu nhân
Tao nói rằng “biến vấn đề thành khó hơn thì dễ nhưng biến thành đơn giản hơn thì khó, và AI chưa từng cho thấy nó giỏi hơn con người ở điểm này”, nhưng với cách LLM vận hành thì hoàn toàn có thể xuất hiện mức độ thấu hiểu cao hơn nhiều
Hiện tại chúng giống trợ lý, bộ kiểm chứng sự thật, công cụ xử lý việc nhàm chán hơn, nhưng sớm muộn sẽ trở thành thứ có thể đề xuất insight. Ngay từ bây giờ LLM đã tạo embedding và nén tri thức, nên có thể sở hữu những insight mà chúng ta không nhìn ra
Cảnh Hinton lấy ví dụ về mối liên hệ giữa bom hạt nhân và đống ủ phân: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
Nó chỉ là cỗ máy được huấn luyện để bắt chước cách con người viết, và không có dữ liệu huấn luyện cần thiết để bắt chước thứ gì đó thông minh hơn con người
Tôi không nghi ngờ việc machine learning sẽ vượt qua trí thông minh con người, nhưng nút thắt là tìm ra cách để nó tự học từ chính đầu ra của mình mà không cần con người can thiệp, thay vì hồi quy trên toàn bộ kho chữ viết của thế giới
Ramanujan dù không được giáo dục chính quy và chỉ tiếp xúc với vài cuốn sách toán vẫn có những khám phá toán học rực rỡ; xét từ góc độ dữ liệu huấn luyện của mô hình machine learning thì lượng đó gần như chẳng là gì
Mất khoảng 10 giây để diễn đạt bằng lời, nhưng nếu đã biết thông tin cần thiết thì đáp án là quá rõ ràng
Hinton cho rằng điều này cho thấy tư duy loại suy, nhưng có rất nhiều bài viết trực tuyến về làm vườn và vật lý của đống ủ phân, nên khả năng cao ChatGPT đã thấy từ lúc huấn luyện rồi
Vì vậy ví dụ này trông giống một trường hợp không kiểm soát được việc LLM về cơ bản đã nhìn thấy sẵn câu trả lời trong văn bản huấn luyện
Đoạn sau trong video khi Ilya nói “đã có một chứng minh tồn tại rồi. Bộ não con người là một mạng nơ-ron” (https://youtu.be/Gg-w_n9NJIE?t=4966) cũng khá thú vị. Tôi nhìn chung đồng ý với quan điểm rằng não người cũng là mạng nơ-ron, nhưng cũng có nhiều phản biện rằng nơ-ron thực không hoạt động theo 8 bit, rồi còn khác biệt về loại tế bào, DNA, môi trường hóa học hormone, v.v., nên đây có vẻ là một ngã rẽ mang tính triết học
Việc đó có thể xong trong vài phút đến vài giờ
Trong khi đó, để có thêm một chuyên gia con người thì phải có ai đó thật sự thích toán như một nghề, trải qua hàng chục năm giáo dục và chuyên môn hóa cao độ, mà cũng chẳng có gì đảm bảo người đó sẽ đi đến cùng và đạt mức đủ sức đẩy tiền tuyến tri thức tiến lên
Trong lúc chờ quãng thời gian đó trôi qua, ta có thể tạo ra hàng nghìn tỷ chuyên gia AI chạy song song
Băng thông để não người hấp thụ thông tin mới là thấp, nhưng máy móc có thể sao chép tri thức cả đời chỉ trong vài giây, thực hiện hàng nghìn cuộc hội thoại song song, và thậm chí tuần tự hóa một phần của bộ não để gửi sang AI khác. Nếu đạt tới vật chất có thể lập trình thì còn có thể tạo computronium theo cấp số nhân, mở ra kiểu omega point nơi hàng nghìn năm nghiên cứu được thực hiện chỉ trong vài giây
Tôi hoàn toàn không biết toán, nhưng điều này gợi tôi nhớ đến lịch sử phần mềm. Trước đây, những dự án đáng kinh ngạc như RollerCoaster Tycoon hầu như là tác phẩm do gần như một người làm ra
Sau đó, kỹ nghệ phần mềm được mô-đun hóa theo cách khá giống như mô tả trong bài phỏng vấn, và giờ nó đã trở thành một dây chuyền lắp ráp khổng lồ nơi những người như tôi sản xuất React để kiếm sống, còn năng suất trên đầu người hay mức kỹ năng yêu cầu dường như gần như bằng 0
Tôi có cảm giác rằng khi một lĩnh vực ở thời kỳ đỉnh cao, một thiên tài có thể chứa cả trăm thứ trong đầu và làm ra công trình tốt nhất; còn khi thứ đó bị thay bằng dây chuyền lắp ráp, lĩnh vực ấy không còn tạo ra được những thứ thực sự có giá trị nữa
Kỹ nghệ phần mềm không hề ngừng tạo ra những thứ tuyệt vời, mà tôi nghĩ là hoàn toàn ngược lại
Bỏ chuyện đùa sang một bên, đến lúc nào đó khi phải sửa một bug nghiêm trọng thì năng lực thật sẽ lộ ra. Chỉ vì sản phẩm hay dịch vụ đã ổn định và có lợi nhuận không có nghĩa là các nhà phát triển ban đầu đã rời đi, hay không còn ai có thể làm được việc lớn
Nói rằng lĩnh vực này không còn tạo ra những thứ thực sự có giá trị nữa là sai nghiêm trọng
Cảm giác như đang so một nhà thờ lớn do 100 người xây trong 100 năm với một túp lều do một người dựng trong một tháng. Túp lều cũng đứng vững và cho ta chỗ ở, nhưng không phải là nhà thờ lớn
Bên web development thì chỉ riêng muốn nhìn vào Python thôi cũng đã có quá nhiều framework và công nghệ cho từng bánh răng nhỏ trong guồng máy, đến mức thực sự khó mà theo kịp
Năng lực nhìn chung tuân theo phân phối log-normal, nên người xuất chúng vốn dĩ rất ít; và ở các lĩnh vực nhỏ thời kỳ đầu, do hạ tầng hỗ trợ còn thiếu, chỉ những người có tài năng cực cao mới sống sót được, khiến mật độ nhân tài top đầu có thể cao một cách phi thực tế
Việc cố gượng ghép 47 framework mới nhất để xuất xưởng một ứng dụng danh sách việc cần làm và việc tạo ra tác động có ý nghĩa về bản chất là hai việc khác nhau
Xét theo góc độ chi phí/lợi ích, có một cực trị cục bộ rất mạnh nghiêng về phía xả ra thật nhiều code giá rẻ thay vì đầu tư dài hạn cho việc lớn, và lĩnh vực càng trưởng thành thì ngưỡng kỹ năng tối thiểu để chạm tới điểm đó càng thấp
Cũng không có nhiều tổ chức tập trung vào việc đào tạo nhân tài hàng đầu. Vì vậy, khi lĩnh vực mở rộng, hiện tượng kỹ năng trung bình bị bỏ mặc rồi suy giảm là điều dễ giải thích, và nếu xử lý phân phối sai cách thì về sau có thể rất tốn kém để sửa
Chứng minh được máy tính kiểm chứng là một lĩnh vực mà AI có thể trở nên hữu ích trong tương lai khá gần. Tuy nhiên, nó có thể gần với mạng nơ-ron trong engine cờ vua hơn là một LLM hoàn chỉnh
Việc tự tay chứng minh mọi thứ thì nhàm chán và tốn thời gian nên người ta đã dùng nhiều solver từ lâu, nhưng các tactic hay solver sẽ gặp khó nếu bạn ném vào quá nhiều định lý và bổ đề
Mạng nơ-ron với vai trò một cỗ máy tìm kiếm để dò ra các bổ đề liên quan bằng pattern matching là một hướng rất phù hợp
Quy nạp và hợp nhất bậc cao thực ra cũng là tổng hợp mã, và việc brute-force lặp lại mọi cây cú pháp có thể có là cực kỳ kém hiệu quả
Solver vốn dĩ đã backtracking, nên AI đưa ra 95% bổ đề vô dụng cũng không sao, và vẫn có thể tốt hơn hẳn so với tìm kiếm thủ công
Tuy vậy, tôi không chắc chứng minh được máy tính kiểm chứng có thật sự tốt cho việc truyền đạt hay không. Chứng minh để con người đọc vốn mang tính cấp cao và lược bỏ chi tiết không chỉ vì độ dài mà còn vì nhiều lý do khác
Vấn đề cốt lõi là nó phải gắn với định nghĩa hình thức của các đối tượng toán học được dùng trong chứng minh
Nhưng khi viết hay đọc chứng minh, con người không suy nghĩ theo cách đó. Thường ta có một cảm nhận phi hình thức ở cấp cao về việc mình đang làm gì theo nghĩa “về mặt tinh thần”, rồi chỉ điền vào các chi tiết hình thức khi cần
Mã máy tính hoạt động phần nào được vì ngữ nghĩa hình thức của ngôn ngữ gần với mô hình tinh thần hơn nhiều, còn toán học thì nhìn chung có mục tiêu khác
Chiến lược sledgehammer của Isabelle kết hợp các trình chứng minh định lý tự động như E, Z3, SPASS và Vampire để cố gắng chứng minh hoặc bác bỏ mục tiêu
Trên lý thuyết thì nghe có vẻ ổn, nhưng trên thực tế bạn lại nhận được một chứng minh tái dựng bằng cách áp dụng 12 bổ đề trông như ngẫu nhiên, và những chứng minh kiểu này vừa không đọc nổi vừa cực kỳ mong manh
Tôi không nghĩ AI sẽ giải quyết vấn đề này một cách thần kỳ
Hiện tại mạng nơ-ron có hiệu quả mẫu cực thấp, còn các bộ dữ liệu toán học hình thức thì nhỏ hơn rất nhiều so với các bộ dữ liệu như mã Python
Vài tháng trước, Terence Tao đã có một bài nói chuyện rất hay về chủ đề này và bàn chi tiết hơn về việc dùng Lean: https://www.youtube.com/watch?v=AayZuuDDKP0
Có người nói một nhà toán học đang làm việc hiện nay đã để GPT-4o chứng minh được một bổ đề có lẽ là mới trong lúc nghiên cứu
“Bạn đời của tôi là một nhà toán học, và tuần trước lần đầu tiên cô ấy dùng ChatGPT để thử chứng minh vài bổ đề phục vụ nghiên cứu. Chúng tôi đã nghi ngờ rằng các mệnh đề đó là đúng và cũng đã có đại khái hướng tiếp cận, nhưng cô ấy không phải chuyên gia về kiểu mệnh đề đó. Đây là lần đầu tiên tôi nhận được từ mô hình một chứng minh vừa chính xác vừa hữu ích
Bổ đề thứ nhất là điều mà cộng sự phát hiện ra khi tính toán với các giá trị e nhỏ. ChatGPT đã không tìm ra chứng minh cho đến khi được gợi ý thử dùng hàm Möbius
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
Bổ đề thứ hai có vẻ chuẩn mực hơn một chút và có lẽ Mathematica cũng làm được. Nhưng Mathematica không cho ra một suy dẫn gọn gàng, nên vẫn rất hữu ích
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
Những thứ này đang trở nên đáng sợ vì giỏi hơn rất nhiều ở suy luận và các chủ đề nặng
Nếu lĩnh vực học máy tiếp tục tập trung vào việc bổ sung năng lực hệ 2 để bù cho kiểu tư duy hệ 1 chủ yếu của LLM, thì mọi chuyện có vẻ sẽ khá dữ dội
Điều gợi tôi nhớ tới là generatingfunctionology
Đây là trí nhớ ấn tượng, chứ không phải suy luận mới
Chúng tôi nghĩ theo tổng của các phân hoạch có thứ tự chứ không phải tổng trên các phân hoạch với hệ số |τ|!, nhưng dĩ nhiên hai cách là như nhau
Nếu lấy các phân hoạch có thứ tự theo chu trình, tức dùng hệ số (|τ|-1)! thay vì |τ|!, thì kết quả ra 0 chứ không phải (-1)^e
Chứng minh tổ hợp của Beren là tạo một song ánh giữa các phân hoạch có thứ tự theo chu trình độ dài chẵn và độ dài lẻ bằng cách chọn một phần tử đặc biệt, nếu phần tử đó đứng một mình thì gộp nó với phần kế tiếp, còn nếu không đứng một mình thì tách nó thành một phần riêng
Với trường hợp thứ tự tuyến tính thì làm tương tự bắt đầu từ phần tử cuối cùng, nhưng các phân hoạch mà phần tử cuối cùng đứng một mình trong phần cuối cùng thì không được ghép cặp, nên ta đệ quy sang phần tử kế tiếp
Cuối cùng mọi thứ đều được ghép cặp, và chỉ còn lại phân hoạch trong đó mọi phần tử đều tách riêng và theo đúng thứ tự ban đầu. Tổng dấu theo tính chẵn lẻ của kích thước tập gốc sẽ dẫn tới mệnh đề ban đầu
Cũng không rõ tổng trên “τ ≤ τ” có bao nhiêu hạng, và điều này kết nối thế nào với việc thiết lập một trong hai vế trái hoặc phải ở bước 3 rồi suy ra vế còn lại
Thực ra ChatGPT đã nhớ lại hàm Möbius của lưới phân hoạch và lặp lại nó mà không có chứng minh, rồi sau đó nói ra những điều nghe có vẻ hợp lý bề ngoài
Việc thiết lập hàm Möbius đó mới thực chất là trọng tâm, và câu hỏi gần như tương đương với việc chứng minh hàm đó có đúng dạng như vậy
Hơn nữa, công thức tổng quát mà ChatGPT đưa ra cũng hơi sai, và chỉ đúng trong trường hợp |σ| = 1 vốn quan trọng cho chứng minh hiện tại
Thực tế điều này có thể được thấy ngay mà không cần dùng tường minh toàn bộ bộ máy hàm Möbius, bằng một phép quy nạp sơ cấp với N(t,e) là số phân hoạch thành t lớp tương đương và hệ thức truy hồi
N(t,e+1)=N(t-1,e)+tN(t,e)Có ba điều nổi bật trong cuộc phỏng vấn này
Thứ nhất, Tao hình dung một tương lai nơi ngay cả trực giác toán học cũng được “sản xuất” giống như các sản phẩm đầu ra khác của xã hội, và ông nói tới các nhà toán học quản lý dự án. Ông cho rằng lý do toán học chưa được công nghiệp hóa đến mức đó là do thiếu công cụ, và AI cùng các proof assistant có thể mang tính cách mạng ở điểm này. Tuy vậy, tương tác và dẫn dắt của con người vẫn cần thiết
Thứ hai, có rất nhiều tri thức ngầm không được đưa vào bài báo. Những thứ như trực giác hay hiểu biết về các thất bại đều quan trọng, nên ngay cả các nhà toán học hàng đầu cũng cần trao đổi với nhau để không lặp lại cùng một sai lầm
Thứ ba, ta rất dễ nghĩ rằng toán học đã được hình thức hóa đủ rồi, nhưng các bài báo thực ra giả định rất nhiều tri thức chung. Nếu hình thức hóa các chứng minh theo cách mà proof assistant có thể hiểu được, điều đó sẽ giúp nhiều người hiểu hơn chuyện gì thực sự đang diễn ra
Như Tao từng cho thấy trong bài nói về dự án Polymath, điều này cho thấy ông luôn là người tìm kiếm các phương pháp mới cho nghiên cứu toán học
Trước mắt, đây có thể là kiểu dự án chỉ khả thi khi những người đoạt Huy chương Fields như Tao hay Scholze có đủ dư dả để dành thời gian gấp 10 lần cho việc chứng minh
Tôi mới nói chuyện với một nghiên cứu viên sau tiến sĩ ở khoa toán thuộc nhóm hàng đầu, và anh ấy bảo quanh mình không có ai dùng lean4 trong công việc thực tế
Nếu là nhà nghiên cứu ở giai đoạn đầu sự nghiệp, có lẽ vẫn tốt hơn nếu tin vào trực giác và ra bài báo
Muốn nhìn chủ đề này cho đúng thì không thể chỉ dựa vào ấn tượng từ vài người
Ngược lại, ở những lĩnh vực có phong cách trực quan hơn như topo chiều thấp, tôi đoán là sẽ có ít người dùng proof checker hơn
Ở đây “trực quan” không có nghĩa là kém chặt chẽ hơn. Một chứng minh bằng hình vẽ cho một tương đương đồng luân sẽ khó chuyển cho Lean hiểu hơn rất nhiều so với việc liệt kê các bất đẳng thức
Tiện nói thêm, tôi làm ở mảng hình học/topo và vẫn chưa từng thấy hay nghe ai dùng các công cụ này
https://lean-lang.org/
https://github.com/leanprover/lean4
“Nếu AI đưa ra một chứng minh khó hiểu và xấu xí, ta có thể dùng nó để phân tích. Nếu chứng minh này dùng 10 giả định để đi đến một kết luận, thì khi bỏ đi một giả định, chứng minh đó còn hoạt động không? Kiểu khoa học này hiện chưa tồn tại vì chưa có nhiều chứng minh do AI tạo ra, nhưng sẽ xuất hiện một kiểu nhà toán học mới, những người tiếp nhận toán học do AI tạo ra và biến nó thành thứ dễ hiểu hơn” — đoạn này hoàn toàn trùng khớp với suy nghĩ của tôi về thiết kế API công khai của mã nguồn
Vai trò vốn trước đây chỉ do các lập trình viên kỳ cựu đảm nhiệm giờ đây có thể được đơn giản hóa rất nhiều và trở nên dễ tiếp cận với mọi người