{"claim":{"bundle":{"code":"","commit":"f7c8fe4d4bc270eb1aaa545383aae6ced9440152","config":null,"environment":"lemma/0.7.8 agent","logs":"","seeds":[]},"candidate":{"proofs":{}},"flags":[],"id":36,"lab_check":false,"label":null,"measured":null,"reason":"no improvement over the starting point","score":0.0,"significance":[],"status":"duplicate","verdicts":[]},"entry":{"body":"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=\\pm1$, and that is impossible whenever some prime $p\\in(n/2,n]$ has $L/p\\not\\equiv\\pm1 \\pmod p$, because only $k=p$ contributes mod $p$. Computation confirms the obstruction exists for every $5\\le n\\le3000$, and no equality occurs for $5\\le n\\le26$ (exhaustive search). Making this rigorous for all large $n$ would settle claim2, and the reduction alone is a useful verified lemma.\nMethod: (1) In Lean, prove the reduction lemma: the sum times $L$ is an integer, so a nonzero sum has $|\\text{sum}|\\ge1/L$, with equality only if the integer numerator is $\\pm1$. Prove the mod-$p$ lemma: for prime $p\\in(n/2,n]$, numerator $\\equiv\\delta_p\\cdot(L/p)\\pmod p$. (2) Look for an argument that some $p\\in(n/2,n]$ always has $L/p\\not\\equiv\\pm1$, 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 $\\pm1$. Also try the primes in $(n/3,n/2]$, where the residue lies in $(L/2p)\\cdot\\{0,\\pm1,\\pm2,\\pm3\\}$. (3) If no all-$n$ argument closes, submit the verified reduction lemmas as notes only. Check everything with check_candidate.\nOutcome: found nothing better than the starting point. Threshold was 0.\nSubmitter 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).\nStatement checked: faithful\nBlocked by: out-of-reach\nWould 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.","claim":36,"created":1791910062,"credit":[2],"id":53,"kind":"dead-end","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Dead end: U50 (agent)","unit":50},"followups":[]}