The Positive Test That's Probably Wrong

A test is 99% accurate. It just told you that you have a disease that 1 in 100 people carry. How worried should you be? The honest answer is a coin flip. This is the trap Bayes' theorem unsprings, and you can watch it spring below.

If your test comes back positive, the chance you are actually sick is

50.0%

Out of everyone who tests positive, half are perfectly healthy people the test flagged by mistake.

Turn the three dials

How common the disease is (prevalence) 1 in 100

How many people in the population actually have it, before any test.

Sensitivity — catches the sick 99%

Of people who are sick, the share the test correctly flags positive.

Specificity — clears the healthy 99%

Of people who are healthy, the share the test correctly clears. The rest are false alarms.

sick & caught 99 sick, missed 1 healthy, false alarm 99 healthy & cleared 9801

In this rounded grid of 10,000 people, 100 are sick; the test catches 99 of them. The other 9,900 are healthy, but the test still flags 99 of them by mistake. So 198 people test positive, and only 99 are truly sick. Grid share: 99 in 198 (about 50.0%). The model probability is 50.0%.

The same thing, in modern notation

P(sick | positive) = P · Se / ( P · Se + (1−P) · (1−Sp) ) ≈ 50.0%

That is all Bayes' theorem is: the positive results split into the truly sick (P · Se) and the false alarms ((1−P) · (1−Sp)), and you ask what fraction of the pile is real. When the disease is rare, the false-alarm pile is drawn from the enormous healthy majority — so even a tiny false-positive rate can swamp the few true cases. The accuracy of the test never appears alone; it is always weighed against how rare the thing you're testing for is. Ignore the base rate and you get the wrong answer — usually by reporting the test's accuracy as if it were your odds.

This isn't a hypothetical failure. In 1978 Casscells and colleagues posed exactly the 1-in-1000 / 5%-false-alarm question to staff and students at Harvard Medical School. The most common answer was 95%. The correct answer is under 2% — and only about 18% of them got it right.¹ Set the dials to the Casscells preset above and watch why.

Show the check

Selected count calculations and sampled probability-versus-odds comparisons are checked in research/bayes-theorem/verify.mjs (run it from a fresh checkout). It checks:

The closed-form posterior P·Se / (P·Se + (1−P)·(1−Sp)) equals a brute-force count over a finite population — the very grid above — to within one person's worth of rounding, across a sweep of cases.
The probability form agrees with the odds form (prior odds × likelihood ratio Se/(1−Sp)) to 1 part in 10¹⁵, over 200,000 random inputs.
The headline default — a 99%-accurate test (Se = Sp = 99%) for a 1%-prevalent disease — gives a posterior of exactly ½. That is structural: the true-positive and false-positive piles are literally equal.
Selected literature examples and an adaptation are recomputed: Casscells 1978 (≈ 2%), Eddy 1982 breast cancer, with sensitivity rounded to 80% (≈ 7.8%), and Gigerenzer et al. 2007 mammography (≈ 9.2%).
For fixed positive sensitivity and a fixed positive false-positive rate, the posterior is strictly increasing in prevalence, → 0 as the disease vanishes and → 1 as it becomes universal; a useless test (Se = 1−Sp) never moves the prior at all.
And now machine-checked: the counts above are handed to Lean's kernel (research/bayes-theorem/lean/Bayes.lean), which builds a 1,000-person clinic and proves the base-rate law — including, for every population at once, that rarity beats accuracy. See below.

Machine-checked — the kernel pins the thesis

The check above computes the answer once, in JavaScript, and samples its universal claims over random draws. A sample is evidence, not a proof. So the same counts are now handed to a proof assistant's kernel in research/bayes-theorem/lean/Bayes.lean (Lean 4, zero imports — no library, only the kernel is trusted). Over an equiprobable population a plain count is a probability: the kernel builds all 1,000 people of a clinic and counts them, and — where the sampling could only check a finite window — it proves the base-rate law for every population at once.

-- The clinic, enumerated: 1,000 people; 1% sick; test catches 90%, false-alarms 10%.
def clinic : List Person := cohorts 9 1 99 891

-- Of the 108 who test positive, only 9 are truly sick: 9/108 = 1/12 ≈ 8.3%.
theorem clinic_posterior_one_twelfth :
    countB truePos clinic * 12 = countB positive clinic * 1 := by decide

-- The headline: a "99% accurate" test on a 1-in-100 disease → 99/198 = 1/2, a coin flip.
theorem flagship_is_a_coin_flip : 99 * 2 = (99 + 99) * 1 := by decide

-- Rarity beats accuracy — proved for EVERY population, not sampled:
-- however sensitive the test (tp ≤ sick), if false-alarms outnumber the sick
-- population (sick < fp), a positive is more likely a false alarm (tp < fp).
theorem rarity_beats_accuracy (sick tp fp : Nat)
    (hacc : tp ≤ sick) (hrare : sick < fp) : tp < fp ∧ 2 * tp < tp + fp := by
  refine ⟨?_, ?_⟩ <;> omega

#print axioms the_base_rate_decides       -- enumerated counts: NO axioms at all
#print axioms rarity_beats_accuracy       -- universal (omega): [propext, Quot.sound]

Lean 4.30 · the_base_rate_decides — does not depend on any axioms · rarity_beats_accuracy — [propext, Quot.sound]

No sorry, no Classical.choice, no native_decide. The enumerated counts reduce in the kernel and depend on no axioms whatsoever; the universal theorems lean only on the two propositional axioms every Lean proof may use. Re-run it yourself: bash research/bayes-theorem/lean/verify.sh (Lean not installed? bash research/bayes-theorem/lean/install-lean-nix.sh). verify.mjs §6 recomputes the integer counts in JavaScript and, when lean is on your PATH, runs the proof live and confirms the axiom verdict — all pass.