Dead end: U50 (agent)

Lemma.erdos_317.variants.claim2 (eventually, every nonzero $|\sum _{k\le n}{\delta }_k/k|$ is $>1/\mathrm{lcm}(1..n)$) reduces to a local statement. Equality can only happen when $\sum {\delta }_{k}L/k=\pm 1$, and that is impossible whenever some prime $p\in (n/2,n]$ has $L/p\not\equiv \pm 1(\mathrm{mod}p)$, because only $k=p$ contributes mod $p$. Computation confirms the obstruction exists for every $5\le n\le 3000$, and no equality occurs for $5\le n\le 26$ (exhaustive search). Making this rigorous for all large $n$ would settle claim2, and the reduction alone is a useful verified lemma. Method: (1) In Lean, prove the reduction lemma: the sum times $L$ is an integer, so a nonzero sum has $|\text{sum}|\ge 1/L$, with equality only if the integer numerator is $\pm 1$. Prove the mod-$p$ lemma: for prime $p\in (n/2,n]$, numerator $\equiv {\delta }_p\cdot (L/p)(\mathrm{mod}p)$. (2) Look for an argument that some $p\in (n/2,n]$ always has $L/p\not\equiv \pm 1$, for example by pairing two primes $p<q$ in $(n/2,n]$ and using $L/p\cdot p=L/q\cdot q$ to derive a contradiction when both residues are $\pm 1$. Also try the primes in $(n/3,n/2]$, where the residue lies in $(L/2p)\cdot \{0,\pm 1,\pm 2,\pm 3\}$. (3) If no all-$n$ argument closes, submit the verified reduction lemmas as notes only. Check everything with check_candidate. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U50: I checked the statement by elaboration. (k+1) is ↑↑k+1 in ℚ and the bound is 1/↑((Icc 1 n).lcm id) in ℚ, so it is faithful. I verified a reduction in Lean (it compiled under check_candidate, with only the main theorem's sorry left): erdos317_mul_sum_int says lcm(1..n)·Σδ_k/(k+1) ∈ ℤ for integer δ, and erdos317_ge says that for all n and δ∈{-1,0,1}^n, a nonzero |sum| is ≥ 1/lcm(1..n). Claim2 is therefore equivalent to: eventually L·Σδ_k/k ≠ ±1. The mod-p obstruction (prime p∈(n/2,n] with L/p ≢ ±1 mod p, which held computationally for 5≤n≤3000) has no all-n proof; pairing primes gives no contradiction. The proof file is in scratch/r.lean of this unit; it is not submitted because the main theorem still uses sorry. I submitted an empty candidate (nothing settled). Statement checked: faithful Blocked by: out-of-reach Would unblock it: Proving that for every large n some prime p in (n/2,n] has lcm(1..n)/p ≢ ±1 (mod p), or finding another obstruction to L·Σδ_k/k = ±1, which looks as hard as the open problem itself.

{"proofs":{}}