math.OCJun 2, 2026

Optimizing Explicit Unit-Distance Lower-Bound Certificates

Authors: Michael T. M. Emmerich

Organizations: Faculty of Information Technology, University of Jyväskylä, Finland.

Abstract

The 2026 disproof of Erdős's unit-distance conjecture and Sawin's quantitative refinement show that the maximum number u(n)u(n) of unit distances among nn planar points can exceed n1+εn^{1+\varepsilon} for a fixed positive ε\varepsilon. Sawin's explicit bound gives more than n1.014n^{1.014} unit distances for arbitrarily large nn and exposes integer parameters whose choice is not fully optimized. This report treats Sawin's parameter selection as a nonlinear integer optimization problem and develops an open-source Python optimization and verification pipeline for certificates involving prime sets TT and SQS_Q, integer multiplicities k(p)k(p), and a rationally encoded real parameter RR. After reproducing Sawin's certificate with δ=0.014114δ=0.014114\ldots, the pipeline yields improved certificates with the same TT. We develop a tailored integer evolution strategy achieving a certificate with δ=0.015263δ=0.015263\ldots and supporting the cautious statement u(n)>n1.0152u(n)>n^{1.0152} for arbitrarily large nn. For extended ramified prime ranges, the Emmerich--Cordella certificate obtained with the same framework reports u(n)>n1.031u(n)>n^{1.031} for #T=67\#T=67, illustrating the importance of enlarging TT. Very recent MathOverflow discussions, brought to the author's attention as of version~4, report further improvements, including certificates above δ>0.035δ>0.035 and beyond δ>0.036δ>0.036. Some of these improvements may rely not only on larger prime ranges but also on modified constraint systems and additional degrees of freedom that deviate from Sawin's original formulation. Beyond this application, the work illustrates how randomized optimization heuristics can improve, verify, and refine explicit certificates for combinatorial geometry through nonlinear integer optimization.

Explore similar work

Aug 8, 2026math.CO

Exact Zarankiewicz Values On Two Finite Frontier Slices

The Zarankiewicz number Z(m,n,s,t) is the maximum number of edges in a bipartite graph with parts of orders m and n containing no copy of Ks,t. We give one combined, certificate-based computer-assisted proof for two finite slices and a corrected neighboring frontier: Z(12,n,3,3) = 6n (18 <= n <= 22), Z(13,22,3,3) = 137, Z(13, 18, 3, 3) = 116, Z(14, 18, 3, 3) = 124, Z(15,18,3,3) = 132, Z(14, 17, 3, 3) = 118, Z(15, 17, 3, 3) = 126, 132 <= Z(16,17,3,3) <= 133. The load-bearing new upper bounds are the exact 12 x 18 and 13 x 18 certificate packages. Their orbit certificates exclude every hypothetical matrix at the next edge count. Deletion lemmas and explicit witnesses close four neighboring cells, while the 16 x 17 entry is deliberately reported as an interval because only its 132-edge lower witness and the published 133 upper bound are certified here. Separately, the 13 x 22 proof excludes 138 ones by reducing to 83 degree profiles, rationally separating 77 of them, and eliminating the remaining six by marked-row congruences, leave enumeration, modular Gram tests, and exact Farkas certificates. All accepted claims are replayed by standard-library Python and exact integer/rational arithmetic; floating-point optimization is used only to discover certificates.
Koyar Afrasyab
Jun 4, 2026cs.SC

A Finite Certificate for the Positive n=9 Vasc Inequality

We prove the positive-real n=9n=9 case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all 8!=403208!=40320 sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has 3681536815 coefficient leaves, 22362236 ordinary Polya multiplier leaves, and 12691269 AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.
Dakai Guo, Ruichen Qiu, Yichuan Cao +1
Apr 8, 2026cs.CC

Descent Before Hardness: Orbit-Gap Obstructions in Exact Certification

Tractability tests are often computed from input syntax: support-graph treewidth, local coefficient patterns, backdoor tests, or action-count bounds. Before such a test can be lower-bounded or made algorithmic, it must define a predicate on the exact-certification problem itself. Equivalent presentations must receive the same verdict. The semantic object is the correctness quotient, whose classes are states with the same correct outputs. Correctness-preserving presentation moves generate closure orbits. A target that changes inside one closure orbit has an orbit gap and fails descent. Exact closure-invariant classification is possible exactly when the positive and negative orbit hulls are disjoint; the positive hull is then the least exact classifier, and computable orbit representatives make the classifier algorithmic. The results separate three layers. The descent layer gives orbit-gap obstructions for raw local syntax, raw action and coordinate counts, and raw support-graph predicates. The post-descent complexity layer applies ordinary reductions to descended objects: graph-predicate lower bounds transfer through action-gap graph extraction, and Action-Gap-Treewidth is NP-complete when the width bound is part of the input. The certification layer asks whether a proxy descends: for split proxies bφ(z)b\wedge\varphi(z), SAT reduces to non-descent and UNSAT reduces to descent. Positive regimes use quotient-preserving normalizations or catalogues before model checking; bounded quotient size, bounded full Gaifman treewidth of the constructed quotient, sparse unary-gap certificates, and strict-margin perturbation balls give explicit cost bounds after quotient construction.
Tristan Simas