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).