本稿では、Markovianサンプルを用いたQ学習および線形時間的差分（TD）学習のほぼ確実な収束を、Mathlibライブラリに基づいたLean 4定理証明器を用いて形式化します。Q学習と線形TDは、初期の重要な強化学習（RL）アルゴリズムの1つであり、その収束特性の研究は初期のRL分野の主要な研究テーマでした。本研究は、Robbins-Siegmund定理に基づく統一的な枠組みの中で、これらのアルゴリズムのほぼ確実な収束を正式に検証します。さらに、この枠組みは収束速度や他の収束モードに簡単に拡張可能であり、収束するRL結果の完全な形式化に向けた重要な一歩といえます。