The Bloch constant is defined using the set 
of complex analytic functions 
defined on an open region containing
the set closure of the unit
disk 
satisfying 
and 
.
For each 
in 
, let 
be the supremum of all numbers
such that there is a subregion 
in 
on which 
is one-to-one and such that
contains a disk
of radius 
.
Bloch (1925) showed that 
(Conway 1989).
Define Bloch's constant as the infimum
 |
(1)
|
The classical bounds are (Ahlfors and Grunsky 1937, Ahlfors 1938)
 |
(2)
|
Bonk (1990) proved that 
,
which Chen and Gauthier (1996) improved to 
(Finch 2003, p. 456). Wikström
(2026) reports the stronger bound 
using a computer-assisted
proof with interval arithmetic.
Ahlfors and Grunsky (1937) conjectured that 
, where
 |  |  |
(3)
|
 |  |  |
(4)
|
 |  |  |
(5)
|
(Le Lionnais 1983; OEIS A085508), where 
is the gamma
function.
Zhang (2026) reports a refutation of the Ahlfors-Grunsky conjectured value by obtaining 
. The paper
supplies a Lean formalization generated using Codex and reports exploratory ChatGPT
use. The general proof and the formalization have not been independently verified
here.
