Mathematics in Lean 4も最後の方に辿り着きつつあります。これから数回にわたってLean4による解析学の証明を見ていきます。Mathematics In Lean 4の章立てで言えば10.1 Filtersあたりなのですが、そこでの扱いはもっとはるかに抽象的です。この記事では具体例を中心に説明します。 まずは極限ですよね。普通の数学では$\varepsilon - \delta$論法が証明の中心です。一方Lean 4では定義域や値域での極限操作をフィルタという概念で統一的に表現しています。フィルタの概念のレベルで証明が完結する場合もあれば、それを不等式や集合に展開して個別のケ…