A certified lower bound for Erdős's minimum-overlap problem

An open, from-scratch, fully rigorous independent re-certification of White's (2023) lower bound for Erdős Problem #36 (the minimum-overlap problem), together with an independent verifier. The certificate is computed in exact-rational and interval (mpmath.iv) arithmetic, with no floating-point-accuracy assumption and no proprietary solver in the trusted path, and yields

μ ≥ 0.3792959

(White's published value is 0.379005).

Use of AI. This work is LLM-assisted and openly so. The code, the from-scratch re-derivation of White's SOCP, the 4th-moment identity, and the documentation were developed with substantial assistance from Claude (Anthropic), as an experiment. The language model's fallibility is contained by design: every numerical claim is a certificate that an independent, separately written verifier re-checks in exact/interval arithmetic — correctness rests on the published proofs, mpmath.iv + Python integers, and the checker, not on the tools that produced the code.

⚠️ This result has been superseded — please read first

A stronger lower bound was posted one day before this repository. On 2026-06-29, an independent certificate establishing

c_E > 0.38055470

for Erdős #36 was published at https://github.com/Leeham06972452/erdos-36-lower-bound. That value substantially exceeds the one certified here (0.3792959) and White's 0.379005. Combined with the known upper bound, it gives 0.38055470 < μ ≤ 0.38092685.

We independently verified that stronger result. We audited its proof note and its Arb/python-flint verifier line by line, found no soundness gap, and re-ran the full 172-bin ball-arithmetic verification ourselves — it certifies c_E > 0.38055470 correctly, reproducing the author's reported figures to ~20 digits. Details and reproduction in docs/INDEPENDENT_VERIFICATION.md.

This repository is therefore not a state-of-the-art result. It is kept as an open, self-contained archive of an independent, fully rigorous re-certification of White's bound and the methodology behind it. The mathematics is written up in docs/METHOD.md.

For $A \sqcup B = {1,\dots,2n}$ with $|A| = |B| = n$, let $M(n) = \min_{A} \max_k \bigl|{(a,b)\in A\times B : b-a = k}\bigr|$. The minimum-overlap constant is $\mu = \lim_{n\to\infty} M(n)/n$. A theorem of Swinnerton-Dyer (see Haugland 1996) recasts $\mu$ as the optimum of a continuous variational problem $\mu = \inf_f \lVert M\rVert_\infty$, where $f:[-1,1]\to[0,1]$, $\int f = 1$, $g = 1-f$, and $M(x)=\int_{-1}^1 f(t),g(x+t),dt$ on $[-2,2]$.

White (2023, arXiv:2201.05704) relaxes this to a second-order cone program (SOCP) and certifies $\mu \ge 0.379005$ numerically — solving with IBM CPLEX and verifying the dual feasible point against a worst-case double-precision floating-point error bound (Higham 1993). This project re-derives White's relaxation from scratch and certifies it rigorously (no floating point in the trusted path, no proprietary solver), with an independent verifier. The full mathematical write-up is in docs/METHOD.md.

• Erdős Problem #36 (minimum overlap): https://www.erdosproblems.com/36
• Discussion forum thread: https://www.erdosproblems.com/forum/thread/36
• Stronger lower bound c_E > 0.38055470 (2026-06-29), independently verified here: https://github.com/Leeham06972452/erdos-36-lower-bound — see docs/INDEPENDENT_VERIFICATION.md.
• White (2023), the bound re-certified here: https://arxiv.org/abs/2201.05704

code/
  certify_socp_exact.py      # THE certifier (trusted path): exact-rational + mpmath.iv interval
                             #   arithmetic, rigorous interval cos/sin (no libm assumption),
                             #   residual-tolerant weak conic duality, Farkas infeasibility.
  verify_socp.py             # Independent verifier: separate assembly/arithmetic/cos-sin code.
  verify_certificate.py      # Standalone portable verifier for the even-LP certificate.
  certify_white.py           # Exact-rational dual certification of White's even LP -> mu >= 0.375123.
  reproduce_white.py         # White's LP (Prop 8) and full convex program (Prop 9), re-encoded.
  verify_haugland.py         # Reproduces Haugland's upper-bound step functions in exact arithmetic.
  certify_convex.py          # Earlier cvxpy-lowered certifier (<=16-ulp FP assumption); cross-check.
  tests/test_verify_haugland.py
  experiments/
    socp_region_cover.py     # Gapless cover of the residual region -> mu >= 0.3792959.
    socp_full_cover.py       # (experimental, compute-heavy) cover of the full outer box.
    identity_symbolic_proof.py  # CAS proof of the 4th-moment identity (two independent ways).
    moment4_t_trend.py          # asymptotic redundancy of the moment cut (lift ~ 0.019/sqrt(T)).
    moment4_cell_sweep.py, moment4_identity_check.py, moment4_probe.py
docs/
  METHOD.md                  # the mathematics: method, lemmas + proofs, trust model, moment identity.
  INDEPENDENT_VERIFICATION.md# our independent verification of the stronger 0.38055470 bound.
  outer_box_bounds.md        # elementary derivation of the outer parameter box.
  references.bib             # bibliography.
  LICENSE                    # CC-BY-4.0 (prose/documentation).
certs/
  even_lp_certificate.json   # the even-LP certificate (checked by verify_certificate.py).

Python 3.10–3.13.

git clone https://github.com/occisn/erdos-36-certified-lower-bound
cd erdos-36-certified-lower-bound
python3 -m venv venv && . venv/bin/activate
pip install -r requirements.txt

The trusted certification path (certify_socp_exact.py) uses only numpy, scipy, mpmath, and Python integers/Fraction. clarabel is used only to propose candidate dual points (its output is never trusted — every bound is re-derived in exact/interval arithmetic). cvxpy/sympy are used by the cross-check and the symbolic identity proof.

Performance note. This certifier is essentially single-core-bound. If you parallelise covers across processes, pin each to one compute thread (RAYON_NUM_THREADS=1 OMP_NUM_THREADS=1 OPENBLAS_NUM_THREADS=1 MKL_NUM_THREADS=1) and run more processes — multithreaded solves contend and stall under load.

μ ≥ 0.3792959 is the minimum of a gapless divide-and-conquer cover of White's residual region $0 \le E(M^) \le 0.06$, $0.33 \le c_1^ \le 0.45$, $|d_1^*| \le 0.02$ at full resolution N, T, R = 28000, 7000, 10.

python3 code/experiments/socp_region_cover.py          # full run, ~70 min single-core
python3 code/experiments/socp_region_cover.py quick     # coarse T=2000 smoke test (minutes)

python3 code/verify_socp.py            # validate the verifier against the fast path (T=2000)
python3 code/verify_socp.py FULL 7000 10   # re-verify the region-cover boxes at full resolution
python3 code/verify_certificate.py     # checks certs/even_lp_certificate.json

A new exact 4th-moment identity for the overlap functional (with $m_k = \int_{-1}^1 t^k f$):

$$\int_{-2}^{2} x^4 M(x),dx ;=; \tfrac{2}{5} + 4 m_2 - 6 m_2^2 + 8,E(f),m_3,$$

in which the $m_4$ terms cancel between the two double integrals (CAS-proven two independent ways). The associated 4th-moment cut lifts the most binding cell by an exactly certified $+1.75\times10^{-4}$ at $T=7000$, but the lift decays as $\approx 0.019/\sqrt{T}\to 0$: the cut — and Fourier-basis moment cuts generally — are asymptotically redundant, improving only finite-truncation bounds, not the limit. See docs/METHOD.md §7.

python3 code/experiments/identity_symbolic_proof.py    # CAS proof of the 4th-moment identity
python3 code/experiments/moment4_t_trend.py            # the cut's asymptotic redundancy (lift vs T)
python3 code/certify_white.py                          # even-only cert -> mu >= 0.375123
python3 code/reproduce_white.py                        # White's LP + full convex program
python3 code/verify_haugland.py                        # Haugland upper-bound step functions
python3 -m unittest discover -s code/tests

The certificate is a rigorous lower bound by residual-tolerant weak conic duality: for a dual-feasible z ∈ K* with residual r = Aᵀz + q, μ ≥ Ω* ≥ −bᵀz − Σⱼ xⱼᵐᵃˣ|rⱼ|, evaluated in exact Fractions and rigorous mpmath.iv intervals (the irrationals π, cos, sin are enclosed with no libm-accuracy assumption), and floored to an exact rational.

• Trusted: the proofs in docs/METHOD.md, exact-rational + mpmath.iv arithmetic, Python integers, and the small independent verifier.
• Not trusted, by design: the SOCP solver (only proposes a candidate z), floating-point arithmetic (not used in the bound), and the language model that wrote the code (every certificate is independently machine-checkable).
• Assumed/cited, not reproven: the discrete→continuous reduction (Swinnerton-Dyer, via Haugland 1996), White's Proposition 9, and — for the residual region — White's numerical divide-and-conquer pass.
• What it is not: a Lean/formal proof, and not an unconditional from-scratch re-derivation of the whole chain.

• Established: an open, from-scratch, fully rigorous re-certification of White's relaxation (exact-rational + interval, no FP assumption, no proprietary solver), yielding μ ≥ 0.3792959, with an independent verifier; a new exact 4th-moment identity (CAS-proven); and a theorem that the associated moment cut — and Fourier-basis moment cuts generally — are asymptotically redundant.
• Reused/cited, not ours: the SOCP relaxation (White's Prop 9) and the (SD)+(P9) reduction. We re-encode; we do not invent or reprove these.
• Not claimed: that the limiting constant μ is moved by a new idea (the moment cut is asymptotically redundant); that the result is self-contained (it relies on White's divide-and-conquer pass for the part of the parameter box outside the residual region); and — as the notice above makes explicit — this is not the best known bound (see the stronger, independently verified 0.38055470 result).