Classic mathematics

The binomial theorem: squares

Expand a square and a cube. Lean’s core grind tactic normalizes polynomial expressions.

-- Top 100 #44: The binomial theorem: squares
-- History: 1665 · Newton’s generalized expansion.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The coefficient 2 counts the two cross terms ab and ba.
-- Scope: Proves the square and cube expansions for all integers. Arbitrary exponents and generalized infinite expansions are outside this file.
-- Source: https://lurch.plus/100/

theorem binomial_square (a b : Int) :
    (a+b)^2 = a^2 + 2*a*b + b^2 := by
  grind

theorem binomial_cube (a b : Int) :
    (a+b)^3 = a^3 + 3*a^2*b + 3*a*b^2 + b^3 := by
  grind

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.

`grind`

Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.

`Int`

Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.

Background and proof scope

1665 · Newton’s generalized expansion

The coefficient 2 counts the two cross terms ab and ba.

Proves the square and cube expansions for all integers. Arbitrary exponents and generalized infinite expansions are outside this file.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

File checked successfully.

Exercise

Write the fourth-power expansion. Try a wrong coefficient and inspect Lean’s feedback.