seasawher https://blog.hatena.ne.jp/seasawher/ パンの木を植えて https://seasawher.hatenablog.com/ 私が書いたLean言語の本が出版されました。 ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発www.lambdanote.com 9/4 に出版されて購入可能になっていたのですけど、報告が遅れてしまいました。よろしくお願いします。 さて出版を機に再び話題にしたいのですが、以前こんなコメントをいただきました。 東大の植田一石先生の4年講究で"Mathematics in Lean"が講究本に入ってたことが少し話題になってましたね。私は各論文雑誌がコンパイルの通ったLeanのコードを提出することが義務化される世の中になる事を切望しています（そうしたら論文が完璧に読めるよ… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fseasawher.hatenablog.com%2Fentry%2F2025%2F09%2F06%2F212334" title="出版報告と、なぜ私は初等的な話しかしないのかについての弁明 - パンの木を植えて" 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 2025-09-06 21:23:34 rich https://seasawher.hatenablog.com/entry/2025/09/06/212334 1.0 100%