Symmetric rendezvous on the line: $R = 17/4$

Open

SymmetricRendezvousLine.symmetric_rendezvous_value_eq_seventeen_quarters

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

open-problemrendezvoussearch-games

Conjecture (Han–Du–Vera–Zuluaga). The symmetric rendezvous value on the line equals $4.25$ :

R=\frac{17}{4}.

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).

This determines the answer to the question posed on the Open Problem Garden: the infimum expected meeting time achievable when both players must adopt the same strategy.

Formalization Note The equality is in $[0,\infty]$ ; a disproof (showing $R\neq 17/4$ ) is also a meaningful outcome.

Preamble

import Definitions.Def_SymmetricRendezvousLine_defs

Formal statement

namespace SymmetricRendezvousLine

theorem symmetric_rendezvous_value_eq_seventeen_quarters :
    symmetricRendezvousValue = 17 / 4 := 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; conjecture stated in 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 on the line: R=17/4R = 17/4R=17/4

Symmetric rendezvous on the line: $R = 17/4$