Prove2Me

The 37% rule: the optimal success probability tends to 1/e1/e

Proved
ClassicalSecretary.tendsto_optimalProb

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

optimal-stoppingprobabilitysecretary-problem

Let VnV_n be the largest probability, over all stopping rules that use only the relative ranks of the applicants seen so far, of selecting the best of nn applicants interviewed in a uniformly random order. Then

lim⁡n→∞Vn=1e≈0.368.\lim_{n\to\infty} V_n = \frac1e \approx 0.368 .

This is the classical solution of the secretary problem: as the number of applicants grows, the best achievable chance of picking the single best one converges to 1/e1/e.

Preamble
import Mathlib
import Definitions.Def_ClassicalSecretary_Model

open Finset Filter Topology
Formal statement
namespace ClassicalSecretary

theorem tendsto_optimalProb :
    Tendsto optimalProb atTop (𝓝 (Real.exp (-1))) := by sorry

end ClassicalSecretary
Source
Wikipedia, "Secretary problem", https://en.wikipedia.org/wiki/Secretary_problem, section "Deriving the optimal policy": "the best applicant is selected with probability 1/e" and "The probability of selecting the best applicant in the classical secretary problem converges toward 1/e ≈ 0.368".
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