An independent certified computation excluding four mutually unbiased bases in dimension six

We show that there are no four mutually unbiased bases in ℂ⁶, so that the maximum number of such bases is three. The proof is computer-assisted and assumes that the machine on which the computation ran carried out binary64 arithmetic correctly, as made precise in Section 3.1. It carries out the discretization proof of a recent preprint by OpenAI, which has not appeared in a refereed journal. Our programs are written from the text of the preprint, and we prove every statement of the preprint that our proof uses. Four mutually unbiased bases could be taken to consist of the standard basis, the columns of a complex Hadamard matrix divided by √6, and two further bases. Finitely many balls in phase coordinates cover all complex Hadamard matrices of order six up to equivalence, and on each small ball a finite search shows that these two further bases do not exist. Every inequality that the programs decide in order to reject a case or to cover a set of matrices is decided in exact integer arithmetic or in interval arithmetic with outward rounding. The programs, with the logs and data of the computation, are deposited.