Busy Beaver thứ năm được xác nhận, các nhà nghiên cứu tiến sát giới hạn của tính toán
(quantamagazine.org)- Busy Beaver Challenge với sự tham gia của hơn 20 người trên toàn thế giới đã xác minh số Busy Beaver của máy Turing 5 quy tắc là BB(5)=47,176,870
- Điều này xác nhận rằng cỗ máy dừng sau 47,176,870 bước do Marxen và Buntrock tìm ra năm 1989 thực sự là máy dừng 5 quy tắc chạy lâu nhất
- Nhóm đã kết hợp phương pháp phả hệ để giảm các ứng viên trùng lặp, chương trình nhận diện máy không dừng và Coq proof assistant để xử lý hàng chục triệu ứng viên
- Kết quả cuối cùng được hoàn thiện dưới dạng bằng chứng Coq dài 40.000 dòng do mxdys tích hợp từ các kỹ thuật của cộng đồng, và được chuyên gia Coq Yannick Forster của Inria rà soát
- Ở BB(6), cỗ máy 6 quy tắc Antihydra mang đặc điểm giống giả thuyết Collatz đã xuất hiện như một rào cản, khiến BB(5) có thể là số Busy Beaver cuối cùng mà nhân loại biết chính xác
BB(5) đã được xác nhận
- Nhóm Busy Beaver Challenge đã xác minh giá trị chính xác của BB(5) là 47,176,870
- Giá trị này biểu thị số bước tối đa mà một máy Turing có 5 quy tắc và có dừng có thể thực hiện
- Việc xác minh sử dụng Coq proof assistant, công cụ chứng nhận rằng chứng minh toán học được xây dựng không có sai sót
- Cristopher Moore của Santa Fe Institute đánh giá cao khía cạnh kỹ thuật xã hội lẫn kỹ thuật toán học của công trình này
- Damien Woods của Maynooth University ví tốc độ ra kết quả này như đang ở “lãnh địa của Usain Bolt”
- Điểm cốt lõi của BB(5) không nằm ở ứng dụng cho các lĩnh vực khoa học máy tính khác, mà ở chỗ đây là thành tựu đạt được tại ranh giới của tính không thể tính được
Bài toán Busy Beaver và bài toán dừng
- Bài toán Busy Beaver không xét ngôn ngữ lập trình thông thường mà xét máy Turing
- Máy Turing đọc và ghi 0 và 1 trên một băng vô hạn, trong khi đầu đọc ghi di chuyển từng ô và hoạt động theo bảng quy tắc
- Mỗi quy tắc chỉ định hành động tiếp theo tùy theo giá trị đang đọc là 0 hay 1
- thay đổi giá trị hoặc giữ nguyên
- di chuyển sang trái hoặc sang phải
- chỉ định quy tắc sẽ tham chiếu tiếp theo
- một quy tắc đặc biệt xác định khi nào máy sẽ dừng
- Bài toán xác định liệu một máy Turing cuối cùng có dừng hay sẽ chạy mãi mãi nói chung được gọi là bài toán dừng
- Alan Turing đã chứng minh rằng không có lời giải tổng quát cho bài toán dừng
- Việc săn Busy Beaver, thay vì giải tổng quát việc dừng hay không dừng của mọi cỗ máy, là công việc phân loại từng máy trong một tập hữu hạn khi số quy tắc đã được cố định
Busy Beaver game của Radó
- Trong bài báo năm 1962, Tibor Radó đã định nghĩa Busy Beaver game bằng cách nhóm các máy Turing theo số quy tắc
- Trong tập hợp tất cả các máy Turing có n quy tắc:
- một số máy sẽ chạy mãi mãi
- một số máy sẽ dừng
- trong các máy dừng, máy chạy lâu nhất là busy beaver
- số bước chạy của nó là BB(n)
- Để xác định BB(n), cần kiểm tra thời gian chạy của mọi máy dừng và chứng minh rằng toàn bộ các máy còn lại không dừng
- Việc đo thời gian chạy thường có thể thực hiện bằng mô phỏng máy tính, nhưng chứng minh không dừng thì gần như là giải bài toán dừng cho từng máy cụ thể
- Shawn Ligocki, cộng tác viên của Busy Beaver Challenge, xem công việc này là hoạt động ở “ranh giới của điều chưa biết”
Từ BB(1) đến BB(4)
- BB(1)=1 có thể kiểm tra dễ dàng
- nếu quy tắc đầu tiên dừng khi đọc 0 thì máy dừng ở bước đầu tiên
- nếu không, nó sẽ tiếp tục di chuyển dọc theo băng toàn số 0
- Chỉ với 2 quy tắc đã có hơn 6.000 máy Turing khác nhau; với 3 quy tắc là hàng triệu; với 4 quy tắc là hàng tỷ
- Allen Brady đã tích hợp phương pháp phả hệ vào chương trình máy tính để giảm trùng lặp bằng cách nhóm những cỗ máy có hành vi ban đầu giống nhau
- Shen Lin cùng với Radó đã chứng minh BB(3)=21, và kết quả được công bố năm 1965
- Năm 1966, Brady phát hiện một máy 4 quy tắc dừng sau 107 bước, và năm 1974 chứng minh rằng đó là BB(4)
- Sau đó, BB(4) đã là số Busy Beaver cuối cùng mà nhân loại biết đến trong hơn 40 năm
Cuộc săn Busy Beaver thứ năm
- Cuộc thi ở Dortmund năm 1984 là cuộc săn quy mô lớn đầu tiên nhắm tới BB(5)
- Có gần 1,7 nghìn tỷ máy Turing 5 quy tắc, và ngay cả khi liệt kê mỗi máy trong 1 mili giây thì cũng mất hơn 500 năm
- Cỗ máy bận rộn nhất mà những người tham gia Dortmund tìm được đã dừng sau hơn 100.000 bước
- Sau đó, một nhà nghiên cứu khác tìm được cỗ máy chạy hơn 2 triệu bước
- Heiner Marxen và Jürgen Buntrock đã phát triển các kỹ thuật toán học để tăng tốc mô phỏng máy Turing
- Năm 1989, Marxen chạy chương trình suốt cuối tuần trên chiếc máy tính mới mạnh mẽ của công ty và phát hiện một cỗ máy dừng sau 47,176,870 bước
- Buntrock tái hiện được kết quả, và đầu năm 1990 hai người công bố bài báo
- Trên thực tế, cỗ máy đó chính là Busy Beaver thứ năm, nhưng phải mất thêm hơn 30 năm nữa mới chứng minh được rằng toàn bộ các máy còn lại đều không dừng
Skelet và các cỗ máy chưa giải quyết được
- Đầu những năm 2000, nhà khoa học máy tính người Bulgaria Georgi Ivanov Georgiev đã tiến rất gần tới BB(5)
- Georgiev đã dành nhiều giờ mỗi ngày trong suốt 2 năm để cải thiện chương trình nhận diện máy không dừng
- Chương trình cuối cùng là 6.000 dòng mã dày đặc không có chú thích và mất hơn 1 tuần để chạy
- Chương trình này để lại khoảng 100 máy Turing chưa giải quyết được, và Georgiev dùng phân tích thủ công để giảm con số xuống còn 43
- Năm 2003, Georgiev đăng kết quả trực tuyến dưới bút danh Skelet
- 43 cỗ máy khó nhằn này về sau được gọi là Skelet machines theo bút danh của ông
- Georgiev cho biết sau hai năm làm việc cường độ cao, ông đã kiệt sức đến mức không thể nghĩ ra ý tưởng mới nào nữa
Cấu trúc hợp tác của Busy Beaver Challenge
- Tristan Stérin khởi động Busy Beaver Challenge vào năm 2022
- Dự án được triển khai theo hình thức hợp tác trực tuyến và phát triển thành một cộng đồng quốc tế hơn 20 người, trong đó có nhiều người đóng góp không có tư cách học thuật truyền thống
- Stérin cho rằng để xác định BB(5), cần có một chứng minh được ghi chép đầy đủ và có thể tái hiện
- Chương trình của Georgiev rất tinh vi nhưng khó để các nhà nghiên cứu khác rà soát
- Stérin chia nhỏ công việc dựa trên các cách tiếp cận sẵn có
- loại bỏ các cỗ máy trùng lặp bằng phương pháp phả hệ của Brady
- xác định các máy dừng trong vòng 47,176,870 bước
- xử lý các máy chạy mãi mãi bằng các chương trình độc lập, mỗi chương trình chứa một phương pháp chứng minh riêng
- Chương trình giai đoạn đầu được viết vào cuối năm 2021 đã tạo ra danh sách khoảng 120 triệu máy Turing, đủ để quyết định BB(5)
- Trong số đó, khoảng một phần tư dừng trước cỗ máy của Marxen và Buntrock, còn 88 triệu tiếp tục là đối tượng cần rà soát
- Stérin cũng xây dựng giao diện trực tuyến hiển thị hành vi của máy dưới dạng sơ đồ không-thời gian với lưới hai chiều của 0 và 1
Ngôn ngữ băng đóng và sự tăng tốc của hợp tác
- Shawn Ligocki tham gia Busy Beaver Challenge năm 2022 và khôi phục phương pháp ngôn ngữ băng đóng do Marxen tạo ra
- Phương pháp này cung cấp một khung toán học thống nhất để chỉ ra rằng máy Turing không dừng bằng cách tận dụng các mẫu trên băng của máy
- Ligocki đã viết bài blog giới thiệu kỹ thuật này, nhưng chưa biết cách viết chương trình bao quát mọi trường hợp
- Sau khi Justin Blanchard tham gia dự án, ông đã hiện thực hóa nó, và hai người đóng góp khác đã tăng tốc độ thực thi lên đáng kể
- Chỉ trong vài tháng, phương pháp ngôn ngữ băng đóng đã trở thành một trong những công cụ mạnh nhất của nhóm
- Kỹ thuật này thậm chí xử lý được 10 trong số 43 Skelet machine mà Georgiev để lại
- Ligocki cho rằng kết quả này sẽ không thể xuất hiện nếu chỉ có đóng góp của một người duy nhất
Skelet #1, Skelet #17 và Coq
- Skelet #1 là một cỗ máy luân phiên giữa các pha có thể dự đoán được và các pha hỗn loạn
- Tháng 3 năm 2023, Ligocki và Pavel Kropitz đã tăng cường kỹ thuật mô phỏng tăng tốc 30 năm tuổi của Marxen và Buntrock để phân tích Skelet #1
- Skelet #1 chỉ đi vào chu kỳ lặp sau khi vượt quá 1 nghìn tỷ × 1 nghìn tỷ bước, và chu kỳ lặp đó dài hơn 8 tỷ bước
- Sau khi học Coq, lập trình viên tự học 21 tuổi mei đã chuyển nhiều chứng minh của Busy Beaver Challenge sang Coq
- mei cũng chuyển chứng minh không dừng của Skelet #1 do Ligocki và Kropitz xây dựng sang Coq, giúp kết quả đó trở nên chắc chắn hơn
- Skelet #17 là một cỗ máy khó khác mà Chris Xu đã tạo ra bước đột phá
- Chứng minh của Xu rất xuất sắc, nhưng chứa trực giác toán học khó chuyển sang dạng hình thức chính xác mà Coq yêu cầu
- Nhóm muốn có các chứng minh có thể tái hiện một cách hợp lý, chứ không phải kiểu chứng minh “hãy chạy chương trình trong 6 tháng”
Bằng chứng Coq 40.000 dòng
- Tháng 4 năm 2024, một cộng tác viên mới chỉ được biết đến qua bút danh mxdys đã tham gia hoàn thiện chứng minh Coq
- Ngay cả nhóm cũng không biết vị trí hay bối cảnh cá nhân của mxdys
- Ngày 10 tháng 5, mxdys đăng trên Discord: “The Coq proof of BB(5) is finished.”
- Chỉ trong vài tuần, mxdys đã tích hợp các kỹ thuật và kết quả của cộng đồng để hoàn thiện một bằng chứng Coq dài 40.000 dòng
- Chứng minh được công bố trong kho Coq-BB5
- Yannick Forster, chuyên gia Coq của Inria, đã rà soát chứng minh này và đánh giá rằng đây không phải việc dễ hình thức hóa
- Kết quả là cỗ máy 47,176,870 bước do Marxen và Buntrock tìm ra hơn 30 năm trước đã được xác nhận thực sự là Busy Beaver thứ năm
- Georgiev cho biết ông chưa từng kỳ vọng bài toán này sẽ được giải trong đời mình
- Allen Brady qua đời ở tuổi 90 vào ngày 21 tháng 4 năm 2024, một tháng trước khi chứng minh được hoàn tất
BB(6) và ranh giới tiếp theo
- Các cộng tác viên của Busy Beaver Challenge đã bắt đầu chuẩn bị bài báo học thuật chính thức giải thích kết quả
- Bài báo dự kiến sẽ bổ sung cho chứng minh Coq của mxdys bằng các chứng minh để con người có thể đọc được
- Một số thành viên trong nhóm đã chuyển sang Busy Beaver tiếp theo
- mxdys và Racheline đã phát hiện một rào cản có vẻ rất khó vượt qua ở BB(6)
- Rào cản này là một cỗ máy 6 quy tắc có bài toán dừng mang đặc điểm giống Collatz conjecture
- Cỗ máy này được gọi là Antihydra
- Mối liên hệ giữa máy Turing và Collatz conjecture đã có từ bài báo năm 1993 của Pascal Michel, nhưng Antihydra có vẻ là cỗ máy nhỏ nhất mà sẽ không thể giải quyết nếu không có đột phá mang tính khái niệm trong toán học
- Scott Aaronson cho rằng BB(5) có thể là số Busy Beaver cuối cùng mà nhân loại sẽ biết
- Một số người đóng góp dự định tiếp tục xử lý các biến thể của bài toán Busy Beaver, nhưng không phải mọi người tham gia đều sẽ đi theo cùng một hướng
- Stérin cho biết Busy Beaver Challenge đã khiến ông tin chắc vào hiệu quả của hình thức nghiên cứu hợp tác trực tuyến, và ông muốn phát triển các công cụ phần mềm hỗ trợ những dự án hợp tác trong các lĩnh vực toán học khác
1 bình luận
Các ý kiến trên Hacker News
Có một bình luận của Scott Aaronson về kết quả này: https://scottaaronson.blog/?p=8088
Và cũng có vài luồng thảo luận lớn hồi đầu năm nay liên quan đến “leisure-class beavers”:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
Vốn dĩ bài toán hải ly bận rộn có nhiều biến thể, một trong số đó là hải ly bận rộn hàm, được định nghĩa bằng phép tính lambda [1]
Vì đo kích thước chương trình theo bit chứ không phải số trạng thái, nên có thể xác định được nhiều giá trị hơn; trong khi đến nay với máy Turing chỉ có 6 giá trị, phía này đã có tới 37 giá trị. Khoảng cách giữa giá trị lớn nhất đã biết và một giá trị vượt Graham's Number cũng chỉ là 13 bit chương trình. Một biến thể gần gũi [2] có thể được biểu diễn trực tiếp bằng độ phức tạp Kolmogorov, và Mikhail Andreev [3] cho rằng điều này quan trọng đối với các ứng dụng trong lý thuyết thông tin
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
Tôi tìm thấy https://oeis.org/A141475, nhưng ở đây với 5 thì ghi là 27 nghìn tỷ
Tôi nhớ đã xem một video giải thích định nghĩa đó
Tôi từng làm việc vài năm với một kỹ sư thông minh đến mức phi thường và khó hiểu, người thăng tiến cấp IC ở một công ty công nghệ tinh hoa nhanh hơn bất kỳ ai tôi từng thấy
Anh ấy đã nghỉ việc vài năm trước; khi tôi hỏi kế hoạch là gì, anh ấy nói sẽ nghiên cứu bài toán hải ly bận rộn. Tôi tò mò liệu người đóng góp ẩn danh mxdys, người hoàn tất chứng minh hình thức cho BB(5) trong bài viết, có phải là anh ấy không, nhưng có lẽ tôi sẽ mãi không biết
Tôi không rõ phần thưởng là gì, và nếu có trí tuệ xuất sắc như vậy thì tôi mong người đó giải các vấn đề liên quan hơn đến việc cải thiện thế giới
Bài báo gốc về hải ly bận rộn của Tibor Radó, “On Non-Computable Functions”, thực ra khá dễ đọc và thú vị
Bản hiện đại có thêm chú thích ở đây: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Điểm nổi bật ở đây là chứng minh này là một chứng minh Coq
Tôi tò mò liệu đây có phải là chứng minh quan trọng đầu tiên được triển khai ngay từ đầu trong trợ lý định lý, thay vì chuyển một chứng minh đã biết vào trợ lý định lý hay không. Trước đây cũng đã có chứng minh có máy tính hỗ trợ, nhưng định lý bốn màu hay giả thuyết Kepler chỉ về sau mới được chuyển sang môi trường kiểm chứng hình thức
Vấn đề chính là các bộ quyết định và chứng minh thủ công chưa được sắp xếp gọn gàng và có phần đáng ngờ. Đặc biệt Skelet #1 cần một chương trình chuyên dụng để tăng tốc đến mẫu cuối cùng [0], còn Skelet #17 buộc Xu phải dùng 7 trang suy luận dày đặc để chứng minh không dừng [1]. Chứng minh Coq đầy đủ đem lại mức độ tin cậy rất cần thiết cho các kết quả này
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
Có thể tôi chưa hiểu chính xác “môi trường kiểm chứng hình thức” nghĩa là gì, nhưng theo tôi biết định lý bốn màu đã được chứng minh bằng máy tính ngay từ đầu. Nỗ lực chứng minh ban đầu của Kempe có lỗi, nhưng đã cung cấp một số công cụ cơ bản dùng trong các chứng minh sau này, và cuối cùng định lý dường như đã được chứng minh bằng máy tính
Con hải ly bận rộn này được phát hiện vào năm 1990, và mọi máy có kích thước 5 có lẽ cũng đã được liệt kê ngay sau đó
Xin chúc mừng nhóm. Vậy là bài toán dừng của các chương trình máy Turing 5 trạng thái 2 ký hiệu trên băng trống đã được giải quyết
Tôi tò mò không biết đã có ai thử áp dụng cùng kỹ thuật cho trường hợp 2 trạng thái 4 ký hiệu chưa. Nhìn chung ký hiệu thường mạnh hơn trạng thái, nhưng mức đó có lẽ vẫn xử lý được và có thể có kết quả bất ngờ. Cả 6 trạng thái 2 ký hiệu lẫn 2 trạng thái 5 ký hiệu đều có vẻ khó xử lý, thậm chí có thể là khó theo cách chứng minh được. Nhân tiện, có một ý tưởng vô lý nhưng kỳ lạ là khá phổ biến rằng con người có thể trực giác được lời giải bài toán dừng bằng con mắt tâm trí hoặc cơ học lượng tử trong não; tất nhiên, chứng minh lần này không có những thứ đó tham gia
Theo tôi biết, chỉ riêng các bộ quyết định hiện đang dùng đã đủ để chứng minh mọi trường hợp còn lại của 2×4 là không dừng. Vì vậy, nếu không có lỗi lớn trong thiết kế bộ quyết định, từ nhà vô địch hiện tại ta có Σ(2,4) = 2.050, S(2,4) = 3.932.964. Chỉ là kết quả chưa được tổng hợp ở một nơi
Ở 2×5 có Hydra và ở 6×2 có Antihydra; hai máy này tính cùng một phép lặp, chỉ khác điểm bắt đầu và điều kiện dừng. Phỏng đoán chuẩn, liên quan đến bài toán 3/2 của Mahler, là phép lặp này phân bố đều modulo 2; nếu chứng minh được phỏng đoán đó, ta sẽ có cận trên và cận dưới cho tỷ lệ tích lũy của 0 và 1, qua đó gần như chắc chắn chứng minh được hai máy không dừng. Dĩ nhiên hiện chưa có phương pháp chứng minh nào được biết
Họ dùng một bộ sinh chứng minh dựa trên lý thuyết logic tên là Aleph*, và khi đó người ta đã biết từ 1.500 năm trước rằng ZFC không thể xác lập BB(18). So với năm 2024, không chương trình nào có từ trước thời Aleph* được dùng, thậm chí về mặt lý thuyết, để kiểm tra chứng minh vét cạn nhằm giải BB(18). Điều này trái với việc ngày nay về mặt lý thuyết ta có thể liệt kê và kiểm tra các chứng minh ZFC để giải BB(??)
Lập trường “con người trực giác được lời giải bài toán dừng” có nghĩa như vậy. Theo tôi biết, không có lý do lý thuyết mạnh nào cho thấy lịch sử tương lai như thế là bất khả thi. Và vì Busy Beaver là không tính được, con người hẳn đã phải phát triển lý thuyết mới để tạo ra chương trình cần thiết. Công lao của kết quả phải thuộc về một thứ gì đó; khi chương trình khi ấy chưa tồn tại, không thể quy cho tính toán được
Tôi tự hỏi liệu tất cả các chương trình không dừng độ dài 5 có tình cờ đều chứng minh được là không dừng hay không
“Sẽ không bao giờ chứng minh được rằng Σ(5) = 1.915 và S(5) = 2.358.064. Hoặc nếu một cận dưới lớn hơn được tìm thấy, thì có thể thay giá trị mới đó vào dự đoán này.”
Lý do là có khả năng cao tự nhiên đã cài ít nhất một vấn đề khó nắm bắt như giả thuyết Goldbach vào giữa các máy 5 trạng thái còn treo. Nói cách khác, rất có thể tồn tại các mẫu đệ quy không dừng vượt quá khả năng nhận biết của chúng ta. May mắn là dự đoán này đã không thành hiện thực, nhưng chỉ cách có thêm một trạng thái
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. Chương này cũng có trong ấn bản thứ 2, Springer, 1995, pp. 237–254.
Nếu theo nghĩa thực tiễn thì những người khác đã trả lời rồi. Nếu theo nghĩa toán học thì tôi nghĩ sẽ khá ngạc nhiên nếu BB(5) là bất khả quyết định. Vì 5 trạng thái 2 ký hiệu quá nhỏ để mã hóa hành vi bất khả quyết định
Tuy nhiên, do hệ quả của các định lý bất toàn, nhất định phải tồn tại một n nào đó mà toán học chuẩn không thể chứng minh giá trị của BB(n). Trong vài năm gần đây, nhiều người đã nghiên cứu xem có thể tìm và hạ n đó xuống thấp đến đâu; kỷ lục hiện tại[0] là 745. Kỷ lục này có lẽ còn hạ thấp được nữa, nhưng vẫn còn khoảng cách lớn giữa giá trị cao nhất chúng ta biết là 5 và giá trị thấp nhất mà ta biết là không thể biết, 745
[0] Phòng khi bạn thắc mắc “toán học chuẩn” là gì, đây là kỷ lục hiện tại cho cả ZFC lẫn PA. Vì vậy ít nhất với PA thì có vẻ lẽ ra phải có thể hạ thấp hơn. Cho đến nay dường như chưa tìm được cách nào tốt hơn trong PA so với ZFC, nhưng tất nhiên chẳng phải là nên có sao?
“Chỉ bốn ngày trước, mxdys và một người đóng góp khác tên Racheline đã phát hiện một rào cản có vẻ khó vượt qua đối với BB(6). Đó là một máy 6 quy tắc mà bài toán dừng của nó giống với giả thuyết Collatz, một bài toán toán học nổi tiếng khó xử lý. Mối liên hệ giữa máy Turing và giả thuyết Collatz đã có từ bài báo năm 1993 của nhà toán học Pascal Michel, nhưng máy mới được phát hiện, tên là ‘Antihydra’, có vẻ là máy nhỏ nhất không thể giải nếu thiếu một đột phá khái niệm trong toán học.”
Tôi từng viết một chương trình như dự án cá nhân để giải bài toán cắt vật liệu (https://en.wikipedia.org/wiki/Cutting_stock_problem)
Vật liệu tồn kho có các đoạn cắt dạng /---/, /---|, |---|, và vì không muốn lãng phí vật liệu ở các vết cắt 45 độ nên tôi không thể, hoặc không muốn, dùng chương trình có sẵn. Mô tả rằng Brady đã cắt bỏ các cây con tìm kiếm nơi khác biệt không quan trọng để tối ưu hóa việc tìm BB(4) khá giống với việc tôi đã làm để làm cho chương trình của mình chạy nhanh, nên thấy thú vị
Theo bài blog của Scott Aaronson, có 16.679.880.978.201 máy Turing 5 trạng thái
Tôi tò mò không biết người ta có biết bao nhiêu phần trăm trong số này dừng hay không. Sửa: số máy Turing n trạng thái là (4n + 1)^(2n). Tôi đã tìm thấy dữ liệu cho n nhỏ, khá giống phân tích mà tôi tò mò: https://github.com/LukasKalbertodt/beaver
Tôi không tìm thấy trên trang bbchallenge.org, nhưng mọi máy đều đã được phân loại
Tổng hợp lại thì phần chứng minh khá ngắn. Tính cả khoảng trắng và chú thích là 19.000 dòng Coq
Theo kinh nghiệm của tôi, nếu biên soạn thành một bài báo truyền thống thì có lẽ sẽ ngắn hơn nhiều so với phiên bản Coq. Tất nhiên độ dài của chứng minh không phải là thước đo độ khó hay độ phức tạp, nhưng có thể dùng như một tiêu chí rất sơ bộ
Khi nói về giới hạn tri thức của con người, ta thường nghĩ đến những định lý có thể chứng minh được nhưng quá phức tạp đến mức không con người nào hiểu nổi. Có lẽ chứng minh phức tạp nhất mà chúng ta có là phân loại các nhóm đơn hữu hạn, dài đến hàng nghìn, hàng chục nghìn trang, và có khả năng trên Trái Đất chỉ có rất ít người, hoặc thậm chí không ai, hiểu trọn vẹn toàn bộ
Như bài viết nói, BB(6) có thể là không quyết định được. Nhưng cũng có khả năng nó có một chứng minh dài hàng triệu trang, nằm ngoài tầm với của nhân loại