うかうかしていたら７月になりました．
今はまだ７月になった程度で済んでいますが，そのうち８月もやってくることでしょう．特にキリは良くありませんが，このあたりで再び振り返り記事を書こうと思います．前回の振り返り記事は４月８日で，だいたい３カ月経っています．
Lean by Example
「タクティク逆引きリスト」にかなり気合を入れて更新を叩き込みました．
まず，以前は Lean と Mathlib のタクティクを紹介するだけの本だったのですが，def や inductive や #check といったコマンドについても紹介するようになり，名前も「Lean by Example」と改めました．これはかなり大きな変更です．
リンク切れが怖いので「タクティク逆引きリスト」とは別の書籍として作ろうと思っていたのですが，lean ja のディスコードで「合体させた方が絶対見やすい」という声もあり決行する運びとなりました．（SnO2WMaNさんありがとうございました）懸念材料だったリンク切れ問題は気合と根性でリダイレクトしてほぼ解決したので，やって良かったです．
コマンド紹介は良い感じにできたので，今後さらに紹介対象を拡大していこうと思ってます．ちょっとした計画があります．
というのも，私が Lean に関して問題だと思ってることの一つに，読まなきゃいけないドキュメント多すぎ問題 があります．
Lean 言語の公式マニュアル Lean Manual を筆頭に，証明をする方法を解説した Theorem Proving in Lean, 数学理論を形式化する方法を解説した Mathematics in Lean, 関数型プログラミングを行う方法を解説した Functional Programming in Lean, そしてメタプログラミングの方法を解説した Metaprogramming in Lean 4 と，なんと主要ドキュメントだけで５つもあります．これを全部読まないと言語の全貌がつかめないというひどい事態になっているわけです．
おまけに，ドキュメントが分散しているせいで「あれどこに書いてあったっけ？」というとき探すのが面倒です．上記の５つのドキュメントについて検索を繰り返さなければならないからです．しかも，目指す場所に辿り着いたとしても，そのドキュメントが「最初から順に読むことを意図して」書かれているために，その部分だけ読むと意味がわからないということがあります．数論幾何学よりはマシかもしれませんが，ひどいもんです．もうちょっと優しくしてほしいですね．
要は，「Lean 言語とライブラリの機能全体を概観できて」「各ページに依存関係がなくて」「知りたいことから該当箇所にたどり着きやすい」という条件を満たしているような新たなドキュメントが必要だと思うわけです．ついでに「最新の情報がきちんと反映されている」ことも要件に加えてもいいかも．そういうユーザのニーズに答えられるドキュメントとして，Lean by Example を成長させていきたいなと思っているのです．
わりと順調に成長できていると思うので，近い将来宣伝とか知名度向上がボトルネックになりそうだなと予想しています．
数学ボーイZさんから動画が出たよ
今まで Lean 言語についての動画を定期的に出している Youtuber は日本には存在しなかったのですが，数学ボーイＺさんという方が Lean の動画を出してくださるようになりました．
これで知名度が高まるといいな～と思ってます．実際ちょっと上がったっぽくてほくほくしています．lean ja のディスコードサーバのメンバーもちょっと増えて 55 人になりました．
しかし，なかなか形式証明というものが抱える問題自体がまだ大きく，一気に大ヒットというわけにはいかなさそうです．数学科で研究をしている人にとっては「Lean で何ができるの？」という感想になりそうですし，実際今できることはすごく少ないです．Lean は定理証明支援系として，以下のような問題があると感じています：
- Isabelle のスレッジハンマーのような強力なタクティクが欠けている．duper があるけど開発途上．
- 型クラスのダイアモンド継承があるときの解決法がめちゃくちゃ非自明で，問題を指摘する linter もない．
- Lean に組み込める計算機代数システムがまだないので，プログラミング言語としての利点が生かせない
- Lean と Mathlib のアップデートが毎月来るが，そのたびに破壊的変更が結構入るので，証明を保守するために自動更新ツールが欲しくなる
逆に言えば言語の基本的な設計とコミュニティは良いと思っているので，今後上に上げた問題がどう対処されていくか期待しています．
Lean と Mathlib のアップデートが毎月来るが，そのたびに破壊的変更が結構入るので，証明を保守するために自動更新ツールが欲しくなる
ところでこれに関しては，既に「更新があったら更新をお知らせして，問題がなければ PR も出す」という GitHub Action ができました．私も開発にちょっと関わってます．
これだけでも複数の Lean プロジェクトの保守が多少楽になりましたし，ちょっと前進といったところです．
