2024年11月から進められてきた AtCoder の言語処理系の更新作業が一段落つき、 いよいよ AtCoder Daily Training での先行運用が始まりました。 今回の更新ではなんと定理証明支援系である Lean が追加される予定です。 そこで、とりあえず証明は抜きに Lean でのプログラムの書き方を確認しつつ、問題を解いていきます。

色々な人がCTF初心者におすすめと紹介していて気になっていたångstromCTF 2023に参加しました。

Diff Adjacent (AtCoder Beginner Contest 297 Ex)の解法を説明します。 同じ解法の解説はすでにありますが、この記事では立式パートを詳しめに書いています。