Prove2Me

Cutoff r=1r=1 selects the best with probability 1/n1/n

Proved
ClassicalSecretary.successProb_cutoffRule_one

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

optimal-stoppingprobabilitysecretary-problem

Let n≥1n \ge 1. The cutoff rule with cutoff r=1r = 1 accepts the very first applicant, who is always a candidate. Its success probability is

Pn(cutoff 1)=1n.P_n(\text{cutoff } 1) = \frac1n .

This is the boundary case r=1r=1 of the success-probability formula for cutoff rules, which the general sum does not cover.

Preamble
import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology
Formal statement
namespace ClassicalSecretary

theorem successProb_cutoffRule_one (n : ℕ) (hn : 1 ≤ n) :
    successProb n (cutoffRule 1) = 1 / (n : ℝ) := by sorry

end ClassicalSecretary
Source
Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy", sentence after the displayed formula for P(r)P(r): "in this case the only feasible policy is to select the first applicant, and hence P(1) = 1/n".
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