{"claim":null,"entry":{"body":"Hypothesis: Lemma.erdos_366 (∃ n>0, Nat.Full 2 n ∧ Nat.Full 3 (n+1)) is existential, so one explicit n settles it, with a Lean proof by norm_num/decide on primeFactors (Nat.Full k n = ∀ p ∈ n.primeFactors, p^k ∣ n, which I printed in T119). 3-full numbers are sparse: about $c X^{1/3}$ of them up to X, which is roughly $10^7$ below $10^{20}$. So enumerating m = n+1 over 3-full numbers and testing whether m−1 is powerful reaches far beyond naive search. No lab entry has searched this.\nMethod: (1) C with __int128: enumerate the 3-full m ≤ X (X = 10^18, then 10^20 if time allows) recursively as products of p^e with e≥3. (2) For each m, test n=m−1 for powerfulness. First trial-divide by primes < 2000 and reject as soon as some prime divides exactly once, which removes almost all candidates. For survivors, the cofactor r must be powerful with all prime factors >2000: accept if r=1, or r is a perfect square or cube, or r = a^2 b^3 found via Pollard rho. (3) Validate on the known reverse pair (8 is 3-full, 9 is 2-full) and with brute force below 10^7. (4) On a hit, write the Lean proof: `⟨n, by norm_num, ...⟩` with explicit factorizations via Nat.primeFactors lemmas, then check_candidate. Otherwise post the verified bound to chat. Threshold 0.\nThreshold: 0 (must reach)\nEstimated cost: 60 min\nWhy it's new: No notebook entry or chat message touches 366 (I checked N47, N54, N55, N57, N58 and the summary N75). This is a sparse-enumeration search on an existential statement, unlike the universal-statement searches in N54, N55 and N58.\nRelated: N47, N54, N55, N58, N75","claim":null,"created":1791927851,"credit":[2],"id":76,"kind":"proposal","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Proposal U92: Lemma.erdos_366 (∃ n>0, Nat.Full 2 n ∧ Nat.Full 3 (n+1)) is existential, so one explicit n…","unit":92},"followups":[]}