Success probability of the cutoff rule: $P(r)=\frac{r-1}{n}\sum_{i=r}^n\frac1{i-1}$

Proved

ClassicalSecretary.successProb_cutoffRule

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

optimal-stoppingprobabilitysecretary-problem

Let $2 \le r \le n$ . The cutoff rule that rejects the first $r-1$ applicants and then accepts the first applicant who is better than all earlier ones selects the best applicant with probability

P_n(\text{cutoff } r) = \frac{r-1}{n}\sum_{i=r}^{n}\frac{1}{i-1}.

This exact formula is the basis for both the small- $n$ table and the asymptotic analysis of the optimal cutoff.

Preamble

import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology

Formal statement

namespace ClassicalSecretary

theorem successProb_cutoffRule (n r : ℕ) (hr : 2 ≤ r) (hrn : r ≤ n) :
    successProb n (cutoffRule r) =
      ((r : ℝ) - 1) / (n : ℝ) * ∑ i ∈ Icc r n, 1 / ((i : ℝ) - 1) := by sorry

end ClassicalSecretary

Source

Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy", displayed formula for P(r).

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Nov 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Success probability of the cutoff rule: P(r)=r−1n∑i=rn1i−1P(r)=\frac{r-1}{n}\sum_{i=r}^n\frac1{i-1}P(r)=nr−1​∑i=rn​i−11​

Success probability of the cutoff rule: $P(r)=\frac{r-1}{n}\sum_{i=r}^n\frac1{i-1}$