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 $\hat{g}$ which approximately satisfies the Einstein condition to known high precision, and then demonstrating that $\hat{g}$ can be perturbed into a true Einstein metric $g$.