We present a machine-checked, formal proof of PAC learnability of the concept class of decision stumps. This classic result in machine learning theory derives a bound on error probabilities for a simple type of classifier. We construct and check our proof using the Lean theorem prover. Though such a proof appears simple on paper, analytic and measure-theoretic subtleties arise when carrying it out fully formally. We explain how we can cleanly separate out parts that deal with these subtleties.