Ahlfors and Grunsky conjectured that the classical Bloch constant equals the value A_AG ≈ 0.4718617 obtained from their equilateral-triangle construction. The problem is to decide whether this upper bound is sharp.

The Ahlfors–Grunsky function is realized as a developing map of a genus-two equilateral translation surface, built as a branched double cover of a flat torus. A shear is applied on a lifted cylinder, and the resulting map is renormalized through the Beltrami equation. The first variation of the hyperbolic derivative is then computed. Critical points stay at the triangle vertices, so univalent disks are bounded by triangle circumradii. A second shear of the compact surface gives an explicit quantitative bound.

The Bloch constant is strictly smaller than A_AG, which disproves the Bloch constant conjecture, and an explicit improved upper bound is derived. Theorem 1.1, Corollary 1.2 and Theorem 1.3 are formalized in Lean 4 with Mathlib.