現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が１つヒットしました！ A slightly longer Lean 4 proof tour | What's new 実数の２つの無限数列に関するある補題の証明をLean4を使って形式化して確認する、というものです。証明自体は望遠鏡和(telescoping sum)という手法を使ったものです。有限和をうまく作ると、実は隣り合った項が打ち消しあって最初と最後の項だけが…
