遅ればせながら、Antigravityで初めてAIエージェントを試しました。
便利ですね。
パーサをちょっと書いてもらって「こりゃすごい！」と思ったのですが、すぐクォータが切れて2週間待てと…
流石にこれでは使い物にならないので、VSCodeの拡張Clineを導入しました。
サブスクは好きじゃないので、従量課金にすべくGemini API。
(余談ですが、最近までGeminiで満足していたのですが、あっちこっちあれがいいこれがいいという話を聞くとGeminiもひとつかな？という気分になったので、AIの評価というのは難しいものですね)
で、エージェントで何をしようかなと思ったのですが、やっぱりこれを機会に数学かと。
数学はついに、AIというツルハシで挑める金鉱という時代になりました。
なので、Leanを1行も書いたことがないLean使いになろうかと。
難しい現代数学よりオイラー辺りのほうが好きなのでその辺から遊ぼうかな。
追記。
n^2が偶数ならnも偶数の証明に$0.5かかりました。(無料枠も使ったから実際にはもっと？)
そして…できたコードがよくわからない🤪
