erdős #307

← #306 · #308 → (packet.json; erdosproblems.com)

Are there two finite sets of primes $P, Q$ such that $1 = p \in P \sum \frac{1}{p} q \in Q \sum \frac{1}{q} ?$

Open problem — our best result is machine-sealed: verified reduction, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · formalized (Lean) · 3 attempts

machinery: unit-fractions,prime-reciprocal-sums,p-adic-valuation-balance,finite-witness-search,consecutive-integer-window,divisor-numerator-divisibility,Egyptian-fractions

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

routes

verified computationpython:verify_307_barrier.py

congruence-barrier construction re-check (pinned tier: scripts/requirements-verifiers.txt)

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

the congruence-barrier construction verified

targets

the unconditional bound remains open.1

evidence

verified reduction

needs verification

Transfer from #306/#295: PROVEN equivalence -- #307 <=> a squarefree arithmetic-derivative 2-cycle M(P)'=M(Q), M(Q)'=M(P); exhaustive negative search (no cycle in first 17-24 primes).

Used the M(S)=prod(S), A(S)=sum M(S)/p bookkeeping from #306/#295. AM-GM screen: a solution needs union reciprocal mass >=2 (first 58 primes insufficient, 59 exceed). Exhausted 131054 subsets of first 17 primes, segments to size 24 -- no cycle. SCOPE: exact reduction + bounded negative search; #307 open. Official page records a sharper >=60-prime bound.

verified reduction

machine-sealed

Erdős #307 is PROVEN EQUIVALENT (Lean, lake-build green, no sorry/axiom) to the existence of a squarefree ARITHMETIC-DERIVATIVE 2-CYCLE: finite prime sets P,Q with M(P)'=M(Q) and M(Q)'=M(P), where M(S)=prod(S) and M(S)'=sum_{p in S} M(S)/p (the arithmetic derivative of squarefree M(S)). The reciprocal-sum witness condition is exactly A(S)/M(S)=sum 1/p, verified arithmetically. This is a VERIFIED REDUCTION, not a settlement: whether such a 2-cycle exists is OPEN (exhaustive negative search found none in the first 17-24 primes; no nonexistence proof). Known easy bound: sum_{p in P∪Q} 1/p >= 2, so |P∪Q| >= 60.

Codex reduction + Lean module lean/Vela/Erdos307.lean (imported in Vela.lean), Opus-banked after independently re-running `lake build Vela.Erdos307` (green) and re-checking the reduction identities. The module proves squarefree-derivative-2-cycle => the product-one reciprocal-sum witness, plus the fixed-union discriminant-square obstruction for finite candidate filters. Forward: a structural nonexistence proof of the 2-cycle would settle #307 negatively; the obstruction is compact enough for a possible Lean finite-reduction path.

depends on (the wall): OPEN: existence of a squarefree arithmetic-derivative 2-cycle (M(P)'=M(Q), M(Q)'=M(P)); exhaustive search found none but no nonexistence proof. A finite/structural obstruction would settle #307.

lake build Vela.Erdos307 green (no sorry/axiom), re-run by Opus; reduction identities sum 1/p = A(S)/M(S) and A(S)=arithmetic derivative verified on sample prime sets.

obstruction map

machine-sealed

Erdos #307: finite local obstructions (parity, mod-8, per-prime quadratic-residue, avoidance of primes 3 mod 4) provably cannot bound the primes in a squarefree arithmetic-derivative 2-cycle. Constructively (verified): for any target one builds an arbitrarily large prime set U with all r = 1 mod 8 plus a constructed prime t such that N/r (N=prod U) is a quadratic residue mod every r in U and A(U) = |U| mod 8 is free, with reciprocal mass > 2. Hence the decisive control point is the GLOBAL double-square lemma (A(U) +/- 2 M(U) both perfect squares), not its finite congruence shadows. This maps the barrier; it does not settle the problem.

{"result_type":"barrier / no-go for the congruence approach","construction":"primes r = 1 mod 8 via Dirichlet; quadratic reciprocity makes prod eps_i = +1 so N/r is a QR mod every r; A(U) = |U| mod...

depends on (the wall): scripts/verify_307_barrier.py; lean/Vela/Erdos307.lean

scripts/verify_307_barrier.py + Crossref citation checks

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

As far as is currently known, **no such pair of finite prime sets is known**. In fact, this is a recorded open problem of Erdős (often cited as **Erdős Problem #307**). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_307 : answer(sorry) ↔ ∃ P Q : Finset ℕ, (∀ p ∈ P, p.Prime) ∧ (∀ q ∈ Q, q.Prime) ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)

formal-conjectures/307.lean ↗

Vela formalization: Erdos307.lean (sorry-free)

links

related: #295 · #306 · #385

status

open