Prove2Me

The optimal cutoff is asymptotically n/en/e

Proved
ClassicalSecretary.tendsto_optimal_cutoff_div

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

optimal-stoppingprobabilitysecretary-problem

Let (rn)(r_n) be a sequence such that, for every n≥1n \ge 1, 1≤rn≤n1 \le r_n \le n and the cutoff rule with cutoff rnr_n is optimal, i.e. Pn(cutoff rn)=VnP_n(\text{cutoff } r_n) = V_n. Then

lim⁡n→∞rnn=1e.\lim_{n\to\infty}\frac{r_n}{n} = \frac1e .

The statement holds for every choice of optimal cutoffs (for small nn the optimal cutoff need not be unique).

Preamble
import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology
Formal statement
namespace ClassicalSecretary

theorem tendsto_optimal_cutoff_div (r : ℕ → ℕ)
    (hr : ∀ n : ℕ, 1 ≤ n →
      1 ≤ r n ∧ r n ≤ n ∧ successProb n (cutoffRule (r n)) = optimalProb n) :
    Tendsto (fun n : ℕ => (r n : ℝ) / (n : ℝ)) atTop (𝓝 (Real.exp (-1))) := by sorry

end ClassicalSecretary
Source
Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy": "Thus, the optimal cutoff tends to n/e as n increases".
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).

View graph