A high-tech proof of the Mills-Robbins-Rumsey determinant formula (Q1918896)

The formula in question states that \[ \text{det}\Biggl(\Biggl({i+ j+ \mu\atop 2i- j}\Biggr)^{n- 1}_{i, j= 0}\Biggr)= 2^{- n} \prod^{n- 1}_{k= 0} \Delta_{2k}(2\mu), \] where \(\mu\) is an indeterminate, \(\Delta_0(\mu)= 2\) and for \(j= 1,2,\dots\), \[ \Delta_{2j}(\mu)= {(\mu+ 2j+ 2)_j({1\over 2} \mu+ 2j+ {3\over 2})_{j- 1}\over (j)_j ({1\over 2} \mu+ j+ {3\over 2})_{j- 1}}, \] with \((x)_j= x(x+ 1)\cdots (x+ j- 1)\) being the usual rising factorial. We give here a short computer-assisted proof. This proof is conceptually very simple. The intrinsic depth of the problem is reflected only in the very large polynomial that is contained in the proof certificate.