Pattern · probability
The Door You Didn't Pick
Three doors. A car behind one, a goat behind each of the others. You choose; the host opens a different door to show a goat; then he offers you the swap. Keep your door, or take the last one? The answer feels like a coin-flip and isn't. The deciding detail is the host's rule: he knows where the car is and always reveals a goat.
Play it — the three-door game
Pick a door to begin.
One game cannot establish the win rate. So play a few, watch your own two tallies drift apart, and then let the machine do what no contestant ever could: play the same game ten thousand times.
Skip the suspense — simulate
Uses the host behaviour you selected above: Host knows.
Why two-thirds, not one-half
Your first pick is right one time in three. Under the classic rule, the host always reveals a goat and chooses equally when either goat door can open, so your pick stays at one in three. A strategy of staying wins exactly 1/3. The car is behind one of the other two doors the remaining 2/3 of the time — and the host, by opening the goat among them, quietly sweeps that entire two-thirds onto the single door he leaves closed. Switching doesn't gamble on one door; it collects both of the doors you didn't pick, minus the goat the host kindly removed. That is the whole trick: the host's open door is not new randomness — it's a concentrated clue.
The deciding rule: the host has to know
Flip the toggle to “Host forgets” and run ten thousand games. Switching drops to a coin-flip — 1/2. Nothing about your choice changed. What changed is the host. The two-thirds edge was never really yours; it was information the host injected by deliberately avoiding the car. A host opening a door at random injects nothing: when he happens to miss the car (two times in three), the car is now equally likely to be behind your door or the other one, and switching gains you nothing. The famous answer “always switch” is not a fact about doors. It is a fact about a host who knows where the car is and is bound to reveal a goat. Change that rule and the answer changes with it.
Turn up the doors (a knowing host) — and the intuition arrives
You pick one. The host throws open every goat door but one, then offers the swap. Switching wins 2 / 3 = 66.7%.
At 100 doors the host all but points at the car — and staying loyal to your one-in-a-hundred guess suddenly looks as foolish as it always was.
The check — show the working
The verifier compares exact calculations with seeded Monte-Carlo simulations:
it enumerates the three-door game trees, uses (N−1)/N for N doors, and also
enumerates the ten-door atom counts. The browser runs live simulations against the exact
probabilities. The certificate is research/monty-hall/verify.mjs;
all checks pass:
- Knowing host: staying wins
1/3, switching wins2/3(enumerated exactly; 400,000-game simulation lands at 0.333 / 0.668). - Forgetful host: among games where a goat is shown, staying and switching each win
1/2— and the host reveals the car outright in1/3of all games. - N doors, knowing host opening all but one other: switching wins
(N−1)/N—2/3at N=3,0.99at N=100 (simulation matches each). - Price of the misconception: a switcher wins twice as often as a stayer in the classic game —
2/3vs1/3.
Machine-checked — the kernel pins the thesis
The check above enumerates the game tree — once, in JavaScript, in arithmetic you have to take on trust. Below the same counts are handed to Lean's kernel, a proof anyone can re-run. The model is identical (an equiprobable atom space, so a plain count is a probability), but now the machine decides it, for every case at once, and — the point of this page — proves the two host protocols give two different answers:
-- research/monty-hall/lean/MontyHall.lean (zero imports; the kernel alone) theorem the_host_protocol_decides : classicSwitchCount * 3 = classicAtoms.length * 2 -- knowing host: switch = 2/3 ∧ forgetSwitchCount * 2 = forgetGoatCount * 1 -- forgetful host: switch = 1/2 ∧ forgetGoatCount = 12 ∧ forgetCarRevealedCount = 6 -- car blown 1/3 of the time := by decide
Each count is a finite enumeration the kernel evaluates itself (by decide) — no
sampling, no floating point, no imported library. What it certifies:
- Knowing host (18 equiprobable atoms): switch wins
12/18 = 2/3, stay wins6/18 = 1/3— and the host reveals a goat on all 18 (never your door, never the car). - Forgetful host (same 18): the car is blown outright in
6/18 = 1/3; conditioned on a goat, switch and stay each win6/12 = 1/2. The edge is gone — no door, car, or goat moved, only what the host knew. - Ten doors, knowing host (100 atoms): switch wins
90/100 = 9/10. The effect amplified.
No sorry, no Classical.choice, no native_decide — the
verdict is even tighter than the usual [propext, Quot.sound]: these theorems rest
on no axioms at all. Re-run it yourself: install Lean 4 using the
official installation guide, then download
MontyHall.lean and
verify.sh into the same folder.
From that folder, run bash verify.sh (checked with Lean 4.35.0). The JavaScript
verifier recomputes these integer counts
and, when Lean is present, drives the proof live.
The smartest people in the world got this wrong
When Marilyn vos Savant gave the correct answer — switch — in her Parade column in 1990, she estimated receiving some 10,000 letters, most disagreeing. Close to 1,000 critical letters carried PhD signatures, many on mathematics and science department letterhead.1 Paul Erdős, one of the most prolific mathematicians who ever lived, refused to accept the result until a colleague showed him a computer simulation of it1 — the very thing you just ran. The problem had been posed and correctly solved fifteen years earlier, in 1975, by the statistician Steve Selvin in a pair of letters to The American Statistician; his second letter is the first known use of the name “Monty Hall problem,” after the host of the game show Let's Make a Deal.1
Honest apparatus
The classic answer rests on stated rules, not vibes. “Always switch”
requires that the host (a) always opens a door, (b) always opens one with a goat, never
the car or your door, and (c) always offers the switch regardless of your first pick. These
are the standard assumptions of the puzzle; vos Savant later clarified them after the
controversy, because a host with other habits gives other answers. The “Host forgets”
toggle drops assumption (b) and the answer moves to 1/2 — the page makes the
dependence operable rather than burying it. A host who only offers the switch when you've
picked the car could make switching lose every time; that adversarial case is
named here but not simulated.
What's proven vs. asserted. The probabilities are proven for the stated rules — enumerated exactly, matched by simulation (see the check), and machine-checked: Lean's kernel re-derives the same counts with zero imports and no axioms (research/monty-hall/lean/MontyHall.lean). The historical figures (≈10,000 letters, ≈1,000 PhDs; Erdős persuaded only by simulation; Selvin's 1975 priority) are reported from the sources below, not independently audited; vos Savant's letter counts are her own estimate.
- Wikipedia, “Monty Hall problem” — the standard assumptions, vos Savant's 1990 Parade column and the ≈10,000-letter response, Paul Erdős's simulation, and Steve Selvin's 1975 American Statistician letters. en.wikipedia.org/wiki/Monty_Hall_problem. Origin: S. Selvin, “A Problem in Probability,” The American Statistician 29(1), 1975.
Verifier: research/monty-hall/verify.mjs (exact calculation + seeded Monte-Carlo for the knowing host, the forgetful host, and the N-door version).
More in this vein
Probability is the branch of mathematics our intuition is worst at, and this is one of the Wasteland's largest veins. The same trap — trust the gut, get it confidently wrong — runs through the birthday paradox, the 99%-accurate test that's a coin-flip, and a chart that pure chance draws for free. The whole vein, walked movement by movement, is gathered at The Paradoxes of Chance.
Corrections
Corrected 2026-10-14: The Bayes relation said a random host's goat reveal was no real evidence and updated nothing. It raises the chosen door's probability from 1/3 to 1/2, leaving both unopened doors equally likely; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The film's upload date was listed as 2026-07-09. The publication commit and accompanying log record it on 2026-06-26; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said changing the host rule explained why the puzzle fooled careful readers. The answer does depend on the rule, but vos Savant reported that most correspondents understood the conditions; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page directed readers to install-lean-nix.sh without supplying a public copy. It now links to Lean's installation guide and the published proof and runner; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The two authored verifier links led to a missing /research/ URL. They now point to the published /checks/research/monty-hall/verify.mjs; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said most or almost every telling omitted the host's knowledge and that the internet left it out. The original column explicitly states the host's knowledge; the prevalence claim was unsupported; found by the assay line, 2026-10-14.