Number theory

Four squares: find a witness

Build a search program, then supply an explicit witness that Lean checks independently.

-- Top 100 #19: Four squares: find a witness
-- History: 1770 · Lagrange.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Zero is allowed as a square, so “four” includes sums needing fewer terms.
-- Scope: Proves an explicit four-square representation of 30 and runs a witness search. It does not prove existence for every natural number.
-- Source: https://lurch.plus/100/

def fourSquares (n : Nat) : Option (Nat × Nat × Nat × Nat) := do
  for a in List.range (n+1) do
    for b in List.range (a+1) do
      for c in List.range (b+1) do
        for d in List.range (c+1) do
          if a*a + b*b + c*c + d*d == n then
            return (a, b, c, d)
  none

theorem thirty_is_four_squares :
    ∃ a b c d : Nat, 30 = a*a + b*b + c*c + d*d := by
  exact ⟨4, 3, 2, 1, by decide⟩

def main : IO Unit := do
  match fourSquares 30 with
  | some (a,b,c,d) => IO.println s!"30 = {a}² + {b}² + {c}² + {d}²"
  | none => IO.println "No witness found"

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

1770 · Lagrange

Zero is allowed as a square, so “four” includes sums needing fewer terms.

Proves an explicit four-square representation of 30 and runs a witness search. It does not prove existence for every natural number.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

30 = 4² + 3² + 2² + 1²

Exercise

Search for a representation of 23, then write a separate theorem using its four witnesses.