← Contents

The Cube-Root Trick

Described, implemented in Lean, visualised, and proved correct. repo

1 · What the trick does

That's the clip up top. What looks like a memory stunt is really just two fast lookups, and you'll have them yourself in a couple of minutes. The part that's fun for us comes after the trick: proving it never once gets the answer wrong.

Here's the game. Someone takes a whole number from 1 to 99, cubes it, and reads you the result — a perfect cube of up to six digits, say 157464. You name the root. Since the root has at most two digits, there are only two things to find: its units digit and its tens digit, and each takes one glance.

The units digit. Look at the last digit of the cube. Cubing does something very tidy to units digits — it just permutes them:

Every column is different, so the bottom row can be read backwards without ambiguity. And you barely have to memorise it: six digits (0, 1, 4, 5, 6, 9) are fixed — the cube ends in the same digit the root does — and the other four are just two swaps, 2 ↔ 8 and 3 ↔ 7. So a cube ending in 4 has a root ending in 4; a cube ending in 3 has a root ending in 7.

The tens digit. Cross off the last three digits of the cube and look at what's left. Find the largest digit d whose cube fits inside it. That d is the tens digit.

Why the last three? Because the tens digit a of the root contributes a × 10, and (10a + b)³ = 1000·a³ + (smaller terms). Dividing the cube by 1000 — i.e. dropping three digits — leaves a number whose own "how many whole cubes fit?" answer is exactly a.

• Units: 157464 ends in 4 → root ends in 4 (a fixed digit).
• Tens: drop the last three → 157. The largest cube that fits is 5³ = 125 (since 125 ≤ 157 < 216 = 6³) → tens digit 5.
• Read them off: 54 = 54. And indeed 54³ = 157464.

2 · The implementation, in Lean

Two tiny pieces, mirroring the two glances: a units-digit lookup, and a descending search for the tens digit — the same shape as the trial-digit search from the division chapter, but comparing cubes.

3 · See it run — two glances

Enter a perfect cube — say 157464, which is 54³ — and the trick pulls its root back out. Step through the two lookups: the units digit comes straight off the table, and the tens digit falls out of the descending cube search. A number that isn't a cube of some 1–99 gets a polite refusal, since the trick doesn't apply to it.

4 · Before the proof — think like a verifier

You know the routine by now: before reading the proof, try to predict its shape. What must the statement assume? Why is each of the two glances sound? And the interesting one here — what are the two quite different ways you could prove a trick like this?

What should the theorem say?

Why the units lookup is safe

The trick reads the root's units digit off the cube's units digit. What makes that reading unambiguous?

Two roads to a proof

The claim covers only the numbers 1–99. What proof strategy does that finiteness unlock — and what does it cost?

5 · The formal Lean proof

Each module below leads with the argument in plain English — what it claims and why it is true — and folds the machine-checked Lean underneath. Read the reasoning first; open a proof only when you want to see how the idea is spelled out for the kernel. The chapter shows two roads: a lazy proof that just checks all hundred cases, and an honest chain that proves why each glance recovers its digit, never mentioning a specific number.

6 · Test the ideas

Reading a cube backwards

A perfect cube (root 1–99) ends in 2. What does its root end in?

Why cubes and not squares?

The units trick works for cube roots. Why wouldn't the same idea recover a square root's units digit?

Why drop exactly three digits?

Why search down from 9?

findCubeTensHelper counts down from 9 rather than up from 0. Why that direction?

What native_decide is trusting

The brute-force proof closes each of the 100 cases with native_decide rather than decide. Why?

Where the two lemmas meet

In the structural proof, cubeUnitsDigit_inverts gives one number and cubeTensDigit_eq gives another. How do they combine into the root?

How the tens search is pinned

The structural proof shows the tens search returns exactly the right digit a. What forces that?

Predict the trick

Run the trick on 1728. What root does it give?

7 · Write some Lean

A worksheet. Each cell has a starting goal with a gap for you to fill. Press Run (or Ctrl+Enter in the cell) and Lean compiles your code on the server. Run all checks every cell in turn, Reset all restores the blank cells, and every cell hides a reference solution you can reveal once you've tried. (Requires the checker server — see web/checker/README.md. In the listings digit literals may be shown as ⟨3,_⟩; the server spells them ⟨3, by omega⟩. The first run is slow: Lean is cold-loading Mathlib.)

The real, machine-checked proofs are exactly those in §5 — clone the repo and run them in VS Code.