Lean formalization of the proof on the upper bound of the probability for LIPO to reject a candidate.
Install Lean, then run lake exe cache get in the root directory. Explore UpperBound.lean for the proof.
One can also look at the HTML-rendered proof here or in html/UpperBound.lean.html.