Symmetric rendezvous: $R < 4.2574$

Open

SymmetricRendezvousLine.symmetric_rendezvous_value_lt_4_2574

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

rendezvoussearch-games

Theorem (Han–Du–Vera–Zuluaga). The symmetric rendezvous value on the line satisfies

R<4.2574.

Here $R=\inf_S E(S,S)$ is the symmetric rendezvous value on the line: two players start at distance $2$ , each with an independently random unknown orientation, both moving at speed at most $1$ , both required to use the same mixed strategy $S$ , and $E(S,S)$ is the expected first meeting time (see the definition file).

Equivalently, some single mixed strategy used by both players achieves expected meeting time below $4.2574$ .

Preamble

import Definitions.Def_SymmetricRendezvousLine_defs

Formal statement

namespace SymmetricRendezvousLine

theorem symmetric_rendezvous_value_lt_4_2574 :
    symmetricRendezvousValue < (42574 / 10000 : ENNReal) := by sorry

end SymmetricRendezvousLine

Source

Open Problem Garden, 'Rendezvous on a line' (posted by mdevos, 2007), http://www.openproblemgarden.org/op/rendezvous_on_a_line ("proving 4.1520 < R < 4.2574"); Q. Han, D. Du, J. C. Vera, L. F. Zuluaga, Improved bounds for the symmetric rendezvous search problem on the line, Operations Research 56(3) (2008).

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

Symmetric rendezvous: R<4.2574R < 4.2574R<4.2574

Symmetric rendezvous: $R < 4.2574$