Validity and Certification
Our proof depends heavily on computer calculations, raising two issues
about its validity:
Calculations. Reproducing elaborate calculations on a large computer
is difficult; particularly when a complicated parallel computer program is involved, everybody should be skeptical
about the reliability of the results; and
We address these issues in turn.
What our program was trying to
compute is an eigenvalue of a matrix. The amount and length of the
computations are irrelevant to the
fact that eventually we have stored
on disk a witness array of floating-point numbers (the “proof”), approximately 450GB in size, which is a good
approximation of the eigenvector
corresponding to λ27. This array provides rigorous bounds on the true eigenvalue λ27, because the relation ( 1)
holds for any vector yold and its successor vector ynew. To check the proof and
evaluate the bounds ( 1), a program
has to read only the approximate eigenvector yold and carry out one iteration (∗). This approach of providing
simple certificates for the result of
complicated computations is the philosophy of “certifying algorithms.” 25
To ensure the correctness of our
checking program, we relied on tradi-
tional methods (such as testing and
code inspection). Some parts of the
program (such as reading the data
from the files) are irrelevant for the
correctness of the result. The main
body of the program consists of a
few simple loops (such as the itera-
tion (∗) and the evaluation of ( 1)). The
only technically challenging part of
the algorithm is the successor com-
putation. For this task, we had two
programs at our disposal that were
written independently by two people
who used different state representa-
tions—and lived in different coun-
tries and did their work several years
apart. We ran two different checking
programs based on these procedures,
giving us additional confidence. We
also tested explicitly that the two suc-
cessor programs yielded the same re-
sults. Both checking programs ran in
a purely sequential manner, and the
running time was approximately 20
Regarding the accuracy of the calculations, one can analyze how the
recurrence (∗) produces ynew from
yold. One finds that each term in the
lower bound ( 1) results from the input data (the approximate eigenvector yold) through at most 26 additions
of positive numbers for computing
ynew[s], plus one division, all in single-precision float. The final minimization was error-free. Since we took care
that no denormalized floating-point
numbers occurred, the magnitude of
the numerical errors was comparable
to the accuracy of floating-point numbers, and the accumulated error was
thus much smaller than the gap we
opened between our new bound and
4. By carefully bounding the floating-point error, we obtained 4.00253176
as a certified lower bound on λ. In
particular, we thus now know that the
leading digit of λ is 4.
We acknowledge the support of the facilities and staff of the Hasso Plattner
Institute Future SOC Lab in Potsdam,
Germany, who let us use their Hewlett
Packard ProLiant DL980 G7 server. A
technical version of this article6 was
presented at the 23rd Annual European
Symposium on Algorithms in Patras,
Greece, September 2015.
1. Appel, K. and Haken, W. Every planar map is four
colorable. Illinois Journal of Mathematics 21, 3 (Sept.
1977), 429−490 (part I) and 491−567 (part II).
2. Avigad, J. and Harrison, J. Formally verified
mathematics. Commun. ACM 57, 4 (April 2014), 66− 75.
3. Aleksandrowicz, G., Asinowski, A., Barequet, G., and
Barequet, R. Formulae for polyominoes on twisted
cylinders. In Proceedings of the Eighth International
Conference on Language and Automata Theory and
Applications, Lecture Notes in Computer Science
8370 (Madrid, Spain, Mar. 10− 14). Springer-Verlag,
Heidelberg, New York, Dordrecht, London, 2014, 76–87.
4. Barequet, G. and Moffie, M. On the complexity of Jensen’s
algorithm for counting fixed polyominoes. Journal of
Discrete Algorithms 5, 2 (June 2007), 348−355.
5. Barequet, G., Moffie, M., Ribó, A., and Rote, G. Counting
polyominoes on twisted cylinders. INTEGERS:
Electronic Journal of Combinatorial Number Theory 6
(Sept. 2006), #A22, 37.
6. Barequet, G., Rote, G., and Shalah, M. λ > 4. In
Proceedings of the 23rd Annual European Symposium
on Algorithms Lecture Notes in Computer Science
9294 (Patras, Greece, Sept. 14− 16). Springer-Verlag,
Berlin Heidelberg, Germany, 2015, 83− 94.
7. Barequet, G. and Shalah, M. Polyominoes on twisted
cylinders. In the Video Review at the 29th Annual
Symposium on Computational Geometry (Rio de
Janeiro, Brazil, June 17–20). ACM Press, New York,
2013, 339−340; http://www.computational-geometry.
8. Broadbent, S.R. and Hammersley, J.M. Percolation
processes: I. Crystals and mazes. Proceedings of the
Cambridge Philosophical Society 53, 3 (July 1957),
9. Conway, A. Enumerating 2D percolation series by the
finite-lattice method: Theory. Journal of Physics, A:
Mathematical and General 28, 2 (Jan. 1995), 335−349.
10. Derrida, B. and Herrmann, H.J. Collapse of branched
polymers. Journal de Physique 44, 12 (Dec. 1983),
11. Flesia, S., Gaunt, D.S., Soteros, C.E., and Whittington,
S.G. Statistics of collapsing lattice animals. Journal
of Physics, A: Mathematical and General 27, 17 (Sept.
12. Gaunt, D.S., Sykes, M.F., and Ruskin, H. Percolation
processes in d-dimensions. Journal of Physics
A: Mathematical and General 9, 11 (Nov. 1976),
13. Golomb, S. W. Polyominoes, Second Edition. Princeton
University Press, Princeton, NJ, 1994.
14. Gonthier, G. Formal proof—The four color theorem.
Notices of the AMS 55, 11 (Dec. 2008), 1382−1393.
15. Guttmann, A.J., Ed. Polygons, Polyominoes and
Polycubes, Lecture Notes in Physics 775. Springer,
Heidelberg, Germany, 2009.
16. Hales, T., Solovyev, A., and Le Truong, H. The Flyspeck
Project: Announcement of Completion, Aug. 10,
17. Hopcroft, J.E. and Tarjan, R.E. Dividing a graph
into triconnected components. SIAM Journal of
Computing 2, 3 (Sept. 1973), 135−158.
18. Jensen, I. Counting polyominoes: A parallel
implementation for cluster computing. In Proceedings
of the International Conference on Computational
Science, Part III, Lecture Notes in Computer Science,
2659 (Melbourne, Australia, and St. Petersburg,
Russian Federation, June 2− 4). Springer-Verlag, Berlin,
Heidelberg, New York, 2003, 203−212.
19. Klarner, D.A. Cell growth problems. Canadian Journal
of Mathematics 19, 4 (1967), 851−863.
20. Klarner, D.A. and Rivest, R.L. A procedure for improving
the upper bound for the number of n-ominoes. Canadian
Journal of Mathematics 25, 3 (Jan. 1973), 585−602.
21. Lagarias, J.C., Ed. The Kepler Conjecture: The Hales-Ferguson Proof. Springer, New York, 2011.
22. Lubensky, T.C. and Isaacson, J. Statistics of lattice
animals and dilute branched polymers. Physical
Review A 20, 5 (Nov. 1979), 2130−2146.
23. Madras, N. A pattern theorem for lattice clusters.
Annals of Combinatorics 3, 2–4 (June 1999), 357−384.
24. Madras, N., Soteros, C.E., Whittington, S.G., Martin,
J.L., Sykes, M.F., Flesia, S., and Gaunt, D.S. The free
energy of a collapsing branched polymer. Journal of
Physics, A: Mathematical and General 23, 22 (Nov.
25. McConnell, R.M., Mehlhorn, K., Näher, S., and
Schweitzer, P. Certifying algorithms. Computer
Science Review 5, 2 (May 2011), 119−161.
26. Mertens, S. and Lautenbacher, M.E. Counting lattice
animals: A parallel attack. Journal of Statistical
Physics 66, 1–2 (Jan. 1992), 669−678.
27. Redelmeier, D.H. Counting polyominoes: Yet another
attack. Discrete Mathematics 36, 3 (Dec. 1981), 191−203.
28. Schmidt, J.M. Contractions, removals and certifying
3-connectivity in linear time, SIAM Journal on
Computing 42, 2 (Mar. 2013), 494−535.
29. Sykes, M. F. and Glen, M. Percolation processes in two
dimensions: I. Low-density series expansions. Journal
of Physics, A: Mathematical and General 9, 1 (Jan.
30. Tucker, W. A rigorous ODE solver and Smale’s 14th
problem. Foundations of Computational Mathematics 2,
1 (Jan. 2002), 53− 117.
Gill Barequet ( firstname.lastname@example.org) is an associate
professor in and vice dean of the Department of Computer
Science at the Technion - Israel Institute of Technology,
Günter Rote ( email@example.com) is a professor in the
Department of Computer Science at Freie Universität
Mira Shalah ( firstname.lastname@example.org) is a Ph.D.
student, under the supervision of Gill Barequet, in
the Department of Computer Science at the Technion -
Israel Institute of Technology, Haifa, Israel.
© 2016 ACM 0001-0782/16/07 $15.00