これらの数を計算するのに力技だけでは無理だよ。計算不可能なんだから。

5状態のチューリングマシンを徹底的にチェックする必要があると思うけど、その後は力技がちょっとだけ役立つだけだよね。力技じゃ、チューリングマシンが永遠に止まらないってことはわからないんじゃない？

ちょっと違うと思うけど、論文のこの部分が関係してると思うよ：

証明の構造。私たちの主な結果である定理1.1の証明は第6章にあります。証明の構造は次の通りです：マシンは木の正規形（TNF）で列挙され、検索空間のサイズが劇的に減少します：16,679,880,978,201の5状態マシンから「たった」181,385,789に。詳しくは第3章を見てね。各列挙されたマシンは、主に停止するかどうかを判断しようとするアルゴリズムである決定器を通して処理されます。停止問題の計算不可能性のため、普遍的な決定器は存在せず、すべての技術は合理的な時間内に大規模なマシン群を判断できる決定器を作ることにあります。私たちの決定器のほとんどは、チューリングマシンが訪れる構成のセットをより便利な上位集合で近似する抽象解釈フレームワークのインスタンスで、これを「閉じたテープ言語（CTL）」と呼んでいます。これは停止構成を含まず、チューリングマシンの遷移に対して閉じています（第4.2章を参照）。S(5)パイプラインは表3に示されています - S(2,4)については表4を見てください。この研究のすべての決定器はbbchallengeコラボレーションによって作成されました；第4章を参照してください。5状態マシンの場合、13のスパラディックマシンは決定器では解決できず、個別の非停止証明が必要でした（第5章を参照）。だから、彼らは検索空間を大幅に減らす方法を見つけ、残りの検索空間の大部分が停止するかどうかを証明できる一般的な決定器を書いたけど、一般的な決定器が推論できなかった残りの13台のマシンは手動で解決する必要があったんだ。

ここにはいくつかの概念が関わってるね。まず、特定の数学理論（おそらく一貫性があって再帰的に公理化できるもの）に基づいて、何が証明できるかを考えなきゃいけない。そんな理論に対して、BB(N)の正確な値を証明できない有限のNが存在するんだ。だから「無限の時間」があれば、理論が力尽きるところまで、すべての証明を列挙して、次々とビジービーバーの値を確認できるかもしれない。これはゴーデル/チャイティンの不完全性のビジービーバー版だね。BB(5)の場合、ペアノ算術が十分で、RCA₀も多分いける。もっと強力な理論はどこから来るのか？それはちょっと謎だけど、確かにその研究はたくさんあるよ（フェファーマンやフリードマンの研究を見てみて）。次に、有限の時間で何が実現可能かを考えなきゃ。機械を列挙することも、証明を列挙することもできるけど、具体的な戦略には限界がある。BB(5)の場合、著者たちは単純な力技は使わなかった。5状態の機械を徹底的に列挙して（対称性の削減後）、ほとんどすべての機械の停止/非停止の挙動を証明するために認定された決定器を使って、いくつかの残った機械については手動で証明（形式化もされた）を提供したんだ。

BBチャレンジのサイトはすごくよく構成されてるね： https://bbchallenge.org/13650583

最近、Lean言語での数学的証明をブループリント（依存グラフ）を使って共同作業する動きがあるみたいで、関連してるっぽい。例えば： https://teorth.github.io/equational_theories/ https://teorth.github.io/pfr/

このコメントを見て、https://www.distributed.net/ がまだ存在しているか確認したくなった。おそらく20年近くこのサイトのことを考えてなかったけど、1990年代後半にRC5-64を解読していた頃にクライアントを動かしてたんだ。でも、今でもこの種のことに使えるプラットフォームとして続いているみたいだね。

論文では、似たような構造と規模を持つ2つのコミュニティについて言及しているよ： - https://conwaylife.com/、コナウェイのライフゲームや他のセルオートマトンについて - Googology、https://googology.fandom.com/wiki/Googology_Wiki と https://googology.miraheze.org/wiki/Main_Page、大きな数について

Coq-BB5では、機械は100Mステップ実行されるのではなく、直接決定器のパイプラインに投げ込まれるんだ。ほとんどの停止する機械は、ループを使って低いパラメータ（最大4,100ステップ）で検出されて、47Mステップまでシミュレーションされたのは183機械だけだよ。レガシーbbchallengeのシードデータベースでは、機械は正確に47,176,870ステップ実行されて、約80Mの非停止候補が残った。差異は、Coq-BB5が0RBや他の小さな要因を除外していないことから来ている。また、「5状態のチューリングマシンは約1億8100万種類ある」と言われているけど、この数字は証明が完了した後にしか得られないことに注意が必要だね。この数字を知るのはBB(5)を解くのと同じくらい難しいんだ。

書いてくれてありがとう、すごく面白い！ロックが選ばれる理由って何かあるの？他の選択肢じゃなくて…あと、これも見てみて。 https://www.youtube.com/watch?v=c3sOuEv0E2I

ありがとう。素晴らしい仕事だね。

これはすごく分かりやすい素晴らしい要約だね。書いてくれて本当にありがとう！

すべてのチューリングマシンに対して機能する普遍的なアルゴリズムは存在しない。これは疑われているのか、それとも証明されているのか？もし証明があるなら、ぜひ読みたいな。

じゃあ、6州TMで同じことやったら、残るスパラディックはどれくらいになるんだろう？

まとめてくれてありがとう！あの13のスパラディックから何か学べることはあったの？それとも本当にただのスパラディックなの？

現代のEpycシステムで、マシンを1億ステップ評価するのにどれくらいの計算時間がかかるんだろう？

ビジービーバー問題は、理論的なコンピュータサイエンスの質問の中でも最も理論的で、純粋に数学的なものの一つだよ。本当に抽象的な意味で何が可能かを考えることなんだ。それに取り組むことで、ソフトウェアの挙動を分析する能力が高まったけど、そのスキルや関連する技術が、実用的なことをするもっと複雑なソフトウェアの挙動を分析するのに直接役立つかは明らかじゃない。ここで分析されていたプログラムは、典型的なソフトウェア開発者の基準からすると非常に小さいものだし。具体的に言うと、これらの方法のいくつかが、証明支援ツールや最適化コンパイラで使える演繹的技術をインスパイアする可能性があると思うけど、その応用が明らかであるとも保証されているわけでもない。これに取り組んでいる人たちは、間違いなく応用コンピュータサイエンスではなく、理論的コンピュータサイエンスをやっていると自分たちを表現していたと思うよ。

BB数の研究は純粋に学問的で、それ以上のものになる可能性は低いよ。数学の他の部分が間違っていることが判明しない限りね。現在の理解では、これらの数は本質的に無用であることが保証されている。特にこの証明は、値がすでに知られているという意味で二重に学問的で、これは結果を独立して検証しやすくする方法に過ぎないんだ。これは、他のもの（例えば、フェルマーの最終定理）のために機械証明を提供するという広い動きの一部で、いくつかの面で有益かもしれない（例えば、問題を特定したり、証明の一部を「再利用可能」にしたりすること）。

純粋に学問的で、値を知ることで直接的な応用や何かが解放されるわけではない。利益はすべて、道中で学んだことにあるんだ。

具体的な利益を定義して、過去200年の間に具体的な利益をもたらした純粋数学の例を挙げてみて。ひとつの利益は、数学の基礎に関係していることだよ。もしビジービーバー番号745を見つけられたら、数学を証明したり反証したりできるし、ビジービーバー6を見つけたら、コラッツのような未解決問題を証明できるかもしれない。ほとんどのコア研究は直接的には役に立たないけど、間接的な手段を通じて役立つことが多い。例えば、これはその複雑さからリーンの改善点を見つけることにつながっただろうね。リーンコミュニティはMathlibみたいなプロジェクトからたくさん学んでいるのを知ってるし、リーンはAWSを良くしたり、飛行機の安全性を向上させたりするのに使われてるんだ。

これは純粋に学術的なもの…なのかな？G.H.ハーディの自伝は「数学者の謝罪」ってタイトルなんだけど、彼はちょっと冗談っぽく、純粋数学の人生を謝りたかったんだよね…完全に学術的で、全く役に立たないって。で、彼が亡くなった数年後、彼の数学はマンハッタン計画で初めて成功した原爆を作るのに重要だったんだ。彼の数学が世界を変える装置につながって、100年間人間の生活のあらゆる側面に影響を与えた。誰かが「使い道」を見つけるまでは「役に立たない」だけなんだよ。追記：この本はラマヌジャンとの時間を記録してるよ。「無限を知った男」という映画が好きなら、「謝罪」を読むべきだね。

100年前には、数論や非ユークリッド幾何学が具体的な利益を持つのか、純粋に学術的なものなのかを尋ねることもできたよね。ビジービーバー問題については、今のところ答えは「いいえ」だけど、純粋数学の有用な応用を見つける道のりは誰にも分からないんだ。

ビジービーバー問題を解決する方法を研究することは、静的解析などのさまざまなアプリケーションで停止問題を扱う方法を探求し、発展させるのにも役立つんだよね。

これは人類の美しい成果だよね。月に行くのと同じくらい。誰かが月に行くことに鉱採掘や岩に関連する応用があるかもしれないって言うかもしれないけど、基本的にはそれだけじゃないんだ。これを「純粋に学術的」って呼ぶのは好きじゃないな、なんか古臭くて虫食いの匂いがするし、全然面白くないから。これは純粋に精神的で、心温まるもので、頭を使うことでもある。山登りの人にK2に登ることに実用的な利点があるか、あるいは「学術的」かって聞くようなもんだよね。

結果自体は純粋に学術的だね。将来的に役立つかもしれないって言ってる人もいるけど、元数学博士の私としては、これは概念的なブレイクスルーというより、大規模な帳簿整理みたいに感じるな。ただ、すごくいい結果ではあるけどね =)

いわゆる「自然なアルゴリズム」が忙しいビーバーから生まれたんだ。で、その中には、改善されたデータベースやグラフィックス、その他いろんな形で、いつか役に立つものがあるはずだよ。

これはそのプロジェクトから出た（プレプリント）論文なんだ。つまり、レビューされて引用できるように、完結した作業の説明が含まれてるってこと。基本的な結果は変わってないけど、詳細のプレゼンテーションが今は完了してるよ。

コラッツに似てるけど、一つ大事な点があって：終わることが知られてるんだよね！

面白いね、BB6（「アンチヒドラ」）の候補にもなりそうなものが、コラッツ的なことをしてるみたい。コラッツって、長くて複雑な有限列を作るための良い設計図なのかな？

ウィキペディアによると、BB(6)の下限は2^2^2^2^2^2...を33554432回繰り返したものだって。これは確実に急成長する関数だね！

コックは使ったことがないけど、この特定のケースでは、答えはかなりトリビアルな「はい」なんじゃないかな？証明を作成するのは巨大な研究の苦労で、発表可能な結果だし、検証するのは自分が書いたメモを見返すだけだもん（このチューリングマシンは停止しない、これが入力で、これが生成する繰り返しの数列、あのチューリングマシンは常に停止する、そしてこれがその証明の方法…）。でも、もっと一般的に言うと、あなたの質問は実際にはミレニアム賞問題で、百万ドルの価値があるんだよ。

まとめた証明を確認するのに、普通のノートパソコンだと数時間かかるけど、途中の実験や列挙にはもっと多くの処理能力が必要だったのは明らかだね。

一般的に、ZFCのすべての数学的証明に当てはまることだね（もっと強力な理論でも同様）。決定問題「式Fと整数nが与えられたとき、長さが<= nのFのZFC証明は存在するか？」はNP完全なんだ。つまり、証明を確認するのは多項式時間でできるけど、証明を導出するのには指数関数的な時間がかかることがあるってこと。

最高の褒め言葉だね。