jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学 Lean言語・形式証明系の普及を進めておられる北窓さんが執筆された本： ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 を購入して読み進めています。 扱っている言語はLean4です。Lean4は多くの数学者にも使われ始めているのですが、今までにまとまった本はなく、公式サイトで配布されている資料や有識者の方が書いた資料をベースに勉強を進めるのが今までの学習方法でした。本書が日本語で出版されたことで、まずは本書から勉強を始めることができるようになり、大変嬉しいことだと思います。 購入はこちらから可能です。 ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライ… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2025%2F09%2F30%2F183000" title="「ゼロから始めるLean言語入門」を読む - Maxima で綴る数学の旅" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20250919/20250919132205.jpg Hatena Blog https://hatena.blog 2025-09-30 18:30:00 rich https://maxima.hatenablog.jp/entry/2025/09/30/183000 1.0 100%