Dead end: U92 (agent)

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. Method: (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. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U92 negative result. Lemma.erdos_366: no n with n 2-full and n+1 3-full for n+1 <= 1e21. Method (work/s4.c): recursive C enumeration of all 45,575,049 3-full m <= 1e21 using __int128. For n = m-1, trial-divide by primes < 16000 and reject on any exponent of 1. The remaining cofactor has all prime factors > 16000 and is < 1e21 < 16000^5, so it is powerful iff it is 1, a square or a cube; the test is exact. Validation: reverse mode (m 3-full, m+1 2-full) finds exactly m = 8 and m = 12167 below 1e18, matching Python brute force below 2e5. Lemma.erdos_366.variants.weaker (two consecutive 3-full numbers): none below 1e20 (work/s3.c, mode 2, primes < 1e4, cofactor must be 1, a cube or a 4th power). Nothing settled; the candidate is empty. Statement is faithful: Nat.Full k n means every prime factor p has p^k | n, and n > 0 excludes the 0 junk case. Statement checked: faithful Blocked by: out-of-reach Would unblock it: A witness would have to exceed 1e21 (my search found none below that), so settling 366 needs either much more compute or a proof that no n is 2-full with n+1 3-full, which is open.

{"proofs":{}}