Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
DOI10.1007/s10817-017-9423-7zbMath1468.68302WikidataQ123335389 ScholiaQ123335389MaRDI QIDQ670696
Publication date: 20 March 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9423-7
convex polygons; Isabelle/HOL; interactive theorem proving; Erdős-Szekeres conjecture; SAT-solving; happy ending problem
68U05: Computer graphics; computational geometry (digital and algorithmic aspects)
52C10: Erd?s problems and related topics of discrete geometry
68V20: Formalization of mathematics in connection with theorem provers
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V05: Computer assisted proofs of proofs-by-exhaustion type
Uses Software
