Lean4はNixでも環境構築できる( https://leanprover.github.io/lean4/doc/setup/nix.html )という旨が書かれて入るが内容の通りかなり実験的な状態で，少なくともこれに書かれたテンプレートを用いると毎回最新のLean4をビルドする羽目になって大変なことになる気がする（lean-toolchainは無視される）のと，Lean側で依存しているライブラリ等もNIxで明示的に記載しなければならず二度手間になる上に場合に依っては出来ないケースもある（Mathlib4がそうでNix Flakeを提供していないため）#要調査

https://scrapbox.io/sno2wman/2023.07.26#64c0a27113a1580000c95a55