The Number With No Room Beneath It

Write it as 0.999… — a nine, then another, then nines forever. People feel sure it must fall a hair short of 1, leaving a sliver of room underneath. So go find that room: name a number that sits strictly between 0.999… and 1. The catch is that there isn't one, and the reason isn't a trick — it's that 0.999… and 1 are two names for the same number.

This page lets you try the impossible first, then shows you three different roads to why. Every number on it is recomputed in front of you with exact (whole-number ratio) arithmetic — nothing is rounded into agreeing.

Try it — find the gap

Type any number you believe is strictly between 0.999… and 1. Enter sends it.

Waiting for your number…

Whatever you enter, it lands in one of three places, never between: it's already 1 (an endpoint), it's above 1, or — if it's any finite decimal below 1 — some run of nines 0.99…9 already overtakes it, which means it sits below 0.999…, not inside a gap. Watch where your number falls on the line as you zoom in:

window: 0 … 1

The orange mark is your number; the bright tick on the right is 1, where 0.999… also lives. Keep zooming and the gap you're chasing keeps shrinking by a factor of ten — it never opens.

Three roads to the same place

Each is a real proof; press play and the numbers fill in.

The schoolroom one: multiply by ten algebra

Call the repeating decimal x. Shifting the decimal point one place (multiplying by 10) leaves an identical tail of nines — so subtracting cancels it completely.

Honest footnote: this works because 0.999… already names a real number (the limit below). It's a clean demonstration, and the rigorous proof is the third road.

The thirds: a fact you already trust fractions

You accept that one third written as a decimal is 0.333… forever. Multiply both sides by 3:

The verifier confirms 3 × (1/3) = 1 with exact ratios — the multiplication lands on 1 on the nose, never on a 0.999…9 that's secretly short.

The real reason: what an infinite decimal means limit

A decimal like 0.999… isn't an endless process that never arrives — it's a single number, defined as the limit its partial sums approach:

0.999… = 9⁄10 + 9⁄100 + 9⁄1000 + … = Σ 9·(1⁄10)ᵏ

Slide to add more nines. The partial sum is Sₙ = 1 − 1⁄10ⁿ, and the gap to 1 is exactly 1⁄10ⁿ — a real, positive sliver at every finite n. The infinite decimal is the place all these are heading:

n = 3

S₃ = 0.999

gap to 1 = 1⁄1000 = 0.001

The sliver never becomes zero at any finite n — and it never has to. The geometric series sums exactly: 9⁄10 ÷ (1 − 1⁄10) = 9⁄10 ÷ 9⁄10 = 1. The limit is the value, and the value is 1.

The check — show the working

The companion verifier recomputes every claim above in exact whole-number ratios (BigInt), so nothing rounds into agreement. 14 checks, all passing:

Source: research/does-point-nine-equal-one/verify.mjs. The on-page challenge uses the same overtaking rule (smallest n with 0.99…9 > your number), computed live with BigInt.

The check that doesn't stop

Read the first line of that list again: checked to n = 60. The claim is about every n, and a loop only ever reaches a finite one. Sixty stages of a statement about all of them is corroboration, not proof, and sixty was chosen because it looked like plenty.

That line is now settled by Lean's type checker instead, for every n at once, from a single identity proved with no imports at all (no library, nothing trusted but the kernel):

9 × (1 + 10 + 100 + … + 10n−1) + 1 = 10n

The left-hand product is the numerator of 0.99…9 with n nines, over the denominator 10n. The + 1 is the gap, and it is a 1 rather than a 0 at every n there will ever be. Divide through and you have the sentence the slider prints: the gap to 1 is exactly 1⁄10n. Regroup the very same line as 3 × (3 × repunit) + 1 and it is the thirds claim, which is why those two bullets were never independent facts.

The second half carries more weight, because "no finite run of nines ever arrives" is the argument for believing 0.999… falls short. What settles it the other way is that the gap is empty, and that is proved too: for every rational p⁄q below 1 there is a stage whose truncation already exceeds it. So the only rational that is at or above every truncation and at or below 1 is 1 itself. The challenge at the top of this page is not merely hard. It has no answer, and the kernel now says so for every fraction rather than for the four the verifier happened to try.

What the kernel is not saying. It does not prove 0.999… = 1. That sentence needs a definition of what an infinite decimal denotes (the limit of its truncations) and a construction of the real numbers to take that limit in, and a file with no imports has neither. What is proved is the pair of facts that definition turns into the equality, and the pair is about rationals. The real-number statement wants Mathlib and is left named rather than implied.

Proof: research/finite-gap/lean/FiniteGap.lean (theorems nines_gap, thirds_gap, trunc_lt_one, overtaken, only_one_limit; zero imports, axiom footprint [propext, Quot.sound], no sorry). The bridge from the proof to this page, which is the part a kernel cannot check, is research/finite-gap/verify-finite-gap.mjs: it asserts that the Lean model computes the same numbers this page computes, and it does so against four deliberately wrong transcriptions that it requires itself to catch.

The one honest "well, actually." "0.999… = 1" is a statement about the ordinary real numbers, and there the equality is total — not "for all practical purposes," but identical. Some number systems (the hyperreals, the surreals) do contain infinitesimals, numbers smaller than every 1⁄10ⁿ yet larger than zero. But the symbol "0.999…" isn't given a smaller value there: by the standard meaning of decimal notation it denotes the limit of its partial sums, which is 1. The infinitesimals are real mathematics; they just aren't what "0.999…" points at.