Lean のコード生成に関しては、GitHub Copilot の補完AIやエージェントはほとんど役に立ちません（むしろ、邪魔しやがる）。コーディングAIの利用は現実的でないので諦めました。とはいえ、Lean の複雑な言語仕様や巨大な Mathlib ライブラリを理解・把握で…