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
hours each.

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.

Acknowledgments

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.

 

References

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. org/SoCG-videos/socg13video

8. Broadbent, S.R. and Hammersley, J.M. Percolation processes: I. Crystals and mazes. Proceedings of the Cambridge Philosophical Society 53, 3 (July 1957),

629−641.

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), 1365−1376.

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. 1994), 5831−5846.

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), 1899−1911.

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, 2014; https://code.google.com/p/flyspeck/wiki/ AnnouncingCompletion

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. 1990), 5327−5350.

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. 1976), 87−95.

30. Tucker, W. A rigorous ODE solver and Smale’s 14th problem. Foundations of Computational Mathematics 2, 1 (Jan. 2002), 53− 117.

 

Gill Barequet ( [e-mail]) is an associate professor in and vice dean of the Department of Computer Science at the Technion - Israel Institute of Technology, Haifa, Israel.

Günter Rote ( [e-mail]) is a professor in the Department of Computer Science at Freie Universität Berlin, Germany.

Mira Shalah ( [e-mail]) 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