2024.03.12
https://www.youtube.com/watch?v=4YnulwFkUns
これバグとかかと思ったけど普通に尋常ではなく高速に回っているだけだったのすごすぎる
前:
2024.03.11
後:
2024.03.13
#日報
知った
Tarskiの高校代数問題
加法・乗法・累乗で表された正整数の恒等式は,加法・乗法・累乗の基本法則のみを用いて証明できるか?
https://github.com/arakur/ProofHSI/blob/a5aa7fdd05f7312fa42edde5b4b796df5eff2d9c/HSI.lean#L4C21-L4C71
これは出来ない(反例が存在する)ことがわかっている.
この事実を
Lean 4
で形式化したものがあった:
arakur/ProofHSI
おもしろい
知った
Hilbertの24番目の問題
やった
長らく放置していたが
直観主義命題論理のプライム性を用いたKripke完全性定理
をちゃんと埋めた.
プライム拡大補題
は
D. van Dalen; "Logic and structure"
のほうが見通しは良い.
ほとんど省略されているが
真理補題
は全く自明ではない.
観た
HAZBIN HOTEL
を観た.
アラスター
かっこよすぎる
知った
G. Restall
のwebサイトのドメインが
であることを知った
そんなドメインあるか?