An effective André–Oort theorem for Shimura varieties

We give effective bounds for the special subvarieties V that are maximal in a subvariety Z of a Shimura variety, in terms of the degree of Z: for the degree of V, with no hypothesis; and for the discriminant of a number field L_V attached to V and the Klingler–Yafaev invariant α_V of the level, if for some δ > 0 the Dedekind zeta function of L_V has no zero with real part greater than 1 − δ. Here Z is geometrically irreducible and defined over a number field, the level is neat and of product form, and the bounds are explicit in the degree of Z and, for L_V and α_V, also in the degree of the field and δ, with constants that are effectively computable from the Shimura datum, the level and representatives of the connected components of the Shimura variety. A preprint of Cureton and Thorner, whose proof has been formalized in Lean, establishes such a half-plane with δ = 1/32 for every number field; granting it, all these bounds hold with no further hypothesis. For abelian type, an algorithm lists these subvarieties from the bounds, given a finite étale cover by a Shimura variety of Hodge type inside one of Mumford's moduli spaces and equations for the preimage of Z.