Coqというのは定理証明支援系。数学の証明を形式的にチェックしてくれるツールだ。 数学書を漫然と眺めていても仕方ないので，Coqのコードに書きなおしながら読めばいいんじゃないか，と思いついた。「演習 群・環・体 入門」は，本来整数の代数的定義がこの…

試しに難易度をHardにしてみた。が，とてもHardな感じではない。これは普通にAIにお願いして「TOEIC 800 Levelの問題を作ってください」とかやった方がいいな。必須単語は肩慣らし用に作られているとみた。

Finger Drum:Swing(Grade5) シンプルなんだけどなー。Swingだから，perfectを狙おうとすると難しい。途中からゲシュタルト崩壊してくる。なんでJazz playerたちはあのリズムで延々できるのか，というと，やはり身体にしみこんでるんだろうな。