入力となる式が2つ必要な推論規則の扱いが難しい・・・、これがあることで証明がすごくごちゃごちゃした感じになってしまうし、読みづらくなってしまう・・・

プログラミングだと、こういう状況あまり無い気がするなぁ・・・

UX の良い proof verifier を作ろうと思うと、推論規則を結構沢山用意しないとなかなか使い物にならないかも

かと言ってあまりにも多くの推論規則があると「覚えられない」となりそうなので、なかなか難しい・・・

a0. some a { all b { S b != a } }
d0. let 0 { all a { S a != 0 } }
a1. all a b { a = b -> b = a }
a2. all a b c { a = b & b = c -> a = c }
a3. all a b { a = b & b is Nat -> a is Nat }
a4. all a { a is Nat -> S a is Nat }
a5. all a b { S a = S b -> a = b }
a6. all a { S a != 0 }
a7. all pred K { K 0 & all a { K a -> K S a } -> all a { K a } }

バビロン捕囚のバビロンと、キュロスが征服したバビロンが同じものだと分かって、聖書世界と古代ギリシャ世界がグッと近いものに感じられるようになった

みんな AI 好きだなぁ・・・

完全系列 (exact sequence) という言葉を久しぶりに聞いた。やはり数学書は良いものだ

10進数をちゃんと定義して使う、自然言語も極力制限して使う、みたいな数学書を書いたら面白そう

基本の syntax ぐらいは、練りに練ってからもう breaking change しないぐらいの感じでスタートしてほしいもんだなぁと思ったり・・・

Deno も結構そういうところあるけど、Lean のチュートリアル、ちょっと古いやつだと最新の Lean で動かなくなってるぽいのがあるっぽくて注意が必要そうだ・・・

lean4 関数適用式で括弧省略するタイプか・・・嫌いだなぁ

数学者、10進数を定義しないで使いがち

bijective base n もそうだけど、times が全般的に JSR 移行されていないので、そろそろしておこう・・・

bijective base n まだ JSR に移して無かった・・・、今度移行しよう・・・、このライブラリここ数年で自分が書いたモジュールの中で一番好きかも・・・

https://deno.land/x/bijective_base_n@v0.1.1

Lean 4 公式の install 方法が VSCode 経由なのか https://lean-lang.org/lean4/doc/quickstart.html

test

UUID って 6 bits (4.7%, ver + var) をシステムと関係ないメタ情報で使わされてるし、使う意味ないんじゃないかなぁ・・・エンコーディングが非効率的な hex なのも何だか意味がわからない

UUIDv1 = time_low + time_mid + ver + time_high + var + clock_seq + node

UUIDv6 = time_high + time_mid + ver + time_low + var + clock_seq + node

最初の総理大臣就任が明治18年なの面白いなぁ。それまでの国の代表は誰なんだろう?

なんとなく Paul Valéry の La Jeune Parque という作品に興味を持った。フランス語やってて良かった

Parque というのはファイブスター物語でお馴染みの運命の3女神 (ラケシス、クローソー、アトロポス) の事らしい