Classic mathematics

Heron’s formula: a 3–4–5 triangle

Avoid floating-point square roots: verify the squared area with exact natural-number arithmetic.

-- Top 100 #57: Heron’s formula: a 3–4–5 triangle
-- History: c. 75 CE · Heron of Alexandria.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: For sides 3,4,5 the semiperimeter is 6, and the area is also 6.
-- Scope: Checks Heron’s squared-area expression for the 3–4–5 triangle. The geometric formula for arbitrary triangles is not derived.
-- Source: https://lurch.plus/100/

def heronSquared (a b c : Nat) : Nat :=
  let s := (a+b+c)/2
  s*(s-a)*(s-b)*(s-c)

example : heronSquared 3 4 5 = 6^2 := by decide
example : 3*4 = 2*6 := by decide

-- Nat division truncates. Restrict this helper to even perimeters
-- and valid triangles; it is not a general real-valued area function.
#eval heronSquared 3 4 5

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

c. 75 CE · Heron of Alexandria

For sides 3,4,5 the semiperimeter is 6, and the area is also 6.

Checks Heron’s squared-area expression for the 3–4–5 triangle. The geometric formula for arbitrary triangles is not derived.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

Exercise

Check the 5–12–13 triangle: its area is 30.