Dead end: U68 (agent)

Lemma.erdos_931.variants.exists_prime is a ∀-statement, so one explicit counterexample gives a short disproof: decide/norm_num on primeFactors of two concrete products, plus a primality check of every integer in $[n_1,n_2]$. A counterexample must sit inside a prime gap, because $(n_1,n_2+k_2]$ has no prime in $[n_1,n_2]$, and a prime in $B_2$ cannot divide anything in $B_1$. Every prime $r$ dividing the two blocks must also satisfy $r<n_2+k_2-n_1\le g+k_2$, where $g$ is the gap length. So both blocks consist of $(g+k)$-smooth consecutive integers inside a maximal-type prime gap. Only record gaps can host one, which makes a search to ${10}^{12}$ and beyond feasible by checking smoothness inside large gaps only. My Python scan this unit found none for $n_2<3\cdot {10}^5$, $k_1\le 12$. Method: (1) C program: segmented sieve up to ${10}^{10}$ or more. For each prime gap $(p,q)$ with $q-p\ge 7$, take the largest prime factor of every integer in the gap with a smallest-prime-factor sieve per segment. Keep only maximal runs of $\ge 3$ consecutive integers whose prime factors are all $<q-p+12$. Inside those runs, test equality of the radical unions for $k_2\le k_1\le 12$ and $n_1+k_1\le n_2<q$. (2) In parallel, try to prove in Lean the cheap structural lemma that every prime factor of either block is $<n_2+k_2-n_1$, as a verified partial result. (3) On a hit, write the disproof: intro h; have := h k1 k2 n1 n2 ..., discharge primeFactors equality with decide or Nat.primeFactors simp lemmas, and refute the prime by interval_cases plus norm_num. Otherwise post the verified range. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U68 negative result for Lemma.erdos_931.variants.exists_prime. Reduction: the whole interval [n1, n2+k2] must be prime-free, because a prime in either block cannot divide anything in the other block. Each shared prime r satisfies r < n2+k2-n1 <= gap length, which is < 2000 below 1e15. So both blocks are runs of >= 3 consecutive 2000-smooth numbers inside one prime gap. C program (work/s.c): segmented prime sieve plus a log-sieve smoothness filter, exact factorisation of the candidates over primes < 2000 stored as bitmasks, then every (n1,k1,n2,k2) inside each gap is tested with k1, k2 unbounded (only limited by the smooth run length). Validated against Python brute force with the gap condition removed, n < 1500, k1 <= 8: identical 151 hits. Result: no counterexample with n2+k2 < 2*10^11 (chunks overlap by 3000 so gaps that cross chunk boundaries are covered). Nothing was settled; the candidate is empty. Statement checked: faithful Blocked by: out-of-reach Would unblock it: The disproof needs a counterexample above 2e11, which would need a faster sieve or many more CPU-hours. Proving the statement needs a real theorem ruling out equal radicals of consecutive blocks inside a single prime gap.

{"proofs":{}}