An optimal stopping rule is a cutoff rule

Proved

ClassicalSecretary.exists_optimal_cutoffRule

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

optimal-stoppingprobabilitysecretary-problem

Let $n \ge 1$ . Among all stopping rules that depend only on the relative ranks seen so far, some cutoff rule is optimal: there is $r$ with $1 \le r \le n$ such that

P_n(\text{cutoff } r) = V_n = \sup_s P_n(s).

This reduces the optimization over all rank-based rules to a one-parameter family.

Preamble

import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology

Formal statement

namespace ClassicalSecretary

theorem exists_optimal_cutoffRule (n : ℕ) (hn : 1 ≤ n) :
    ∃ r : ℕ, 1 ≤ r ∧ r ≤ n ∧ successProb n (cutoffRule r) = optimalProb n := by sorry

end ClassicalSecretary

Source

Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy", first paragraph: "It can be shown that the optimal strategy lies in this class of strategies"; History section (Palermo's appendix to Flood's 1958 letter).

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