Mathematics in Lean4の数論の章の３つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として３つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して…