The Missing Square

Cut a 64-square into four pieces. Rearrange them into a rectangle. Count again: 65. One square has come from nowhere — so where is it?

Below is an 8×8 board — 64 unit squares, you can count them. It is cut into four pieces: two triangles and two trapezoids, with edges of length 3, 5, 8 and 13 — consecutive Fibonacci numbers. Slide the control, and the four pieces rearrange into a 5×13 rectangle. A 5×13 rectangle has area 65. The same four pieces. One more square.

The trick survives slow motion. The pieces don't stretch, don't overlap, don't leave a visible hole — and yet 64 of something has become 65 of the same something. Both of those statements feel airtight, and they cannot both be true. Press Show the gap, finish the rearrangement, and look along the rectangle's diagonal.

The square didn't vanish — it spread out

The pieces almost meet along the rectangle's diagonal, but not quite. What looks like one straight cut is really two edges with slightly different slopes, and between them lies a long, impossibly thin parallelogram — a sliver of area exactly 1. That sliver is the missing square. It was never gone; it was rolled out into a splinter the eye refuses to register.

It's not a coincidence. It's Cassini's identity.

Why those numbers — 3, 5, 8, 13? Take any three consecutive Fibonacci numbers. The square is F(n)×F(n); the rectangle is F(n−1)×F(n+1). The difference between their areas is governed by a 1680 identity of Cassini:

Move n and watch the same paradox at every scale. Even n: the rectangle gains a unit (a gap). Odd n: the pieces overlap instead, and the rectangle loses a unit. And as n grows, the consecutive ratios race toward the golden ratio φ = 1.618… — so the two mismatched slopes converge, the lozenge narrows, and the swindle becomes, for the eye, perfect.

Checked by the kernel

That the discrepancy is always ±1 — for every n at once, not just the cases drawn here — is not something a picture can establish. So it is proved, and the proof is checked by machine. Cassini's identity is stated in Lean 4 and verified by its kernel, with zero imports: no library is trusted, every step is reduced to the type-checker itself.

Lean 4.31 · no sorry · axioms [propext, Quot.sound]

-- research/the-missing-square/lean/Cassini.lean  (zero imports)
theorem cassini : ∀ n, fib (n+1) * fib (n+1) - fib n * fib (n+2) = alt n
-- the area gap, for every n. And the load-bearing corollary:
theorem cassini_ne_zero (n : Nat) :
    fib (n+1) * fib (n+1) - fib n * fib (n+2) ≠ 0   -- never reconciles

'Cassini.cassini' depends on axioms: [propext, Quot.sound]
'Cassini.cassini_ne_zero' depends on axioms: [propext, Quot.sound]
'Cassini.chessboard_gap' does not depend on any axioms  -- 5·13 − 8² = 1

The alternating sign (−1)ⁿ is given its own definition so the proof needs no library lemma about exponents; the whole-number algebra is core Int rewriting plus omega. Read it: Cassini.lean · verify: verify.sh. This joins the Wasteland's other machine-checked strata — the irrationality of every non-square root and why the pentagon can't tile, where the same golden-ratio wall (5 is not a perfect square) does its other day-job.

Who found it, and what we don't know

The honest apparatus — every claim with its source, every uncertainty named rather than smoothed over.

Sources, in full: Singmaster, Sources in Recreational Mathematics §6.P.1; T. Sillke, "Jigsaw Paradox"; G. Frederickson, Dissections: Plane & Fancy (1997), ch. 23; T. Koshy, Fibonacci and Lucas Numbers with Applications (2001); Wikipedia "Chessboard paradox" and "Cassini and Catalan identities"; Wolfram MathWorld; cut-the-knot.