Remix.run Logo
▲ JacobAsmuth an hour ago

There's nothing to check there, they used the standard mathlib implementation of RH. THey didn't write their own for the 7/8ths proof.