急にモチベが再燃してきて進めていた，Lean 4 版の Natural Number Game が終わりました．
（Natural Number Game とは，Lean という定理証明ができるプログラミング言語の使い方が学べる，ブラウザゲームです）
https://adam.math.hhu.de/#/g/hhu-adam/NNG4
楽しかったんですが，ちょっと人には勧めにくいかもしれません．
UI に未実装の部分があって，タクティックや補題の内容を見ようとしても missing としか表示されないことがある．VSCode を使わせてくれ～という気持ちになる．GitPod 等で代替できたらそちらのほうが実装も楽でいいかもしれない．
教育的な制限がかかっていて，未開放のタクティックを使用するとエラーにされてしまう．使える道具が少なすぎて面倒な手順を踏まないといけないため，「Lean は面倒なもの」という印象にならないか心配
数学にあまり慣れていない人だと，「ペアノの公理から整数の掛け算が可換であることを示す」というような課題の意味がわからないかもしれない．ますます「Lean を使っても面倒の末に虚無命題が示せるだけ」みたいな印象になってしまいそうで怖い．数学に慣れてる人でも，示している主張が地味なので物足りない感じがする
題材が圏論だったら，数学科のひとにもっと勧められたかもしれないですね．
もちろん良いところもありました：
Lean による定理証明の良いチュートリアルになっている．いきなり基礎になっている型理論を勉強したりすると大変．少しずつ無理なく使い方が覚えられるという点で，すごく良い
NNG4 は，Natural Number Game 以外の Lean Game を作るのにも使えるようになっていて，今後これをもとに新たなゲームが生まれるかもしれない．NNG4 を作ったのは偉業だと思う．
個人的にはNNG4は今後も Lean のチュートリアルとして使われ続けるだろう傑作だと思うのですが，代替となるチュートリアルがあるといいですね．
