ushumpei https://blog.hatena.ne.jp/ushumpei/ ushumpei’s blog https://ushumpei.hatenablog.com/ Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。 Lean4 が気になっている理由としては 定理証明支援系で堅牢なソフトウェアかけるんじゃないかなという期待 Lean4 が関数型言語 + 定理証明支援系 という部分 定理証明支援系の使用例を調べてみたが、今回の学習からどう繋がっていくかイメージがまだついていない Hyper-V, Ironclad (契約管理？), ... など… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fushumpei.hatenablog.com%2Fentry%2F2023%2F04%2F05%2F120641" title="Lean4 学習 - ushumpei’s blog" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2023-04-05 12:06:41 rich https://ushumpei.hatenablog.com/entry/2023/04/05/120641 1.0 100%