今日も updateLive() を書いた。
まだバグは直らない。
今日も updateLive() を書いた。
まだバグは直らない。
満を持して ACL2 をやろうと思い立った。
しかし殆ど解説記事が無い...
.lisp ファイルで命題を書いて、.a2s ファイル上で REPL をおこなう。
1=1
を証明した。
(defthm one (equal 1 1) :rule-classes nil)
意味としては、1=1
を書いて、後は自動定理証明器にまかせるかんじだ。
ACL2 の自動定理証明器にばんばん命題を投げていくやり方は、
Lean とも Isabelle とも違うなと思った。
TojoQK の投稿
とても分かり易いです。
今日も updateLive() を書いた。
今日も updateLive() を書いた。
今日も updateLive() を書いた。
イメージとしては、(nが正の場合)左上の001
から出発して、
中央のループをぐるぐる回って、
最後に右下の4-2-1ループ
に辿り着くかんじだ。
下位ビットでのあるループ候補は実はループではなかった → (コラッツ予想としての)対応するループ候補もループではない
は対偶論法で言えると思うので。
かつてコラッツパターンというものを考えていた。
平衡三進法なるものを知った。三進法だが要素を {-1, 0, 1} としている。
コラッツパターンでは左を下位としているが、こちらは右を下位としている。
これに関して先行研究がある。
自分は Kindle版 を購入してみたが、証明の準備段階までしか書いてなかった。
ペーパーバック版には証明が書いてあるのだと思う。
このやり方にはすごい秘密が隠されていそうだ。