Up to dimension seven, compact (simply connected) homogeneous Einstein manifolds had been almost completely classified. The only remaining case was the six-dimensional Lie group S³×S³ ≅ SU(2)×SU(2). The Einstein equations for left-invariant metrics on S³×S³ are extremely messy algebraic equations. (See https://doi.org/10.1016/j.geomphys.2018.02.015) But now this seems to have been resolved! In https://arxiv.org/abs/2609.06425, Gu and Qi use a novel approach that I still have to understand. And they even have an accompanying Lean formalization! According to their paper, the only left-invariant Einstein metrics on S³×S³ are the ones we already know: namely, the product of the round metric on S³ with itself, and another metric that is "nearly Kähler" and comes from the Killing form of SU(2)³ (when you write S³×S³ = SU(2)³/diag(SU(2))). They declare using AI "to explore proof strategies and assist in the drafting", but apparently not for the formalization. I will check out the definitions/theorem statements and report back! By the way, with this classification settled, now earlier results (see https://dx.doi.org/10.4310/CAG.2022.v30.n8.a9) imply that all compact homogeneous Einstein manifolds up to dimension seven which are not Riemannian symmetric spaces are unstable (with respect to the Einstein-Hilbert action).