Computationally-assisted proof of a novel $\mathsf{O}(3)\times \mathsf{O}(10)$-invariant Einstein metric on $S^{12}$

We prove existence of a non-round Einstein metric $g$ on $S^{12}$ that is invariant under the usual cohomogeneity one action of $\mathsf{O}(3)\times \mathsf{O}(10)$ on $S^{12}\subset {\mathbb{R}}^{13}={\mathbb{R}}^3\oplus {\mathbb{R}}^{10}$. The proof involves using several rigorous numerical analysis techniques to produce a Riemannian metric $\widehat{g}$ which approximately satisfies the Einstein condition to known high precision, and then demonstrating that $\widehat{g}$ can be perturbed into a true Einstein metric $g$.