Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The optimal constant of Problem 36, the minimum overlap constant, which the claim calls , satisfies
The claim was submitted to erdosproblems.ai on 2026-10-09 by Justin Wetch as a partial result, with its proof packet and verification code in the release linked above. Both bounds are computer-assisted and use White's continuous formulation: for on with and , both extended by zero, put ; then . For the lower bound, kernel inequalities , where , give for certified ; a case split of into central, transition and outer intervals, with a separate argument near , covers , and the certificates were replayed with Arb and with separately implemented rational and dyadic arithmetic. For the upper bound, an explicit rational step density on 14,337 cells has exact overlap peak , checked at all 86,017 shift knots by two exact methods, and a rounding and balancing argument carries the density back to partitions of with an error. The method is taken from the claim and the release's README. The lower bound lies above the refereed of White (claim page) and above the claimed of Kim and Pilanci (claim page), of Price (claim page) and of Drynshock (claim page). The upper bound lies below the claimed of TTT-Discover, the erdosproblems.com record (claim page), and of Russell (claim page).
Submission note. Posted to erdosproblems.ai as a proof claim by the account Justin Wetch on 9 October 2026, listing no tools. Its title, scope, summary and body, in that order:
Computer-assisted bounds for the minimum-overlap constant: 0.380627425 < μ < 0.3808585738345707361812673
Improved lower and upper bounds for the asymptotic minimum-overlap constant in Erdős problem #36:
0.380627425 < μ < 0.3808585738345707361812673.
The lower bound applies to every admissible measurable density; the upper bound is witnessed by an explicit rational step density. The exact value of μ remains undetermined.
The Fourier-analytic formulation builds on Ethan Patrick White's work. The cited public lower- and upper-bound certificate packages and public EinsteinArena construction data supply prior methods, implementations and baselines; the supporting packet records source versions and provenance.
The claim is limited to the displayed global interval. Stronger mean-zero experiments included as research history are not claimed as global bounds. Original and fresh local verification have passed; external mathematical review is requested.
Proof packet filename: minimum-overlap-final-627425.zip
SHA-256: 0031f6179312299e4d5934c8ed21dbf710b92f78421fcd0190988baed763432a
Let be the minimum, over partitions with , of , and let .
Use the equivalent continuous formulation: on , , and on that interval, with both functions extended by zero. Put . Then .
Lower bound. Fourier and phase-averaged Gram inequalities give universal kernel inequalities , where . Writing , certified upper bounds with give on the covered cases, where . The transition cases strengthen this return using the same physical odd profile : its boundary value, reflection identity, 1-Lipschitz bound and moment identity yield rational flow certificates with every residual and covariance error charged explicitly.
The central case covers by a separate exact radius deduction from executions at . Central, transition and outer intervals cover all of . Their finite collection of strict margins gives a uniform bound .
The lower checkpoint passed a complete fresh-copy replay with Arb and separately implemented rational/dyadic arithmetic, exact coverage auditing, and three control suites. Its 115 frozen input files remained unchanged. Numerical optimizer output is used only to propose certificates.
Upper bound. An admissible rational step density on 14,337 nonuniform cells has exact overlap peak
Two exact arithmetic methods verified its mass, box constraints and all 86,017 shift knots. The overlap is affine between endpoint-difference knots, so these checks cover every real shift. For the return to discrete partitions, hold this finite step density fixed, independently round its sampled values, and balance the two parts. Bounded-differences estimates control all shifts simultaneously, and the rounding and balancing errors are . Dividing by and taking the limit gives
The supporting material contains the analytic proofs, exact certificates, implementations, dependency manifests and executed original/fresh verification reports. Start with README.md and TECHNICAL_NOTE.md. In the repository, run verify_repository.py for integrity checks and follow the reproduction instructions for the mathematical replays. The release ZIP contains the complete research packet and its verify_packet.py integrity checker.
These are computer-assisted bounds, without proof-assistant formalization or external peer review.
Covers. Both bounds: . The claim does not determine .
Depends on. White's claim page: both bounds are proved for White's continuous formulation, so its equivalence with the discrete constant, with the cautions recorded there, is an input to the claim.
Standing. Claimed. erdosproblems.ai lists the claim as unreviewed, with no comments, accessed 2026-10-15. The erdosproblems.com label was OPEN and its commentary, last edited 23 January 2026, does not mention the claim. The claim states that it has no proof-assistant formalization and no outside review, and none is known.