テレンスタオ教授の数学ブログ Lean4 の証明解説

現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。

残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が１つヒットしました！

実数の２つの無限数列に関するある補題の証明をLean4を使って形式化して確認する、というものです。証明自体は望遠鏡和(telescoping sum)という手法を使ったものです。有限和をうまく作ると、実は隣り合った項が打ち消しあって最初と最後の項だけが残る、というやつです。

昨年の12月初旬にある人がX(旧twitter)でこの補題の50行のLean4証明とともに、これをもっと短く証明できないか、というポストがありました。それにタオ教授が反応してX上で3行の証明をポストしました。それからしばらくしてブログの中で上記の記事で10行のLean4証明がポストされました。

タオ教授のブログ記事の目的は、タオ教授がこの補題の証明で肝だと思う部分を明確にするため、及びその証明の肝がLean4による形式化でも明確にわかるようにする、ということのように思います。さらにLean4をどのように使えば良いかのレッスンにもなっていてとても勉強になりました。

以下に私が得たポイントを作業手順的に書いてみます。

まずちゃんと人間が読める普通の証明を青写真(blueprint)として書き下します。青写真なので細かいところまで詰めてなくても良さそうです。
次に定理を形式化します。これで証明に必要な言葉がLean4で表現されました。例えばここでは非増加数列が必要なのですがmathlibですでにAntitoneという性質が定義されていてそれを使ったそうです。既存の定義が使えれば既証明の多くの定理が活用できるのでとても重要なのだそうです。
青写真に従って証明の流れ(構造)を書きます。
この証明では不等式の連鎖で証明するので、calcを使うのですが、calcの中での不等式の連鎖を書き下します。各ステップの証明はとりあえずsorryで済ませておきます。calcを使わない場合も、適当な中間的補題をhaveタクティク（証明はsorry）で書けば良いと思います。
各ステップ、中間補題をsorryから証明に書き換えていきます。
各ステップについてタクティクの選択、検索(!)、適用の解説があります。望遠鏡和そのものがmathlibに入っていて、それをexact?という検索コマンドで見つけて適用する、など実践的な活用が書かれていて面白いです。