PlaceboVsObserved: Two Designs, One Vaccine

In 1954 the United States tested the Salk polio vaccine on about 1.8 million children, with two designs at once. In some counties, half the consenting children in grades 1 to 3 got the vaccine and half a salt-water placebo, and nobody knew who got which. In the rest, consenting second graders were vaccinated and every first and third grader was watched as a control. The randomized design put effectiveness at 71%; the observed design at 62%. Same vaccine, same year.

PlaceboVsObserved rebuilds the 1955 Francis report from its printed tables, in Python and in R written independently, and asks why the two designs disagreed.

How it is built

Each analysis step has a Python script and an R twin; run_all.sh runs both, compares them, and ends with the Lean proofs.

Reproducible. Python, R and Lean are pinned in flake.nix and flake.lock, every download is checked against a pinned SHA-256 fingerprint, and each run records its versions. The report’s tables were transcribed by hand, cell by cell, and checked against an independent transcription, the R package HistData, before any computation.

Tested. 17 pytest and 7 testthat tests, plus the full-run comparison. Python and R agree on 2,348 of 2,372 quantities to 12 decimals. Eight of the other 24 are floating-point rounding at the 10th to 12th decimal; sixteen trace to one cause, R’s fisher.test stopping its search at a loose default tolerance, and solving the same equation to 10⁻¹² in both brings them to 11 places.

The 1955 arithmetic holds

1,064 of the report’s 1,068 printed values reproduce exactly, in both languages. The four misses are the report’s own: two rates that do not follow from the counts beside them, one rate carried over wrongly, one significance level printed a class too cautious. The code expects those four, so a new miss stops the run. Paul Meier’s widely cited 1972 reprint of the main table has one typo, found the same way. Four modern intervals put the randomized effectiveness at about 57% to 81%, against the report’s one-sided limit of 59.7%.

The gap, taken apart

The observed design had two known flaws, and the report’s tables are detailed enough to correct each.

Six-year-olds had the highest polio rate, and the controls were tilted toward them: about one point. Families who refused the vaccine had children with lower polio rates, and the controls mixed them in: four to six points. What is left is two to three points, inside the noise. And the original gap was never statistically real: its 95% interval runs from −8 to +26 points (p = 0.30). Applied where randomization had already balanced ages, the age correction moves 71.24% to 71.20%, which is how a correction should behave when there is nothing to correct.

The one assumption is stated: consent in grades 1 and 3 is taken to equal grade 2’s. Closing the gap fully would need it 16 to 22 points lower, which the README judges implausible.

The Type I claim. The report found the vaccine weaker against Type I polio but never compared the strains with each other. Compared directly, p = 0.26. What does explain it is manufacturing: lots graded good gave 92% protection against Type I, lots graded poor about 0%, while still 94% against Type III.

The verdicts, proved

Python and R put the chance of the randomized result arising by luck at about 4 × 10⁻¹². Lean proves the decision itself, “below 1 in 1,000,” in whole-number arithmetic, some of it over 800 digits long, with no rounding anywhere. From lean/Salk.lean:

/-- The report's rule, 0.1% level: B = P(X <= 33 | 148, N1/(N1+N2)) < 1/1000. -/
theorem paralytic_B_below_one_in_a_thousand :
    1000 * tailNum N1 N2 (n1 + n2) n1 < (N1 + N2) ^ (n1 + n2) := by
  decide

/-- The point estimate of effectiveness, 1 - (n1/N1) / (n2/N2), exceeds one half. -/
theorem paralytic_effectiveness_above_half : 2 * n1 * N2 < n2 * N1 := by
  decide

Mutation tests keep the proofs honest: tighten the threshold to one in 10¹² and the proof fails, as it should; change a case count and it fails.