rate in the sense of the limit λ = limn→∞
A(n + 1)/A(n) exists.
By using interpolation methods,
Sykes and Glen29 estimated in 1976
that λ = 4.06 ± 0.02. This estimate was
refined several times based on heuristic extrapolation from the increasing
number of known values of A(n). The
most accurate estimate— 4.0625696
± 0.0000005—was given by Jensen18
in 2003. Before carrying out this project, the best proven bounds on λ
were roughly 3.9801 from below5
and 4.6496 from above. 20 λ has thus
always been an elusive constant, of
which not even a single significant
digit was known. Our goal was to raise
the lower bound on λ over the barrier
of 4, and thus reveal its first decimal
digit and prove that λ ≠ 4. The current
improvement of the lower bound on λ
to 4.0025 also cuts the difference between the known lower bound and the
estimated value of λ by approximately
25%—from 0.0825 to 0.0600.
Computer-Assisted Proofs
Our proof relies heavily on computer
calculations, thus raising questions
about its credibility and reliability. There are two complementary approaches for addressing this issue:
formally verified computations and
certified computations.
Formally verified computing. In this
paradigm, a program is accompanied
by a correctness proof that is refined
to such a degree of detail and formal-
ity it can be checked mechanically
by a computer. This approach and,
more generally, formally verified
“mathematics,” has become feasible
for industry-level software, as well
as for mathematics far beyond toy
problems due to big advances in re-
cent years; see the review by Avigad
and Harrison. 2 One highlight is the
formally verified proof by Gonthier14
of the Four-Color Theorem, whose
original proof by Appel and Haken1 in
1977 already relied on computer as-
sistance and was the prime instance
of discussion about the validity and
appropriateness of computer meth-
ods in mathematical proofs. (Inci-
dentally, one step in Gonthier’s proof
also involves polyominoes.) Another
example is the verification of Hales’s
proof21 of the Kepler conjecture, which
states the face-centered cubic pack-
random graphs. Suppose a unit of liq-
uid L is poured on top of some porous
material M. What is the chance L makes
its way through M and reaches the
bottom? An idealized mathematical
model of this process is a two- or three-
dimensional grid of vertices (“sites”)
connected with edges (“bonds”), where
each bond is independently open (or
closed) for liquid flow with some prob-
ability μ. In 1957, Broadbent and Ham-
mersley8 asked, for a fixed value of μ
and for the size of the grid tending to
infinity, what is the probability that a
path consisting of open bonds exists
from the top to the bottom. They es-
sentially investigated solute diffusing
through solvent, molecules penetrat-
ing a porous solid, and similar process-
es, representing space as a lattice with
two distinct types of cells.
In the literature of statistical physics,
fixed polyominoes are usually called
“strongly embedded lattice animals,”
and in that context, the analogue of
the growth rate of polyominoes is the
growth constant of lattice animals.
The terms high and low “temperature”
mean high and low “density” of clusters, respectively, and the term “free
energy” corresponds to the natural
logarithm of the growth constant. Lattice animals were used for computing
the mean cluster density in percolation
processes, as in Gaunt et al., 12 particularly in processes involving fluid flow in
random media. Sykes and Glen29 were
the first to observe that A(n), the total
number of connected clusters of size n,
grows asymptotically like Cλnnθ, where
λ is Klarner’s constant and C, θ are two
other fixed values.
Collapse of branched polymers.
Another important topic in statistical
physics is the existence of a collapse
transition of branched polymers in
dilute solution at a high temperature.
In physics, a “field” is an entity each of
whose points has a value that depends
on location and time. Lubensky and
Isaacson22 developed a field theory of
branched polymers in the dilute limit,
using statistics of (bond) lattice animals (important in the theory of percolation) to imply when a solvent is good
or bad for a polymer. Derrida and Herrmann10 investigated two-dimensional
branched polymers by looking at lattice animals on a square lattice and
studying their free energy. Flesia et al. 11
made the connection between collapse
processes to percolation theory, relating the growth constant of strongly embedded site animals to the free energy
in the processes. Several models of
branched polymers in dilute solution
were considered by Madras et al., 24
proving bounds on the growth constants for each such model.
Brief History. Determining the exact
value of λ (or even setting good bounds
on it) is a notably difficult problem in
enumerative combinatorics. In 1967,
Klarner19 showed that the limit λ =
limn→∞ A(n)1/n exists. Since then, λ has
been called “Klarner’s constant.” Only
in 1999, Madras23 proved the stronger
statement that the asymptotic growth
Figure 2. A solitaire game involving six
polyominoes of size 5 (pentominoes),
two of size 6 (hexominoes), two of
size 7 (heptominoes), and one of size 8
(an octomino). The challenge is to tile
the 8× 8 square box with the polyominoes.
Figure 1. The single monomino (A( 1) = 1),
the two dominoes (A( 2) = 2), the A( 3) = 6
triominoes, and the A( 4) = 19 tetrominoes
(Tetris pieces).