No zeros of $\zeta$ with $\tfrac12<\operatorname{Re} s<1$ in the upper strip $\operatorname{Im} s>2$

Let $\zeta$ denote the Riemann zeta function. The assertion is that $\zeta$ has no zero strictly to the right of the critical line inside the critical strip and above height $2$:

This is open, and it is equivalent to the Riemann hypothesis. Indeed, the three facts that are unconditionally known reduce the hypothesis to exactly this region: non-vanishing on $\operatorname{Re} s\ge 1$ is classical; the low-lying rectangle $0<\operatorname{Re} s<1$, $|\operatorname{Im} s|\le 2$ is zero-free by an explicit estimate on the completed zeta function; and the reflection identity $\zeta(\bar s)=\overline{\zeta(s)}$ transfers a zero with $\operatorname{Im} s<-2$ to one with $\operatorname{Im} s>2$. Hence non-vanishing in the region above implies $\zeta(s)\neq 0$ for all $\operatorname{Re} s>\tfrac12$, which by the functional equation and the localisation of the nontrivial zeros in the critical strip is the Riemann hypothesis.

Formalization note. riemannZeta is Mathlib's zeta function.