私が Lean 言語の名前を知って勉強し始めたのは去年の8月くらいなので，勉強を始めて8カ月程度が経過したことになります．全然きりはよくないですが，振り返り記事を書こうと思います．
その間に私が達成できたことは，こんな感じです：
タクティク逆引きリスト
Lean と Mathlib にあるタクティク（定理証明を行うためのツール）が一覧できる資料を作りました．https://lean-ja.github.io/tactic-cheatsheet/
これは現在も開発中ですが，既にレファレンスとして十分な数のタクティクとコマンドを紹介できているかと思います．今後も Lean のアップデートは続くので，バージョン更新と新規機能の継続的な紹介が必要で，気が遠くなりそうですが頑張っていこうかと思います．
mdgen
Lean でコード例交じりの文章を書くためのツール mdgen を作ってリリースしました．
開発の背景を少し書きます．プログラミングに関するドキュメントを書くためのツールが，世の中には意外とありません．要件としては
- 何も設定しなくてもいい感じの見た目にしてほしい．特に，モバイル端末で見やすいことが必要．
- シンタックスハイライトが効くようにしてほしい．Lean のようなマイナー言語だとハイライトが効かないことがあるので，必要に応じて自分でカスタマイズできる必要もある．
- コード例が継続的にテストできるようになっていてほしい．そうでなければ，言語やライブラリのアップデートに追従することが難しく，短期間でゴミになってしまう．（私の経験上，本当に短期間でゴミになります）
- GitHub Pages で簡単に公開できてほしい．
などがあるのですが，すべてを満たすツールはそんなに多くありません．
私が知っている中でこの用途に最も適したツールは mdbook ですが，mdbook でさえ「コード例と本文を分けて管理する」必要があります．でもそれって面倒ですよね．本文とコード例はシームレスに読まれるのだから，書く時もシームレスであってほしいですね．
こういう面倒さを解消するために，lean2md という既存の Python スクリプトをもとに作ったのが mdgen というツールでした．（これは幸運なことに metaprogramming in lean で採用していただくことができました．）mdbook と mdgen を組み合わせることで，コード例と本文の同期問題は完全に解決します．Lean コードから md ファイルを生成できるので，生成された md ファイルを mdbook に食わせればいいだけになります．単純！
他の人が気軽に使えるように，mdbook と mdgen を組み合わせるテンプレートも作成しました．
https://github.com/Seasawher/lean-book
これは，コードブロックをクリックすると online playground へジャンプするなど，いろいろ便利機能を足してあります．早速使って不具合を報告してくださった方もいて感謝のいたりです．
Lean におけるドキュメント作成ツールとしては公式が作っている Verso があって，私はそれにも期待していますがまだ公開されただけで安定リリースには至っていないようですね．
lean-ja のコミュニティ規模
lean-ja というLeanのユーザコミュニティを共同で立ち上げました．Discord サーバがあるのですが，現在 36 人が入ってくださっていて，設立当初は 4 人くらいだったのを考えると 9 倍に成長したことになります．
一方で私の大目標は「Lean を数学科の全員が知っているプログラミング言語にする」ことです．まだまだ達成までは遠いですが，小さい目標に分割することはできます．
現状の目標としては，まずはLeanのユーザを増やさないと話にならないので増やしたいです．Lean が取り込めそうなユーザには以下の層があります：
- 数学科の人で，数学と計算の関わりに興味がある人
- 関数型言語や型理論に興味があるひとたち
Lean で数値計算ができるようになればもっと多くの層が取り込めることが期待できるのですが，現状では難しそうです．数学科の人向けの日本語の Lean の教材は mizuno yuma さんと enomoto haruhisa さんが作成された「数学系のための Lean 勉強会」のリポジトリが既にあるので，関数型プログラミングを Lean で学ぶ日本語の教材があるとよいかもしれないなと思っています．Haskell より Lean はずっとオシャレなので，Haskellのシェアを奪える可能性はあるかなと．
また，タクティクの一覧は作りましたが基本的な構文の一覧は作っていないので，それも作りたいと思っています．それが軌道に乗れば，とりあえず Lean に関する早見表的な資料の潜在的な需要は全部拾えるんじゃないかなと思っています．
また，Haskell と Julia の勉強をちゃんとやった方がいいなと最近思っています．関数型プログラミングにせよ数値計算にせよ，既存のツールのことがわかっていないと何もできない気がするので．
そういう感じです．また「これは進捗だな」と思うことがあったら記事にするかもしれません．
