Prove2Me

The optimal success probability is at least 1/e1/e for every nn

Proved
ClassicalSecretary.exp_neg_one_le_optimalProb

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

optimal-stoppingprobabilitysecretary-problem

For every number of applicants n≥1n \ge 1,

Vn=sup⁡sPn(s) ≥ 1e.V_n = \sup_s P_n(s) \ \ge\ \frac1e .

Together with the goal theorem, this says the optimal success probability never falls below its limit.

Preamble
import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology
Formal statement
namespace ClassicalSecretary

theorem exp_neg_one_le_optimalProb (n : ℕ) (hn : 1 ≤ n) :
    Real.exp (-1) ≤ optimalProb n := by sorry

end ClassicalSecretary
Source
Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, introduction: "It implies that the optimal win probability is always at least 1/e".
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