zbMATH — the first resource for mathematics

Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. (English) Zbl 07038739
Summary: A conjecture originally made by Klein and Szekeres in 1932 (now commonly known as “Erdős-Szekeres” or “Happy Ending” conjecture) claims that for every \(m \geq 3\), every set of \(2^{m-2}+1\) points in a general position (none three different points are collinear) contains a convex \(m\)-gon. The conjecture has been verified for \(m \leq 6\). The case \(m=6\) was solved by Szekeres and Peters and required a huge computer enumeration that took “more than 3000 GHz hours”. In this paper we improve the solution in several directions. By changing the problem representation, by employing symmetry-breaking and by using modern SAT solvers, we reduce the proving time to around only a half of an hour on an ordinary PC computer (i.e., our proof requires only around 1 GHz hour). Also, we formalize the proof within the Isabelle/HOL proof assistant, making it significantly more reliable.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Aehlig, K.; Haftmann, F.; Nipkow, T.; Mohamed, OA (ed.); Munoz, C. (ed.); Tahar, S. (ed.), A compiled implementation of normalization by evaluation, No. 5170, 39-54, (2008), Berlin · Zbl 1165.68442
[2] Avigad, J.; Harrison, J., Formally verified mathematics, Commun. ACM, 57, 66-75, (2014)
[3] Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Proceedings of Mathematical Knowledge Management, MKM, pp. 31-43 (2006) · Zbl 1188.68258
[4] Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[5] Bonnice, WE, On convex polygons determined by a finite planar set, Am. Math. Mon., 81, 749752, (1974) · Zbl 0295.52002
[6] Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Proceedings of Automated Deduction—CADE-26—26th International Conference on Automated Deduction, Gothenburg, Sweden, LNCS. Springer (2017)
[7] Dehnhardt, K.; Harborth, H.; Längi, Z., A partial proof of the Erdős-Szekeres conjecture for hexagons, J. Pure Appl. Math. Adv. Appl., 2, 6986, (2009) · Zbl 1187.52015
[8] Erdős, P.; Szekeres, G., A combinatorial problem in geometry, Compos. Math., 2, 463-470, (1935) · Zbl 0012.27010
[9] Hales, T.C. (ed.): Notices of the AMS: Special Issue on Formal Proof, vol. 55(11). American Mathematical Society (2008)
[10] Harrison, J.: HOL light: a tutorial introduction. In: Proceedings of Formal Methods in Computer-Aided Design, First International Conference, FMCAD’96, Palo Alto, California, USA, pp. 265-269 (1996)
[11] Hölldobler, S., Manthey, N., Philipp, T., Steinke, P.: Generic CDCL—a formalization of modern propositional satisfiability solvers. In: POS@ SAT, pp. 89-102 (2014)
[12] Huet, G., Herbelin, H.: 30 years of research and development around Coq. In: Principles of Programming Languages, POPL, pp. 249-250 (2014) · Zbl 1284.68517
[13] Kalbfleisch, J.D., Kalbfleisch, J.G., Stanton, R.G.: A combinatorial problem on convex n-gons. In: Proceedings of Louisiana Conference on Combinational Graph Theory Computing, Louisiana State University, Baton Rouge (1970) · Zbl 0223.52009
[14] Knuth, D.E.: Axioms and Hulls, LNCS, vol. 606. Springer, Berlin (1992) · Zbl 0777.68012
[15] Lammich, P.: Efficient verified (un)sat certificate checking. In: Proceedings of Automated Deduction—CADE-26—26th International Conference on Automated Deduction, Gothenburg, Sweden, LNCS. Springer (2017) · Zbl 06778407
[16] Marić, F., Formalization and implementation of modern SAT solvers, J. Autom. Reason., 43, 81-119, (2009) · Zbl 1187.68557
[17] Marić, F., Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theor. Comput. Sci., 411, 4333-4356, (2010) · Zbl 1208.68205
[18] Marić, F., A survey of interactive theorem proving, Zb. Rad., 18, 173-223, (2015)
[19] Morris, W.; Soltan, V., The Erdős-Szekeres problem on points in convex position—a survey, Bull. Am. Math. Soc., 37, 437-458, (2000) · Zbl 0958.52018
[20] Morris, W., Soltan, V.: The Erdős-Szekeres Problem. Springer, Cham (2016) · Zbl 1356.52008
[21] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002) · Zbl 0994.68131
[22] Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) Proceedings of Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, pp. 346-361. Springer, Berlin (2001) · Zbl 1005.68557
[23] Shankar, N.; Vaucher, M., The mechanical verification of a DPLL-based satisfiability solver, Electron. Notes Theor. Comput. Sci., 269, 3-17, (2011) · Zbl 1347.68307
[24] Suk, A., On the Erdős-Szekeres convex polygon problem, J. Am. Math. Soc., 30, 1047-1053, (2017) · Zbl 1370.52032
[25] Szekeres, G.; Peters, L., Computer solution to the 17-point Erdős-Szekeres problem, ANZIAM J., 48, 151-164, (2006) · Zbl 1152.52008
[26] Weber, T.: Efficiently checking propositional resolution proofs in Isabelle/HOL. In: Benzmüller, C., Fischer, B., Sutcliffe, G. (eds.) Proceedings of the 6th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, vol. 212, pp. 44-62 (2006)
[27] Weber, T., Integrating a SAT solver with an LCF-style theorem prover, Electr. Notes Theor. Comput. Sci., 144, 67-78, (2006) · Zbl 1272.68366
[28] Wenzel, M.: Isabelle/Isar—a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof—Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23). University of Bialystok (2007)
[29] Wetzler, N., Heule, M.J.H., Hunt, W.A.: Drat-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing—SAT 2014: 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, Proceedings, pp. 422-429. Springer, Cham (2014) · Zbl 1423.68475
[30] Wetzler, N.D., et al.: Efficient, mechanically-verified validation of satisfiability solvers. Ph.D. thesis, University of Texas, Austin, USA (2015)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.