Tính nhất quán của New Foundations – Chứng minh toán học khó đã được kiểm chứng bằng Lean

Dưới đây là phần tóm tắt các ý chính từ bài viết đã cho, được trình bày bằng Markdown:

Chứng minh tính nhất quán của lý thuyết tập hợp New Foundations

• Lý thuyết tập hợp "New Foundations (NF)" do Quine đề xuất năm 1937 đã được Randall Holmes tuyên bố là đã chứng minh tính nhất quán từ sau năm 2010
• Kho lưu trữ này chứng minh rằng NF thực sự không mâu thuẫn bằng cách kiểm chứng các phần khó trong chứng minh của Holmes bằng trình chứng minh định lý tương tác Lean
• Chứng minh hiện đã hoàn tất, và mệnh đề định lý có thể được tìm thấy trong ConNF/Model/Result.lean

Mục tiêu

• NF được biết là nhất quán khi và chỉ khi Tangled Type Theory (TTT) là nhất quán
• Chứng minh tính nhất quán của NF bằng cách xây dựng hình thức một mô hình của TTT trong Lean
• Công trình dựa trên nhiều phiên bản chứng minh của Holmes, nhưng đã có nhiều thay đổi và bổ sung để tương thích với lý thuyết kiểu của Lean
• Dự án này phụ thuộc vào mathlib, thư viện toán học cộng đồng được viết cho Lean, nên có thể sử dụng trực tiếp các kết quả quen thuộc về lực lượng, nhóm, v.v. mà không cần tự chứng minh lại
• Tất cả các định nghĩa và định lý trong mathlib và dự án này đều đã được hạt nhân đáng tin cậy của Lean kiểm chứng, nhưng Lean không thể xác nhận rằng mô tả của các định nghĩa và định lý có khớp với phần diễn giải tiếng Anh dự định hay không, nên cần cẩn trọng khi rút ra kết luận từ mã của dự án sang ngôn ngữ tự nhiên

Tangled Type Theory (TTT)

• TTT là một lý thuyết tập hợp đa hạng với quan hệ đẳng thức = và quan hệ thuộc ∈
• Các hạng được đánh chỉ số bởi một số thứ tự giới hạn λ, và các phần tử của λ được gọi là chỉ số kiểu
• Công thức x = y là hợp thức khi x và y có cùng kiểu, còn công thức x ∈ y là hợp thức khi x có bất kỳ kiểu nào nhỏ hơn y
• Một trong các tiên đề của TTT là ngoại diên tính: một tập hợp kiểu α được xác định duy nhất bởi các phần tử của nó ở mọi kiểu β bất kỳ với β < α
• Ví dụ, nếu hai tập hợp kiểu α khác nhau thì với mọi β < α chúng sẽ có các phần tử kiểu β khác nhau, và tính chất này khiến việc xây dựng mô hình của TTT trở nên khó khăn

Chiến lược

• Việc xây dựng mô hình sử dụng chiến lược tổng quát như sau:

  • Cấu hình kiểu cơ sở

    • Đặt λ là một số thứ tự giới hạn, κ > λ là một số thứ tự chính quy, và μ > κ là một lực lượng giới hạn mạnh có đồng bộ ít nhất là κ
    • Các tập hợp có kích thước nhỏ hơn κ được gọi là nhỏ
    • Ở mức -1, xây dựng một kiểu phụ trợ gọi là kiểu cơ sở, nằm bên dưới mọi kiểu cuối cùng sẽ là một phần của mô hình
    • Các phần tử của kiểu này được gọi là nguyên tử (không phải nguyên tử theo nghĩa của ZFU hay NFU), có μ nguyên tử và được chia thành các litter có kích thước κ

  • Cấu hình từng kiểu

    • Ở mỗi mức kiểu α, tạo ra một họ các phần tử mô hình cho mô hình dự định của TTT, đôi khi được gọi là t-tập hợp
    • Tạo ra một nhóm hoán vị gọi là các hoán vị được chấp nhận, và chúng tác động lên các t-tập hợp
    • Quan hệ thuộc được bảo toàn dưới tác động của các hoán vị được chấp nhận
    • Mỗi t-tập hợp được yêu cầu phải có một giá đỡ dưới tác động của các hoán vị được chấp nhận; đây là một tập nhỏ các đối tượng gọi là địa chỉ, sao cho bất kỳ hoán vị được chấp nhận nào cố định mọi phần tử của giá đỡ thì cũng cố định t-tập hợp đó
    • Với mỗi t-tập hợp ở mức α, một mở rộng ưu tiên ở kiểu β < α được cung cấp, và từ các phần tử của t-tập hợp có thể khôi phục được việc nó ưu tiên mở rộng nào
    • Các mở rộng ở những kiểu con khác của các t-tập hợp này có thể được suy ra từ mở rộng β, nhờ đó có thể thỏa mãn tiên đề ngoại diên tính của TTT

  • Kiểm soát kích thước của từng kiểu

    • Mỗi kiểu α chỉ có thể được xây dựng dưới giả định rằng mọi kiểu β < α đều có kích thước đúng bằng μ, cùng với các giả thuyết khác
    • Có thể dễ dàng chứng minh rằng họ các t-tập hợp ở mức α có lực lượng ít nhất là μ, nên cần chỉ ra rằng tập này có nhiều nhất μ phần tử
    • Điều này có thể thực hiện bằng cách chỉ ra rằng không có quá nhiều mô tả khác biệt về mặt bản chất đối với sự rối xoắn dưới tác động của các hoán vị được chấp nhận
    • Việc này đòi hỏi định lý tự do của tác động, một bổ đề kỹ thuật cho phép xây dựng các hoán vị được chấp nhận
    • Kết quả chính của phần này nằm ở đây

  • Hoàn tất phép quy nạp

    • Chạy đệ quy quá trình trên để tạo ra các kiểu rối xoắn ở mọi mức kiểu α
    • Trong lý thuyết tập hợp đây là bước dễ, nhưng trong lý thuyết kiểu cần rất nhiều công sức do sự đan xen giữa các giả thuyết quy nạp khác nhau
    • Sau đó kiểm tra xem cấu hình này có thực sự tạo ra một mô hình của TTT hay ít nhất thỏa mãn một tiên đề hóa hữu hạn của lý thuyết hay không
    • Nhóm tác giả đã chọn chuyển tiên đề hóa hữu hạn của Hailperin cho lược đồ bao hàm của NF thành một tiên đề hóa hữu hạn của TTT và trình bày nó trong tệp kết quả
    • Tuy nhiên lựa chọn này là tùy ý, và có thể dễ dàng chứng minh các tiên đề hóa hữu hạn khác bằng cách sử dụng hạ tầng đã được chuẩn bị sẵn

Ý kiến của GN⁺

• Chứng minh này là một kết quả rất có ý nghĩa vì đã hình thức hóa việc chứng minh tính nhất quán của lý thuyết tập hợp NF, điều trước đây chỉ được biết đến ở mức rất trừu tượng. Đây không chỉ quan trọng về mặt toán học thuần túy mà còn cho thấy tiến bộ thực chất trong công cụ hỗ trợ chứng minh và chứng minh định lý tự động
• Việc hình thức hóa bằng Lean đảm bảo tính chính xác và đầy đủ của chứng minh, nhưng đồng thời cũng có thể khó hiểu với các nhà toán học vì được viết bằng một ngôn ngữ không quen thuộc. Cần song hành với đó là công việc giải thích rõ ràng các ý tưởng cốt lõi của chứng minh bằng ngôn ngữ tự nhiên
• Phần giải thích trực quan về lý do tiên đề ngoại diên tính kỳ lạ của TTT là cần thiết, hay mối quan hệ của nó với các lý thuyết tập hợp khác, vẫn còn khá thiếu. Nếu được bổ sung thêm thảo luận về bối cảnh triết học và lịch sử chứ không chỉ chứng minh hình thức, mức độ hiểu biết về lý thuyết NF sẽ còn được nâng cao hơn
• Các hướng nghiên cứu tiếp theo như mô hình được xây dựng có quan hệ thế nào với mô hình của lý thuyết tập hợp ZFC tiêu chuẩn, hay tính nhất quán của NF liên hệ ra sao với tính nhất quán của các hệ tiên đề khác, cũng có vẻ rất đáng quan tâm
• Trường hợp hình thức hóa một chứng minh phức tạp như vậy bằng Lean có thể trở thành hình mẫu cho việc tự động hóa chứng minh ở các lĩnh vực toán học khác. Nếu những công việc tương tự được thử nghiệm với các định lý mà trước đây quá trình chứng minh chưa được biết rõ, chúng có thể tạo ra tác động lớn đối với cộng đồng toán học

[GN⁺]

Ý kiến Hacker News

• Nguy cơ chứng minh bằng Lean bị sai là rất thấp. Tuy nhiên, bất kể có lỗi trong Lean hay không, vẫn cần đọc kỹ kết luận và xác nhận rằng điều thực sự được chứng minh là đúng, vì đây là vấn đề đã được biết đến trong kiểm chứng phần mềm và toán học.
• Trường hợp này có vẻ là ví dụ đầu tiên về việc dùng proof assistant để giải quyết trạng thái của một chứng minh khó. Trước đây đã có các dự án kiểm chứng những chứng minh sẵn có có chứa các thành phần tính toán quy mô lớn được xử lý bằng phần mềm không đáng tin cậy, nhưng đây là trường hợp đầu tiên mà vị thế nhận thức luận của kết quả vẫn còn không chắc chắn trong giới toán học.
• Có ý kiến thắc mắc về sự khác biệt nền tảng giữa Coq và Lean, cũng như liệu chúng có hoạt động trên cùng một loại logic hay không. Trong các thảo luận liên quan, nhiều nội dung khó hiểu đã được nhắc đến.
• Những người ủng hộ Lean có xu hướng nhấn quá mạnh rằng Lean là phương pháp chứng minh vượt trội. Lean chỉ là một phương pháp chứng minh thay thế; với tư cách là một ngôn ngữ lập trình và hệ thống, nó cũng có lỗi riêng và phụ thuộc rất lớn vào nhiều tầng thư viện khác nhau do người khác viết.
• Thay vì nói rằng Lean bảo chứng minh là đúng, sẽ chính xác và trung thực hơn nếu nói rằng chứng minh đã được một nhà toán học con người kiểm tra, rồi được chuyển sang Lean và cũng được kiểm tra ở đó. Cách mô tả rằng Lean cung cấp một sự xác minh duy nhất và mang tính tuyệt đối là không chính xác, hoặc ít nhất người viết chưa thấy cách giải thích nào như vậy.
• Có người đề nghị một lời giải thích khái quát, ở mức sinh viên đại học ngành toán hoặc chuyên gia kỹ thuật có thể đọc được, về điểm gì khiến phép hình thức hóa lý thuyết tập hợp "New Foundations" này trở nên đặc biệt hoặc mới mẻ so với các hình thức hóa khác.
• Có người tự hỏi liệu cách tiếp cận này cuối cùng có dẫn đến chứng minh cộng tác và việc 'sửa lỗi', biến toán học thành một quy trình tương tự như code trên GitHub hay không.
• Có câu hỏi rằng theo định lý Gödel, mọi hệ đủ mạnh đều không thể tự chứng minh tính nhất quán của chính nó, vậy điều này nên được hiểu ra sao.
• Có người muốn tiếp tục theo dõi dự án mathlib nhưng không có thời gian. Họ thắc mắc liệu có cách nào tham gia theo kiểu rất thụ động hay không.