コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

ACL2 をやってみた

ACL2(Lisp系)

満を持して ACL2 をやろうと思い立った。
しかし殆ど解説記事が無い...

環境

  • Windows ではうまくいかなかった。
  • Racket もうまくいかなかった。
  • Jupyter のやつは未確認です。
  • Eclipse でできた。これの正式名称は ACL2s というらしい。
    Install ACL2 Sedan
    Ubuntu でおこなった。
    解凍すると、Eclipse も内蔵されている。

画像

.lisp ファイルで命題を書いて、.a2s ファイル上で REPL をおこなう。

はじめの一歩

1=1を証明した。

(defthm one
  (equal 1 1)
  :rule-classes nil)

意味としては、1=1を書いて、後は自動定理証明器にまかせるかんじだ。
ACL2 の自動定理証明器にばんばん命題を投げていくやり方は、
Lean とも Isabelle とも違うなと思った。

参考記事

TojoQK の投稿
とても分かり易いです。




<紹介>コラッツパターンを超えしもの その2

コラッツ予想

前回

下位ビットの状態遷移図

イメージ

イメージとしては、(nが正の場合)左上の001から出発して、
中央のループをぐるぐる回って、
最後に右下の4-2-1ループに辿り着くかんじだ。

現存する4種類のループがあらわれている

この図で未知のループは存在するか？

下位ビットでのあるループ候補は実はループではなかった → (コラッツ予想としての)対応するループ候補もループではない
は対偶論法で言えると思うので。




<紹介>コラッツパターンを超えしもの

コラッツ予想

コラッツパターン

かつてコラッツパターンというものを考えていた。

平衡三進法

平衡三進法なるものを知った。三進法だが要素を {-1, 0, 1} としている。

コラッツパターンでは左を下位としているが、こちらは右を下位としている。

紹介

これに関して先行研究がある。 自分は Kindle版 を購入してみたが、証明の準備段階までしか書いてなかった。
ペーパーバック版には証明が書いてあるのだと思う。

このやり方にはすごい秘密が隠されていそうだ。