TL;DR
- Lean で自然数と整数を動くプログラムとして作りながら、数学とソフトウェアが Lean でどう結び付くかを確かめる本である。
- Lean でソフトウェアを開発するための基礎と、定理証明の基本を身に付けられる。
対象読者
ソフトウェアとして数学を扱いたい人や、数学の力をソフトウェアに結び付けたい人に向けた本である。出版社の紹介ページによると、数学の形式化に興味がある数学者のほか、数学に挑戦したいプログラマや、計算機科学の抽象的な概念を手を動かして確かめたいエンジニアも対象にしている。
目次
- ゼロから始めるLean言語入門
- Leanによる初めての証明
- Leanにおける論理
- 帰納法で、足し算の性質を証明する
- 分配法則を証明し、マクロで再利用可能にする
- 自然数の順序と、計算を利用する証明
- 同値関係で割って整数を作る
- Mathlibを使って整数の性質を証明する
- grindタクティク
感想
本を読みながら手を動かした学習リポジトリは https://github.com/radish-miyazaki/LeanBook にある。