Tiến độ hình thức hóa Định lý cuối cùng của Fermat
(xenaproject.wordpress.com)- Công việc chuyển chứng minh FLT sang Lean đã diễn ra tháng thứ hai; các định nghĩa R và T cần cho định lý “R=T” của Wiles vẫn chưa hoàn tất, nhưng một kết quả đại số giao hoán trừu tượng đã được chứng minh
- Mục tiêu không phải là sao chép nguyên trạng chứng minh gốc của thập niên 1990, mà là xây dựng trên Lean và mathlib một chứng minh đã được tổng quát hóa và đơn giản hóa nhờ các công trình về sau của Diamond/Fujiwara, Kisin, Taylor, Scholze, v.v.
- Trong khi hình thức hóa crystalline cohomology cần cho chứng minh hiện đại, dự án phát hiện một vấn đề: một bổ đề then chốt trong bài báo năm 1965 của Roby, tài liệu chuẩn về cấu trúc divided power, có vẻ là sai
- Brian Conrad tìm thấy một chứng minh thay thế trong phụ lục sách của Berthelot-Ogus, và Arthur Ogus cũng trả lời rằng ông biết cách sửa các lỗi trong phụ lục đó, nhờ vậy dự án có thể tiếp tục
- Trường hợp này cho thấy rủi ro khi các chứng minh chi tiết của toán học hiện đại dựa vào trí nhớ chuyên gia và tri thức ngầm, đồng thời củng cố lý do thực tiễn để ghi lại chứng minh trong các hệ thống hình thức
Tình trạng hiện tại của việc chuyển chứng minh FLT sang Lean
- Công việc dạy máy tính chứng minh Định lý cuối cùng của Fermat (FLT) đã diễn ra tháng thứ hai
- Cần rất nhiều công sức để định nghĩa trong Lean R và T là gì trong định lý “R=T”, phần cốt lõi của chứng minh Wiles; hiện cả hai định nghĩa đều chưa hoàn tất
- Nghiên cứu sinh tiến sĩ Andrew Yang đã chứng minh xong kết quả đại số giao hoán trừu tượng cần thiết
- Đó là kết quả có dạng: “nếu hai vành trừu tượng R và T thỏa nhiều điều kiện kỹ thuật, thì chúng bằng nhau”
- Bản thảo hiện tại được công khai dưới dạng blueprint
- Hệ thống được dùng là Lean và thư viện toán học mathlib
- Những ai biết một chút về Lean và lý thuyết số có thể tham gia qua hướng dẫn đóng góp, bảng điều khiển dự án, và issue
Vì sao không chuyển nguyên trạng chứng minh của thập niên 1990
- Dự án không hình thức hóa nguyên trạng chứng minh của Wiles trong thập niên 1990
- Về sau, các công trình của Diamond/Fujiwara, Kisin, Taylor, Scholze, v.v. đã làm chứng minh trở nên tổng quát hơn và đơn giản hơn
- Mục tiêu không chỉ là chứng minh FLT, mà còn xây dựng trong Lean cả những kết quả tổng quát và mạnh hơn
- Nếu cuộc cách mạng AI trong toán học thật sự xảy ra và Lean trở thành một thành phần quan trọng, việc máy tính có các định nghĩa cốt lõi của lý thuyết số hiện đại ở dạng có thể hiểu được sẽ hữu ích
Divided powers cần cho crystalline cohomology
- Chứng minh đang được hình thức hóa sử dụng crystalline cohomology, thứ không có trong chứng minh gốc của Wiles
- Lý thuyết này phát triển ở Paris trong thập niên 1960–70, với nền tảng do Berthelot xây dựng dựa trên các ý tưởng của Grothendieck
- Các hàm mũ và logarit cổ điển rất quan trọng để hiểu hình học vi phân và de Rham cohomology, nhưng trong những bối cảnh số học như characteristic p, chúng không hoạt động nguyên xi
- Divided power structures, được phát triển trong các bài báo của Roby thập niên 1960, đóng vai trò then chốt trong việc xây dựng các hàm tương tự có thể dùng trong bối cảnh số học
- Để dạy Lean crystalline cohomology, trước hết cần hình thức hóa divided powers
Vấn đề trong tài liệu của Roby lộ ra khi làm việc với Lean
- Antoine Chambert-Loir và Maria Ines de Frutos Fernandez đang hình thức hóa lý thuyết divided powers trong Lean
- Trong mùa hè, Lean đã phát hiện vấn đề trong lập luận kiểu con người của tài liệu chuẩn; sau khi kiểm tra, một bổ đề then chốt trong công trình của Roby có vẻ là sai
- Về mặt kỹ thuật, bài báo của Berthelot không phát triển lý thuyết divided powers từ đầu mà dùng “Les algebres a puissances divisees” của Roby
- Bài báo đó đăng trên Bull Sci Math, 2ième série, 89, 1965, trang 75–91
- Lemme 8 ở trang 86 có vẻ sai, và cũng không rõ phải sửa chứng minh thế nào
- Chứng minh đó trích dẫn sai một bổ đề khác trong bài báo Ann Sci ENS năm 1963 của Roby
- Mệnh đề đúng là
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), nhưng trong quá trình áp dụng đã thiếu một tensor product
- Vấn đề này phá vỡ chứng minh của Roby rằng divided power algebra của một module có divided powers, và kết quả là chặn việc định nghĩa vành
A_cris
Tình huống giống “chứng minh bị khuyết” hơn là “lý thuyết sai”
- Điều này không có nghĩa bản thân crystalline cohomology về thực chất là sai
- Các định lý chính dường như vẫn đúng, nhưng chứng minh mà Antoine và Maria Ines đang đi theo là không hoàn chỉnh
- Vì Roby, Grothendieck và Berthelot đều đã qua đời, không thể hỏi trực tiếp các chuyên gia ban đầu
- Nhiều chuyên gia cho rằng ngay cả khi bổ đề trung gian là sai, chứng minh của các kết quả chính vẫn có thể sửa được
- Trong hình thức hóa, chỉ phán đoán rằng “có thể sửa được” là chưa đủ; cần một chứng minh đã thật sự được sửa
Lối đi vòng nhờ phụ lục Berthelot-Ogus
- Tadashi Tokieda kể chuyện này cho Brian Conrad ở Stanford, và Conrad hỏi câu chuyện crystalline cohomology bị sai là thế nào
- Sau khi nghe các chi tiết kỹ thuật, Conrad đồng ý rằng có vẻ có vấn đề và bắt đầu kiểm tra
- Vài giờ sau, Conrad cho biết trong phụ lục cuốn sách về crystalline cohomology của Berthelot-Ogus có một chứng minh khác rằng universal divided power algebra of a module có divided powers
- Theo góc nhìn của Conrad, cách tiếp cận này có vẻ ổn, và nhờ vậy chứng minh có thể tiếp tục
- Sau đó, khi ăn trưa với Arthur Ogus ở Berkeley và kể rằng phụ lục này đã giải quyết vấn đề, Ogus trả lời rằng phụ lục đó cũng có nhiều lỗi, nhưng ông biết cách sửa
Vì sao tài liệu toán học hiện đại cần hình thức hóa
- Quá trình này cho thấy cách con người ghi chép toán học hiện đại có thể chưa đủ vững chắc
- Nhiều sự thật vẫn nằm ở dạng “các chuyên gia biết”, và có thể không được trình bày chính xác trong tài liệu
- Dù các ý tưởng quan trọng đủ vững để chịu được những cú sốc như vậy, chứng minh chi tiết thực tế có thể không nằm ở nơi ta kỳ vọng
- Nếu ghi chép toán học đúng cách trong các hệ thống hình thức, có thể giảm mạnh khả năng xảy ra lỗi
- Ngay cả với các nhà toán học không theo chủ nghĩa hình thức, nếu muốn máy học lập luận của con người để tự làm toán, trước hết cần có quá trình dạy lập luận đó cho máy
- Maria Ines đã trình bày về việc hình thức hóa divided powers tại Cambridge Formalization of Mathematics seminar, và các vấn đề đó được hiểu là đã được sắp xếp lại
- Dự án đã trở lại đúng quỹ đạo, nhưng vẫn còn khả năng tài liệu lại tiếp tục gây trở ngại
1 bình luận
Các ý kiến trên Hacker News
Tôi nhớ hồi học cao học từng viết mã chạy nhanh để hỗ trợ cách tiếp cận tính toán của giáo sư hướng dẫn đối với giả thuyết Birch–Swinnerton-Dyer
Tại một seminar về lý thuyết số ở thành phố gần đó, tôi được hỏi “anh đang cố củng cố bằng chứng ủng hộ giả thuyết này à”, và khi tôi cười đáp “Không, tôi muốn tìm phản ví dụ hơn”, các chuyên gia đã nổi giận dữ dội
Lý thuyết số quá lâu đời và sâu sắc đến mức việc viết luận án tiến sĩ trong lĩnh vực đó gần như chỉ là bước đầu để trở thành người mới nhập môn; dù biết ký hiệu và định nghĩa, tôi vẫn chưa chạm tới được trực giác bên dưới
Vì vậy, cơn giận của các chuyên gia trước câu “tôi kỳ vọng có phản ví dụ” để lại trong tôi sự tò mò hơn là sợ hãi, và tôi tự hỏi họ đang nhìn thấy điều gì mà vẫn chưa diễn đạt được thành lời
Những tiến bộ trong việc hình thức hóa như thế này khiến toán học dễ tiếp cận hơn rất nhiều với những người quen lập trình hơn
Nỗi bất an về việc thiếu tính hình thức là chính đáng, nhưng tôi cho rằng phản ứng đúng trước nỗi bất an không phải là né tránh mà là tò mò
Nếu một tay lính mới non nớt như bạn tìm được phản ví dụ bằng các phép tính thô và nổi tiếng chỉ sau một đêm, toàn bộ công sức và cấu trúc ấy có thể sụp đổ, nên tôi nghĩ họ đã tức giận
Nếu đưa lời khuyên về cao học toán cho bản thân thời trẻ, tôi sẽ nói rằng với mỗi bài tập “chứng minh X” không tầm thường, hãy dành ít nhất 1/4 thời gian để tìm phản ví dụ
Trong bài tập thì 99% sẽ thất bại, nhưng hiểu biết về vấn đề sẽ lớn hơn nhiều; còn ở 1% còn lại, bạn có thể trông như thiên tài
Khi bước vào nghiên cứu toán học thực sự, xác suất ấy sẽ đổi theo hướng có lợi hơn nhiều cho cách tiếp cận ưu tiên phản ví dụ
Tôi nhớ hồi còn là sinh viên, một người bạn kể rằng có ai đó vừa kết thúc ngày đầu tiên của seminar và mọi người đều phấn khích nói rằng ông ấy sẽ chứng minh được Định lý cuối cùng của Fermat
Người đó là Andrew Wiles, và sau đó, sau khi bổ sung trong vài tháng để xử lý một vấn đề được phát hiện trước khi xuất bản, cuối cùng toàn bộ công trình đã được công bố
Với tư cách một người đang học toán, đó là một sự kiện cực kỳ phấn khích, nên khi thấy cách nói “chứng minh kiểu cũ của thập niên 1990”, tôi thật sự cảm thấy mình già đi
Gần như cả lớp đều là học viên cao học toán, và tôi nghĩ mình không hiểu nổi 20% tài liệu
Tôi thích đoạn nói Lean đã làm một việc đôi khi gây bực mình: nó phàn nàn về cách trình bày lập luận kiểu con người trong tài liệu chuẩn, và khi xem kỹ thì quả thật lập luận của con người có chỗ thiếu
Bỏ qua sự bực bội pha trò ra, đây là điều đáng kinh ngạc, và tôi nghĩ Lean cùng các trình chứng minh định lý khác sẽ trở thành công cụ quan trọng trong toán học về sau
Đoạn nói tài liệu hóa toán học hiện đại còn kém khiến tôi liên tưởng đến UI/UX/thiết kế web
Nhà thiết kế tạo ra các mockup, prototype và luồng tương tác phi hình thức, thiếu chính xác rồi chuyển cho lập trình viên; lập trình viên phải hình thức hóa chúng thành mã và giải thích chính xác cho máy
Trong quá trình đó, họ tất yếu phát hiện các lỗ hổng như những kịch bản tương tác hay đường đi mã mà thiết kế chưa tính đến; đôi khi các lỗi thiết kế lớn lộ ra và lập trình viên hoặc nhà thiết kế phải lấp chúng
Thiết kế và phát triển là các vai trò khác nhau, đòi hỏi lối tư duy khác nhau, và đa số nhà thiết kế rất kháng cự việc làm việc và suy nghĩ như lập trình viên
Sau thất bại đó, chúng ta đã biết rằng không thể hình thức hóa hoàn toàn toán học, và điều này chỉ ra vấn đề căn bản của cách tiếp cận dùng AI để làm toán
Nếu quan tâm đến chủ đề này thì nên xem mã thực tế
Ví dụ: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Bản thiết kế tổng quan giải thích cấu trúc toàn bộ mã cũng đáng xem: https://imperialcollegelondon.github.io/FLT/blueprint/
Dù chỉ nhìn từ bên ngoài, việc xem mã Lean trông ra sao và mọi người đóng góp như thế nào rất thú vị
Tôi cũng thích việc không cần unit test. Theo một nghĩa nào đó, mệnh đề chứng minh cuối cùng chính là unit test
Chẳng hạn, các ví dụ nhỏ và phản ví dụ để kiểm tra rằng một định nghĩa nào đó không rỗng đóng vai trò như vậy
Từ góc nhìn của một người từng làm toán thuần túy, vấn đề lớn là các nhà toán học hầu như không cung cấp các chứng minh tự hoàn chỉnh
Không có động lực để làm vậy, và đôi khi các tác giả còn tự hào về việc “bỏ qua chi tiết”
Rốt cuộc, nếu muốn một chứng minh chặt chẽ có thể theo dõi mọi bước logic, thì chuyên gia phải lấp vào những khoảng trống không dễ tìm thấy trong tài liệu
Đôi khi chỉ khả thi khi có người như vậy viết một cuốn sách giải thích tất cả, và đôi khi ngay cả thế vẫn chưa đủ
Nếu chỉ xét những gì được ghi lại, phần lớn toán học hiện đại đang đứng trên nền tảng bất ổn
Bài báo nghiên cứu toán học được viết cho các chuyên gia khác trong cùng lĩnh vực, và đôi khi có quá ít chi tiết nên tôi thường phàn nàn khi phản biện đồng cấp
Nhưng nếu thật sự cung cấp mọi chi tiết, bài báo sẽ dài hơn rất nhiều
Một ví dụ có thể giải được nếu có nền tảng toán phổ thông vững là bài toán chứng minh rằng tồn tại các hằng số C, X > 0 sao cho với một số thực x > X nào đó,
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < CxNhững mệnh đề dạng này xuất hiện liên tục trong lý thuyết số giải tích, và với chuyên gia thì hiển nhiên đến mức trong bài báo hầu như luôn được viết ra mà không chứng minh
Nếu tạo một chứng minh đầy đủ và chặt chẽ, nó sẽ dài và nhàm chán, và không chuyên gia nào muốn đọc
Cách tiếp cận này có chi phí đánh đổi, nhưng có vẻ vẫn ở mức có thể quản lý
Nghe giống giai đoạn thứ ba mà Tao nói đến: trực giác có thông tin
Ông ấy nói: “Nếu bạn đã làm một việc gì đó 100 lần, bạn có thể nói ‘như dễ dàng quan sát thấy’ rồi bỏ qua”
Nói cách khác, tôi hiểu là cần có người với cơ sở dữ liệu trong đầu tìm ra liệu các tiền đề của một định lý và kết luận ở câu tiếp theo có khớp hay không
Hoặc tôi tò mò liệu có những phần toán học hiện chưa thể diễn đạt theo cách mà bộ kiểm chứng chứng minh có thể đánh giá hay không
Hoặc có lẽ việc dùng bộ kiểm chứng chứng minh chưa phổ biến như tôi tưởng. Nghe giống vị trí của ngôn ngữ kiểu tĩnh trong lập trình
Tức là muốn hỏi đã từng có trường hợp nào một chứng minh được chấp nhận rộng rãi có khiếm khuyết nghiêm trọng vì phần được lướt qua bằng cách nói đại khái chưa
Nếu chuyện đó chưa xảy ra thì cũng dễ hiểu vì sao người ta có thái độ lỏng lẻo trong việc nêu rõ chi tiết
Tôi luôn tự hỏi liệu trực giác rằng “crystalline cohomology đã được dùng quá nhiều từ thập niên 1970 nên nếu có vấn đề thì hẳn đã lộ ra từ lâu” có thật sự đúng không
Liệu có thật sự bất khả thi đến vậy khi cả một nhánh toán học được phát triển trên một chứng minh có khiếm khuyết, rồi nhánh đó đơn giản bị phát hiện là sai hay không
Ông đã tận mắt chứng kiến một lĩnh vực sụp đổ vì một sai sót trong “bổ đề đầu tiên ở trang đầu tiên” của bài báo nền tảng
Có thể xem dòng chảy từ công trình ban đầu về UniMath, năm đặc biệt tại IAS, rồi đến cuốn sách HoTT là những gì đã đẩy chủ đề hình thức hóa toán học lên vị trí ngày nay
Nếu nền tảng sai, một trong các phản ví dụ đó cũng có thể phản bác định lý nền tảng, nên việc xây trên nền tảng sai thậm chí còn có khả năng làm lộ ra khiếm khuyết của nền tảng
Tương tự, khi toán học thỉnh thoảng được áp dụng để tạo dự đoán, nếu toán sai thì dự đoán cũng sai, và dự đoán sai đó sẽ thu hút rất nhiều chú ý
Thật ra từ “lĩnh vực” hơi dễ gây hiểu lầm; nhiều lý thuyết giống một nút thắt được buộc với nhiều lý thuyết khác trong toàn bộ toán học hơn
Các lý thuyết đó lại kết nối với các lý thuyết khác nữa
Sẽ là một tình huống rất kỳ lạ nếu chỉ phần nền tảng sụp đổ về mặt logic mà không ảnh hưởng gì đến các phần khác của nút thắt này
Một khối toán học khổng lồ trôi nổi, hoàn toàn nhất quán nội bộ nhưng chỉ có đúng một lỗi, là điều khó hình dung trong trường hợp cohomology của bài này
Nói nghiêm ngặt thì đây gần với một thái độ triết học, nhưng tôi muốn tin rằng nhiều phần của toán học hiện nay, theo nghĩa nào đó, đã được phát hiện một cách tự nhiên
Bật mí là dù vậy thế giới vẫn tiếp tục vận hành
Trong khoảng một năm qua, tôi thỉnh thoảng thử hình thức hóa một phần chương trình giải tích phức bậc đại học bằng Lean
Có nhiều điều để học và cũng rất đáng làm, nhưng đôi lúc khá bực bội
Gần đây tôi mới có thể định nghĩa hoàn chỉnh dạng cực như một song ánh từ C* đến (-pi,pi] x R, dù số phức, chuỗi lũy thừa, exp, sin đã có sẵn trong mathlib, vì tôi cứ khăng khăng muốn định nghĩa “từ đầu”
Rất có thể phần lớn khó khăn đến từ việc tôi chỉ có bằng cử nhân toán, chưa quen với Lean/mathlib và không có người hướng dẫn. Dù vậy, cộng đồng Zulip đã giúp ích rất nhiều
Nhiều kết quả trong mathlib được phát biểu khá trừu tượng, nên khó nắm được chúng liên hệ thế nào với các định lý chuẩn ở bậc đại học, hoặc liệu những định lý đó có trong mathlib hay không
Điều này hợp lý với cộng đồng toán nghiên cứu, nhưng với cá nhân tôi thì là một trở ngại lớn; nếu Lean được dùng nhiều hơn trong giáo dục, đây có thể trở thành vấn đề tương tự. Tuy nhiên, theo thời gian thì phần này có thể được sắp xếp lại
Tôi cho rằng tự động hóa chứng minh vẫn chưa đủ
Quá nhiều thứ khó chứng minh hơn mức lẽ ra phải có, và điều tôi bất mãn nhất là ép kiểu
Trong toán học thông thường, số thực là một tập con của số phức, nên điều gì đúng với mọi số phức thì tự động đúng với mọi số thực; nhưng trong Lean, chúng là các kiểu khác nhau và phải qua lại bằng ánh xạ đơn ánh/phép ép kiểu, làm lu mờ trọng tâm của chứng minh
Khi các phép ép kiểu chồng chất, chẳng hạn đổi số tự nhiên thành số thực rồi lại thành số phức, mọi thứ trở nên đặc biệt rối rắm
Tất nhiên, đây có thể là vấn đề đặc thù của chủ đề này; trong các lĩnh vực như đại số, nơi xử lý các ánh xạ tường minh, có lẽ nó sẽ tự nhiên hơn nhiều
Rất dễ được chỉ dẫn về cách dùng mathlib, cái gì đã tồn tại và nằm ở đâu
Vấn đề các lớp ép kiểu chồng lên nhau nhìn chung được giải quyết bằng tactic
norm_castNgay cả khi không phải là một câu hỏi cụ thể, nếu bạn chỉ nhắc thoáng qua hoặc trong mã có phong cách chứng minh phức tạp không cần thiết, bạn vẫn có thể nhận được gợi ý về những tactic mà mình chưa biết
Nếu chỉ cảm thấy việc hình thức hóa quá khó mà không biết nên dùng kỹ thuật nào, bạn có thể lấy một chứng minh không vừa ý mà mình vất vả tạo ra, tách thành một ví dụ độc lập rồi hỏi để mọi người thử rút gọn nó
Những câu hỏi như vậy thường được chào đón và ai cũng học được nhiều
Chủ đề này có vẻ nói về cách viết toán cho tốt
Tôi đã đọc, viết, dạy, áp dụng và xuất bản toán học trong nhiều thập kỷ, và cũng có bằng tiến sĩ toán ứng dụng
Đúng là việc viết toán có vấn đề, và một số bài toán được viết rất tệ
Nhưng cũng có những tác phẩm toán học được viết khá tốt
Ít nhất, mọi ký hiệu phải được định nghĩa trước khi dùng; sẽ hữu ích nếu đưa ra động cơ trước khi trình bày toán học; và đôi khi giải thích trực giác cũng có ích
Đọc kỹ những tác phẩm toán học được viết tốt sẽ giúp học cách viết toán
Ví dụ có thể kể đến Finite-Dimensional Vector Spaces của Paul R. Halmos, Advanced Calculus của R. Creighton Buck, Mathematical Analysis của Tom M. Apostol, Real Analysis của H. L. Royden, Real and Complex Analysis của Walter Rudin, Probability của Leo Breiman, và Mathematical Foundations of the Calculus of Probability của Jacques Neveu
Tác giả đã cố kiểm chứng Định lý cuối cùng của Fermat đúng theo cách nó được triển khai trong tài liệu, và trong quá trình đó phát hiện rằng một bổ đề chống đỡ cả một phân ngành không đúng ở dạng đã được sử dụng
Dù vậy, lý do để tin rằng lĩnh vực đó nhìn chung vẫn có thể cứu vãn là niềm tin rằng nếu nó thật sự sai thì hẳn ai đó đã tìm ra một kết quả phủ định rồi
Giờ cần tìm một thứ thay thế phù hợp để chống đỡ lĩnh vực đó
Tác giả viết khá thú vị, nên dù tôi không hiểu khoảng một nửa, trải nghiệm đọc vẫn dễ chịu một cách kỳ lạ
Tôi đã tìm thấy một từ hay để dùng khi một chứng minh bị bác bỏ hoặc phát hiện có khiếm khuyết: vitiated
Tôi thích nó vì ít gây hiểu lầm rằng kết luận đã bị chứng minh là sai, nhưng vẫn truyền đạt được rằng chứng minh đó đã bị tổn hại và cần một chứng minh mới hoặc sửa chữa