More Like this

1. Formal Verification of the Empty Hexagon Number

   https://doi.org/10.4230/LIPIcs.ITP.2024.35  

   Subercaseaux, Bernardo; Nawrocki, Wojciech; Gallicchio, James; Codel, Cayden; Carneiro, Mario; Heule, Marijn J_H (September 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)

   Bertot, Yves; Kutsia, Temur; Norrish, Michael (Ed.)

   A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SAT-based results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computer-assisted proofs. 

   more » « less
2. CONJECTURES ABOUT SIMPLE DYNAMICS FOR SOME REAL NEWTON MAPS ON ℝ2

   https://doi.org/10.1142/S0218348X19500993  

   DE LEO, ROBERTO (September 2019, Fractals)

   We collect from several sources some of the most important results on the forward and backward limits of points under real and complex rational functions, and in particular real and complex Newton maps, in one variable and we provide numerical evidence that the dynamics of Newton maps [Formula: see text] associated to real polynomial maps [Formula: see text] with no complex roots has a complexity comparable with that of complex Newton maps in one variable. In particular such a map [Formula: see text] has no wandering domain, almost every point under [Formula: see text] is asymptotic to a fixed point and there is some non-empty open set of points whose [Formula: see text]-limit equals the set of non-regular points of the Julia set of [Formula: see text]. The first two points were proved by B. Barna in the real one-dimensional case. 

   more » « less
3. Reconstruction of the Crossing Type of a Point Set from the Compatible Exchange Graph of Noncrossing Spanning Trees

   https://doi.org/10.1007/978-3-030-14085-4_19  

   Marcos Oropeza, Csaba D. (February 2019, International Conference on Discrete Geometry for Computer Imagery)

   Let P be a set of n points in the plane in general position. The order type of P specifies, for every ordered triple, a positive or negative orientation; and the x-type (a.k.a. crossing type) of P specifies, for every unordered 4-tuple, whether they are in convex position. Geometric algorithms on P typically rely on primitives involving the order type or x-type (i.e., triples or 4-tuples). In this paper, we show that the x-type of P can be reconstructed from the compatible exchange graph G1(P) of noncrossing spanning trees on P. This extends a recent result by Keller and Perles (2016), who proved that the x-type of P can be reconstructed from the exchange graph G0(P) of noncrossing spanning trees, where G1(P) is a subgraph of G0(P) . A crucial ingredient of our proof is a structure theorem on the maximal sets of pairwise noncrossing edges (msnes) between two components of a planar straight-line graph on the point set P. 

   more » « less
4. Convex polytopes in restricted point sets in R^d

   https://doi.org/10.19086/aic.2025.1  

   Bukh, Boris; Zichao, Dong (January 2025, Advances in Combinatorics)

   For a finite point set P⊂R^d, denote by diam(P) the ratio of the largest to the smallest distances between pairs of points in P. Let c_{d,α}(n) be the largest integer c such that any n-point set P⊂R^d in general position, satisfying diam(P)<αn^{1/d}, contains an c-point convex independent subset. We determine the asymptotics of c_{d,α}(n) as n→∞ by showing the existence of positive constants β=β(d,α) and γ=γ(d) such that βn^{(d−1)/(d+1)}≤c_{d,α}(n)≤γn^{(d−1)/(d+1)} for α≥2. 

   more » « less
5. Dynamic Convex Hulls for Simple Paths

   https://doi.org/10.4230/LIPIcs.SoCG.2024.24  

   Brewer, Bruce; Brodal, Gerth Stølting; Wang, Haitao (June 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik)

   Mulzer, Wolfgang; Phillips, Jeff M (Ed.)

   We consider two restricted cases of the planar dynamic convex hull problem with point insertions and deletions. We assume all updates are performed on a deque (double-ended queue) of points. The first case considers the monotonic path case, where all points are sorted in a given direction, say horizontally left-to-right, and only the leftmost and rightmost points can be inserted and deleted. The second case, which is more general, assumes that the points in the deque constitute a simple path. For both cases, we present solutions supporting deque insertions and deletions in worst-case constant time and standard queries on the convex hull of the points in O(log n) time, where n is the number of points in the current point set. The convex hull of the current point set can be reported in O(h+log n) time, where h is the number of edges of the convex hull. For the 1-sided monotone path case, where updates are only allowed on one side, the reporting time can be reduced to O(h), and queries on the convex hull are supported in O(log h) time. All our time bounds are worst case. In addition, we prove lower bounds that match these time bounds, and thus our results are optimal. 

   more » « less