SnO₂WMaN @sno2wman@fedibird.com

開発機と運用機が別れていないためおれがMathlib4の適当なファイルを開いてもし証明が非常に複雑だった場合はCPU使用率が100%になってOtoMADB側のAPIが重くなるというメチャクチャな事態でずっと生きている

現状ではVSCodeに限って言えば（Emacs等他はどうかは知らない）Nixの例えばdevshellなどが上手くVSCodeと上手く噛み合ってくれるかはかなり微妙で多分出来ておらず，おとなしくelanを入れるか，どうしてもクリーンな環境を保っておきたいならdevcontainerとかを使うのが良いと思う（Mathlib4のものを参照）

https://github.com/leanprover-community/mathlib4/tree/master/.devcontainer

Lean4はNixでも環境構築できる( https://leanprover.github.io/lean4/doc/setup/nix.html )という旨が書かれて入るが内容の通りかなり実験的な状態で，少なくともこれに書かれたテンプレートを用いると毎回最新のLean4をビルドする羽目になって大変なことになる気がする（lean-toolchainは無視される）のと，Lean側で依存しているライブラリ等もNIxで明示的に記載しなければならず二度手間になる上に場合に依っては出来ないケースもある（Mathlib4がそうでNix Flakeを提供していないため）#要調査

https://scrapbox.io/sno2wman/2023.07.26#64c0a27113a1580000c95a55

Lean4を汎用的な関数型プログラミング言語として使うのならCIとかもちゃんとしないとダメだなと思ってGitHub Actionsを用意してみたが，Mathlibに依存していると凄まじく時間がかかり，どうにかしようとしたが結局よくわからなかった（何をキャッシュすればよいのだろう？）

https://scrapbox.io/sno2wman/Lean_4_on_GitHub_Actions

近況としては主に戸次『数理論理学』に基づいて(最小/直観主義/古典)命題論理をLean4で形式化しているが、まだ殆ど何も示していない（せいぜいHilbert流体系について整理したのみ）

https://github.com/SnO2WMaN/lean4-propositional-logic

日報(2023.07.26)

https://scrapbox.io/sno2wman/2023.07.26

日報(2023.07.25)

https://scrapbox.io/sno2wman/2023.07.25

そういえばこの形式の論理式には驚嘆すべき帰結(Consequentia mirabilis)という名前が付いていたことを思い出す

https://en.wikipedia.org/wiki/Consequentia_mirabilis [参照]

日報(2023.07.24)

https://scrapbox.io/sno2wman/2023.07.24

日報(2023.07.23)

https://scrapbox.io/sno2wman/2023.07.23

日報(2023.07.22)

https://scrapbox.io/sno2wman/2023.07.22

日報(2023.07.21)

https://scrapbox.io/sno2wman/2023.07.21

足し算と掛け算しか無いPeano算術に原始再帰的関数全部突っ込んでも本質的には変わらないのでOKという定理ありがたすぎていいな

日報(2023.07.20)

https://scrapbox.io/sno2wman/2023.07.20

情報ありがとうございます．

https://mstdn.jp/@palalansouki/110745269567319776 [参照]

そういえばPeano算術はPAなのにRobinson算術はなぜRAとかでなくQとして表すのだろうか

ここでの投稿内容に数式入れたらKaTeXで適当に表示してくれないかな