Awesome. I've been looking for more Lean resources outside of Theorem Proving in Lean [1].
A series of levels where you prove ever-more-complex theorems in Lean, gaining each proved theorem as a tool to use in proving further theorems! Best puzzle game I've played in years.