Variables and algebraic expressions

Amara in Lagos, Kenji in Osaka and Lucía in Bogotá are building a row of squares out of matchsticks. Neighbouring squares share a side.

How many sticks does a row of $n$ squares need? Each of them finds a rule:

• Amara: "Start with one stick on the left. Every square then adds 3 sticks." That gives $3n + 1$.
• Kenji: "The first square needs 4. Each of the other $n - 1$ squares needs 3." That gives $4 + 3(n - 1)$.
• Lucía: "Every square has 4 sides, but $n - 1$ sides are shared and were counted twice." That gives $4n - (n - 1)$.

They try $n = 1, 2, 3, 4, 5$ and get $4, 7, 10, 13, 16$ every time. Are the three rules always the same — for a row of a thousand squares, or a million? Trying values cannot settle that, because there are infinitely many values to try. In this lesson we learn the language that lets us answer such questions once and for all: variables and algebraic expressions.

In $3n + 1$, the letter $n$ is a variable: a name for a number that we have not fixed. It is like the box in $3 \times \square + 1$ from your work on expressions and unknowns, except that a letter can appear several times and always means the same number each time it appears.

An expression such as $3n + 1$ is a recipe: give it a number, follow the instructions, and a number comes out. Putting a number in place of the variable is called substituting or evaluating.

We write products without a dot: $3n$ means $3 \cdot n$, and $ab$ means $a \cdot b$.

Every rule for rearranging expressions comes from a few basic laws of arithmetic, which hold for all numbers: commutativity ($ab = ba$, $a + b = b + a$), associativity, and the distributive law $a(b + c) = ab + ac$. Because the laws hold for every number, anything we derive from them holds for every number too. That is how we can answer a question about infinitely many values in a few lines.

So Amara, Kenji and Lucía will agree for every row of squares there could ever be. Notice what the proof did not do: it did not try any values.

The theorem tells us exactly how wrong the tempting rule $(a + b)^2 = a^2 + b^2$ is: it leaves out $2ab$. So the tempting rule gives the right answer only when $2ab = 0$.

The same kind of argument shows exactly when $2x$ and $x^2$ — two expressions that are often confused — take the same value.

Powers are shorthand for repeated multiplication: $2^5 = 2 \cdot 2 \cdot 2 \cdot 2 \cdot 2 = 32$. Counting factors gives three laws.

Why $a^0 = 1$? The laws above were proved for exponents $1, 2, 3, \dots$. If we want the first law to keep working when an exponent is $0$, then $a^1 \cdot a^0 = a^{1+0} = a^1$, so $a \cdot a^0 = a$. For $a \neq 0$ we can divide both sides by $a$, and the only possible value is $a^0 = 1$. So $a^0 = 1$ is not an arbitrary rule: it is the only choice that keeps the laws true.

Testing values is a good way to check algebra, and it is all you need to show that two expressions are not equivalent: one counterexample is enough. But passing tests can never prove an equivalence on its own. Here is a striking example.

Someone who tested only $0, 1, 2, 3$ would be fooled. By changing the factors, you can build two expressions that agree on a thousand test values and still differ at the next one.

In Lean, a variable is exactly what it is on paper: a name for an arbitrary number. A statement with (n : Int) among its inputs claims something for every integer at once — which is precisely what "equivalent expressions" means.

First, combining like terms, which is the distributive law read backwards. This one just applies core Lean's law Int.add_mul:

/-- Combining like terms: `a·x + b·x = (a + b)·x` for all integers. This is the distributive
law read from right to left; the proof applies core Lean's `Int.add_mul`. -/
theorem like_terms (a b x : Int) : a * x + b * x = (a + b) * x :=
  (Int.add_mul a b x).symm

The three matchstick rules agree for every integer $n$:

/-- The matchstick pattern: a row of `n` squares needs `3n + 1` sticks. Two other ways of
counting give `4 + 3(n − 1)` ("first square, then 3 more each time") and `4n − (n − 1)`
("4 per square, minus the shared sides"). All three expressions are equivalent: they agree for
*every* integer `n`, not just for the values we tried. -/
theorem stick_formulas_agree (n : Int) :
    4 + 3 * (n - 1) = 3 * n + 1 ∧ 4 * n - (n - 1) = 3 * n + 1 := by
  constructor
  · calc 4 + 3 * (n - 1) = 4 + (3 * n - 3 * 1) := by rw [Int.mul_sub]
      _ = 3 * n + 1 := by omega
  · omega

The square of a sum, by the distributive law twice — and then the square of a difference, obtained by putting $-b$ in place of $b$ (a variable may stand for a negative number):

/-- The square of a sum: `(a + b)² = a² + 2ab + b²`, proved by using the distributive law
twice, exactly as in the lesson:
`(a + b)(a + b) = a(a + b) + b(a + b) = (a² + ab) + (ba + b²)`, then collect like terms. -/
theorem square_of_sum (a b : Int) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 :=
  calc (a + b) ^ 2 = (a + b) * (a + b) := by
        rw [Int.pow_succ, Int.pow_succ, Int.pow_zero, Int.one_mul]
    _ = a * (a + b) + b * (a + b) := Int.add_mul a b (a + b)
    _ = (a * a + a * b) + (b * a + b * b) := by rw [Int.mul_add, Int.mul_add]
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by grind

/-- The square of a difference, `(a − b)² = a² − 2ab + b²`, obtained from `square_of_sum`
by putting `−b` in place of `b`: a variable can stand for *any* integer, negative ones
included. -/
theorem square_of_difference (a b : Int) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 :=
  calc (a - b) ^ 2 = (a + -b) ^ 2 := by rw [Int.sub_eq_add_neg]
    _ = a ^ 2 + 2 * a * -b + (-b) ^ 2 := square_of_sum a (-b)
    _ = a ^ 2 - 2 * a * b + b ^ 2 := by grind

A single counterexample refutes the tempting rule, and the next theorem says exactly when the tempting rule happens to give the right answer:

/-- `(a + b)² = a² + b²` is **not** an identity: one counterexample is enough to refute it.
With `a = b = 1` the left side is `4` and the right side is `2`. -/
theorem square_of_sum_counterexample : ¬ ∀ a b : Int, (a + b) ^ 2 = a ^ 2 + b ^ 2 := by
  intro h
  have h11 := h 1 1
  -- `h11 : (1 + 1) ^ 2 = 1 ^ 2 + 1 ^ 2`, i.e. `4 = 2`, which `decide` refutes.
  revert h11
  decide

/-- Exactly when does the tempting mistake give the right answer?
`(a + b)² = a² + b²` holds precisely when `a = 0` or `b = 0`. By `square_of_sum` the equation
says `2ab = 0`, so `ab = 0`, and a product of integers is `0` only if a factor is `0`
(`Int.mul_eq_zero`). -/
theorem square_of_sum_eq_iff (a b : Int) :
    (a + b) ^ 2 = a ^ 2 + b ^ 2 ↔ a = 0 ∨ b = 0 := by
  rw [square_of_sum]
  constructor
  · intro h
    have hab : a * b = 0 := by grind
    exact Int.mul_eq_zero.mp hab
  · rintro (rfl | rfl) <;> grind

/-- `2x` and `x²` are different expressions, but they *can* take equal values: exactly when
`x = 0` or `x = 2`. Proof: `2x = x²` means `x² − 2x = 0`, that is `x(x − 2) = 0`, and a product
is zero only if one factor is zero. -/
theorem two_mul_eq_sq_iff (x : Int) : 2 * x = x ^ 2 ↔ x = 0 ∨ x = 2 := by
  constructor
  · intro h
    have hfac : x * (x - 2) = 0 := by grind
    rcases Int.mul_eq_zero.mp hfac with h0 | h2
    · exact Or.inl h0
    · right; omega
  · rintro (rfl | rfl) <;> decide

Four passing tests, and still not equivalent:

/-- Testing can refute an equivalence but cannot prove it. The expressions
`x + x(x − 1)(x − 2)(x − 3)` and `x` agree for `x = 0, 1, 2, 3` — four successful tests — yet
they are not equivalent, because at `x = 4` the first is `28`. -/
theorem few_tests_mislead :
    (∀ x : Int, 0 ≤ x → x ≤ 3 → x + x * (x - 1) * (x - 2) * (x - 3) = x) ∧
      (4 : Int) + 4 * (4 - 1) * (4 - 2) * (4 - 3) ≠ 4 := by
  constructor
  · intro x h0 h3
    have hx : x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 := by omega
    rcases hx with rfl | rfl | rfl | rfl <;> decide
  · decide

Lean defines powers just as we did: $a^0 = 1$ and $a^{n+1} = a^n \cdot a$. So the laws of exponents are proved by induction: check the law when the exponent is $0$, then show that whenever it holds for an exponent $k$ it also holds for $k + 1$. Like a row of dominoes, that reaches every whole number. This is the precise version of "count the factors".

/-- `aᵐ · aⁿ = aᵐ⁺ⁿ`: `m` factors of `a` followed by `n` more make `m + n` factors.
Proof by induction on `n`, using associativity of multiplication for the step. -/
theorem pow_add_law (a : Int) (m n : Nat) : a ^ m * a ^ n = a ^ (m + n) := by
  induction n with
  | zero => rw [Int.pow_zero, Int.mul_one, Nat.add_zero]
  | succ k ih =>
    calc a ^ m * a ^ (k + 1) = a ^ m * (a ^ k * a) := by rw [Int.pow_succ]
      _ = (a ^ m * a ^ k) * a := (Int.mul_assoc _ _ _).symm
      _ = a ^ (m + k) * a := by rw [ih]
      _ = a ^ (m + (k + 1)) := by rw [← Nat.add_assoc, Int.pow_succ]

/-- `(aᵐ)ⁿ = aᵐⁿ`: `n` blocks of `m` factors each make `m·n` factors.
Proof by induction on `n`, using `pow_add_law` for the step. -/
theorem pow_mul_law (a : Int) (m n : Nat) : (a ^ m) ^ n = a ^ (m * n) := by
  induction n with
  | zero => rw [Int.pow_zero, Nat.mul_zero, Int.pow_zero]
  | succ k ih =>
    calc (a ^ m) ^ (k + 1) = (a ^ m) ^ k * a ^ m := Int.pow_succ _ _
      _ = a ^ (m * k) * a ^ m := by rw [ih]
      _ = a ^ (m * k + m) := pow_add_law a (m * k) m
      _ = a ^ (m * (k + 1)) := by rw [Nat.mul_succ]

/-- `(ab)ⁿ = aⁿbⁿ`: regroup the factors `ab · ab ⋯ ab` as `a ⋯ a · b ⋯ b`. The regrouping
uses commutativity, which is why this law fails for operations that do not commute (such as
matrix multiplication, later). Proof by induction on `n`. -/
theorem mul_pow_law (a b : Int) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
  induction n with
  | zero => rw [Int.pow_zero, Int.pow_zero, Int.pow_zero, Int.mul_one]
  | succ k ih =>
    calc (a * b) ^ (k + 1) = (a * b) ^ k * (a * b) := Int.pow_succ _ _
      _ = (a ^ k * b ^ k) * (a * b) := by rw [ih]
      _ = (a ^ k * a) * (b ^ k * b) := by grind
      _ = a ^ (k + 1) * b ^ (k + 1) := by rw [Int.pow_succ, Int.pow_succ]

Core Lean also has the first law in its library, so a one-line proof is possible. Both versions are machine-checked; the difference is honesty about who did the work — pow_add_law proves it here, pow_add_library relies on core Lean's Int.pow_add.

/-- The same law, by applying core Lean's `Int.pow_add` (which states it the other way
round). Compare `pow_add_law`, which proves it here by induction. -/
theorem pow_add_library (a : Int) (m n : Nat) : a ^ m * a ^ n = a ^ (m + n) :=
  (Int.pow_add a m n).symm

Finally, the argument that $a^0$ has no choice but to be $1$:

/-- Why `a⁰ = 1`: if the law `a¹ · a⁰ = a¹⁺⁰ = a¹` is to hold, then for `a ≠ 0` the number
`a⁰` must be a `z` with `a · z = a`, and the only such `z` is `1` (cancel the non-zero
factor `a`, using `Int.eq_of_mul_eq_mul_left`). So the definition `a⁰ = 1` is not arbitrary:
it is the only choice that keeps the exponent laws true. -/
theorem pow_zero_forced (a z : Int) (ha : a ≠ 0) (h : a * z = a) : z = 1 := by
  have h' : a * z = a * 1 := by rw [Int.mul_one]; exact h
  exact Int.eq_of_mul_eq_mul_left ha h'

What is formalised here: every identity and law in this lesson for the integers. The same proofs work for rational numbers, because they use only the laws of arithmetic; Mathlib proves them once for every commutative ring (add_sq, pow_add, pow_mul, mul_pow).

"""Are two expressions equivalent? Testing, refuting and expanding.

Two expressions are equivalent when they agree for EVERY value of their
variables. This experiment (1) tests several pairs of expressions on a block
of integer values, reporting the first counterexample if there is one;
(2) shows how a pair can pass four tests in a row and still be different;
(3) counts exactly, on a finite grid, how often the false rule
(a + b)^2 = a^2 + b^2 happens to give the right answer; and (4) asks SymPy to
expand the difference of each pair. Tests can refute an equivalence with one
counterexample; passing tests is evidence only. The symbolic expansion is a
genuine verification for polynomials, as trustworthy as SymPy's
implementation of the laws of algebra.
"""

import sympy

a, b, n, x = sympy.symbols("a b n x")

#: (name, left expression, right expression) - each pair is tested below.
PAIRS = [
    ("4 + 3(n - 1)  vs  3n + 1", 4 + 3 * (n - 1), 3 * n + 1),
    ("4n - (n - 1)  vs  3n + 1", 4 * n - (n - 1), 3 * n + 1),
    ("(a + b)^2  vs  a^2 + b^2", (a + b) ** 2, a ** 2 + b ** 2),
    ("(a + b)^2  vs  a^2 + 2ab + b^2", (a + b) ** 2, a ** 2 + 2 * a * b + b ** 2),
    ("2x  vs  x^2", 2 * x, x ** 2),
]

#: The pair that agrees at x = 0, 1, 2, 3 but is not equivalent.
TRAP = (x + x * (x - 1) * (x - 2) * (x - 3), x)

def value(expr, assignment):
    """Exact value of a SymPy expression for a dict {symbol: integer}."""
    return int(expr.subs(assignment))

def ordered_values(radius):
    """The integers -radius..radius in the order 0, 1, -1, 2, -2, ..."""
    if radius < 0:
        raise ValueError("radius must be non-negative")
    out = [0]
    for k in range(1, radius + 1):
        out += [k, -k]
    return out

def assignments(variables, radius):
    """All ways to give each variable a value in -radius..radius.

    The variables are taken in alphabetical order and the values in the
    order of ``ordered_values``, so small values are tried first.
    """
    out = [{}]
    for var in sorted(variables, key=str):
        out = [{**d, var: k} for d in out for k in ordered_values(radius)]
    return out

def first_counterexample(lhs, rhs, radius):
    """Return (tests run, first assignment where lhs != rhs, or None)."""
    variables = lhs.free_symbols | rhs.free_symbols
    tests = assignments(variables, radius)
    for k, assignment in enumerate(tests, start=1):
        if value(lhs, assignment) != value(rhs, assignment):
            return k, assignment
    return len(tests), None

def symbolic_difference(lhs, rhs):
    """SymPy's expansion of lhs - rhs (0 exactly when they are identical)."""
    return sympy.expand(lhs - rhs)

def agreement_count(radius):
    """Count grid points (a, b) in -radius..radius where (a+b)^2 = a^2 + b^2.

    Uses plain integer arithmetic. By the lesson's theorem this happens
    exactly when a = 0 or b = 0, i.e. at 2(2r + 1) - 1 points.
    """
    values = range(-radius, radius + 1)
    hits = sum(1 for p in values for q in values
               if (p + q) ** 2 == p ** 2 + q ** 2)
    return hits, len(values) ** 2

def describe(assignment):
    """Readable form of an assignment such as 'a = -3, b = -3'."""
    return ", ".join(f"{k} = {v}" for k, v in
                     sorted(assignment.items(), key=lambda kv: str(kv[0])))

def main():
    print("1. Testing pairs on the values 0, 1, -1, 2, -2, 3, -3 until one fails")
    for name, lhs, rhs in PAIRS:
        tests, bad = first_counterexample(lhs, rhs, 3)
        verdict = "all agree" if bad is None else "differ at " + describe(bad)
        print(f"   {name:<31} {tests:>2} test(s): {verdict}")
    print()
    print("2. A pair that passes four tests:  x + x(x-1)(x-2)(x-3)  vs  x")
    lhs, rhs = TRAP
    for k in range(6):
        left, right = value(lhs, {x: k}), value(rhs, {x: k})
        mark = "agree" if left == right else "DIFFER"
        print(f"   x = {k}:  {left:>4}  vs  {right}   {mark}")
    print()
    hits, total = agreement_count(100)
    print("3. (a + b)^2 = a^2 + b^2 on the grid -100..100 (every point checked):")
    print(f"   true at {hits} of {total} points ({100 * hits / total:.2f}%),")
    print("   exactly the points where a = 0 or b = 0.")
    print()
    print("4. SymPy expands  left - right  (0 means identical polynomials)")
    for name, lhs, rhs in PAIRS + [("x + x(x-1)(x-2)(x-3)  vs  x", *TRAP)]:
        diff = str(symbolic_difference(lhs, rhs)).replace("**", "^")
        print(f"   {name:<31} {diff}")
    print()
    print("Epistemic status: parts 1 and 2 are finite tests - a single")
    print("counterexample refutes an equivalence, but passing tests proves")
    print("nothing (part 2 passes four in a row). Part 3 is an exhaustive count")
    print("over a finite grid only. Part 4 is a symbolic verification for these")
    print("polynomials, as reliable as SymPy's built-in algebra; the lesson's")
    print("proofs from the distributive law explain why the identities hold.")

if __name__ == "__main__":
    main()

Read the output carefully. The tests catch the false square rule after nine tries — but the trap expression in part 2 sails through four tests. Part 3 checks every point of a finite grid: the false rule is right less than 1% of the time, at exactly the points our theorem predicts. Part 4 is different in kind. SymPy rewrites $\text{left} - \text{right}$ into a standard form using the laws of algebra, so a result of $0$ is a check of the identity for all values — as reliable as SymPy's own implementation of those laws. The difference $x^4 - 6x^3 + 11x^2 - 6x$ in the last line is $x(x - 1)(x - 2)(x - 3)$, which is zero at $0, 1, 2, 3$ and nowhere else.

Graphing turns "do these expressions agree?" into "where do these curves meet?". Equivalent expressions have the same graph; different expressions can still cross at a few points.

Things to try:

• In the second plot, set $k = 0$: the curves coincide. For any other $k$ they meet only at $x = 0$, and the vertical gap between them at $x$ is exactly $2kx$.
• Use the trace slider on the third plot just past $x = 3$ and watch the curves separate.
• Open "Edit the functions" and graph $4 + 3(x - 1)$ and $3x + 1$. Why can you see only one line?

Clock arithmetic is a whole world where the rules of algebra still work — with surprises like the one in the algebra viewpoint above.

• Around the 3rd century CE, Diophantus of Alexandria wrote his Arithmetica with a special abbreviation for the unknown number and for its powers — a step from writing algebra in full sentences towards symbols.
• In India, mathematicians from Brahmagupta (Brāhmasphuṭasiddhānta, 628 CE) onwards handled several unknowns at once, naming the first yāvat-tāvat ("as much as") and further ones after colours such as kālaka ("black") and nīlaka ("blue"); Bhāskara II's Bījagaṇita (1150) writes them with abbreviated syllables.
• In Baghdad around 820 CE, Muḥammad ibn Mūsā al-Khwārizmī called the unknown shayʾ, "thing", and wrote all his algebra in words. The word algebra comes from the al-jabr in the title of his book.
• In China, Li Ye (Ceyuan haijing, 1248) and Zhu Shijie (1303) wrote polynomials with the tiān yuán ("celestial element") method: a column of counting-rod numerals in which the position of each coefficient showed the power of the unknown.
• In France, François Viète (1591) used letters both for unknowns (vowels) and for known quantities (consonants), so that one calculation solved a whole family of problems. René Descartes' La Géométrie (1637) introduced the convention we still use — $x, y, z$ for unknowns, $a, b, c$ for known quantities — and raised exponents such as $x^3$.

• I. M. Gelfand and A. Shen, Algebra (1993) — a beautiful, problem-driven introduction, including the square of a sum and the laws of exponents.
• W. W. Sawyer, Vision in Elementary Mathematics (1964) — algebra through pictures and patterns, including area models.
• Richard Rusczyk, David Patrick and Ravi Boppana, Prealgebra (2011) — careful practice with expressions, written for curious students.
• Victor J. Katz, A History of Mathematics: An Introduction (3rd edition, 2009) — the story of algebraic notation in many civilisations.