Mandatory source/status audit, two-encoding bounded harness validation, adversarial audit of the 13 displayed OEIS A076445 terms, and construction of a fail-closed witness checker.

isolated adversarial reconstruction

Separate membership and factorization checks from exhaustive completeness; reconstruct finite claims using materially different exact encodings and reject the OEIS interval inference without a cover artifact.

Hypothesis: The canonical a^2*b^3 generator and an independent prime-exponent classifier agree on every powerful integer through 10^6, while exact factor audits validate the 13 displayed A076445 terms but cannot certify that the displayed prefix is complete.

Test: Require exact list equality on [1,10^6], known controls, and exact prime-factor checks of all displayed OEIS endpoints and middles; separately inspect the source trail for a completeness artifact.

The mandatory baseline is complete, the verification contract is now fail-closed, reusable bounded and witness checkers exist, and the evidentiary gap behind the headline computational bound has been isolated without inflating the bounded results.

• A hypothetical triple start is congruent to 7, 27, or 35 modulo 36; this is the known Beckon restriction.
• Exactly 2,027 powerful integers occur in [1,10^6]; independent exact encodings agree, and no powerful triple occurs there.
• For each of the 13 displayed A076445 values n, both n and n+2 are powerful and n+1 is not.
• The inspected public artifacts do not independently certify that those 13 values exhaust all distance-two powerful pairs below the largest displayed value.

• .proof-experiments/20260720-203815-fbb4dd: canonical enumeration through 10^6, return code 0.
• .proof-experiments/20260720-203822-2f8c58: independent SPF exponent reconstruction exactly matched all 2,027 terms and controls.
• .proof-experiments/20260720-204059-94e77d: all 39 displayed pair/middle factorizations checked; output explicitly records completeness_certificate=false.
• artifacts/baseline_powerful_1e6.json SHA-256 6e1b15cf69f5c9da430f80b2419eb1135b1ef4892b8d4f7582c2b27f425b17d6.
• python3 -m unittest -v tests/test_verify_powerful_triple.py: four adversarial tests passed.

• .proof-experiments/20260720-203815-fbb4dd: generated 2,027 powerful integers through 10^6; pair starts [25,70225], no triples.
• .proof-experiments/20260720-203822-2f8c58: independent factor-exponent classifier matched exactly.
• .proof-experiments/20260720-204059-94e77d: displayed OEIS factorizations verified, completeness not certified.

scripts/check_powerful_enumeration.py reconstructs the complete bounded set using prime exponents rather than a^2*b^3 generation. scripts/check_oeis_first13.py independently rechecks factor output using exact products and deterministic primality below 2^64. Any positive witness still requires an external Sage, PARI, or certificate-based reconstruction.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Pell classification of consecutive odd powerful pairs -> an exhaustive kernel/fundamental-unit cover should reproduce every distance-two pair in a toy interval -> source parametrization recovery remains the next test.
• Certificate-carrying counterexample search -> three complete factorizations can validate a finite witness independently of its search process -> fail-closed local checker completed.
• Formal premise retrieval -> the mod-36 restriction should be a compact Lean normalization lemma -> proposed but not executed during this baseline.

• Any hypothetical triple start n is congruent to 7, 27, or 35 modulo 36.
  Elementary mod-4/mod-9 proof; published by Beckon in 2019. · all positive integer starts · proved
• The two independent implementations find 2,027 powerful numbers, pair starts 25 and 70225, and no triple through 10^6.
  .proof-experiments/20260720-203815-fbb4dd and .proof-experiments/20260720-203822-2f8c58 · 1 <= n <= 1000000 inclusive · computed
• All 13 displayed A076445 values are valid distance-two powerful-pair starts and each displayed middle is non-powerful.
  .proof-experiments/20260720-204059-94e77d · the 13 displayed b-file values only · computed
• The abc conjecture implies only finitely many powerful triples.
  Nitaj 1996, Proposition 3.8.3, and the official source summary. · conditional on abc · conditional

• Infer the no-triple-below-7.38e28 claim solely from the audited 13 displayed terms.
  completeness of A076445 below its 13th displayed term · Membership and factorization checks do not exclude omitted distance-two pairs. · .proof-experiments/20260720-204059-94e77d records completeness_certificate=false; OEIS history supplies attribution but no exhaustive artifact. · Obtain a complete search program with a proven domain or an independently checkable exhaustive certificate.
• Naively enumerate a^2*b^3 values to 7.38e28.
  direct canonical generation · The b=1 branch alone exceeds 2.7e14 iterations and would merely replay an arbitrary cutoff. · scripts/enumerate_powerful.py loop bounds and the integer square root of the reported bound. · A proven sublinear pair enumerator or kernel bound making certified exhaustive coverage tractable.
• Transfer van Doorn's growing-difference progressions directly to consecutive integers.
  common difference 1 · The construction has common difference 2*sqrt(N)+1 and addresses a different adjacency question. · https://arxiv.org/abs/2605.06697 · A powerfulness-preserving transformation that provably reduces the difference to 1.

• Reconstruct the completeness evidence for the A076445 prefix.
  This is the cheapest discriminator for whether the official headline computational bound is reproducible. · Encode the Sentance/Mollin-Walsh Pell-kernel cover on [1,10^6] and compare exact pair starts with the baseline artifact. · high · open
• Formalize the mod-36 restriction and Nat/positive equivalence.
  A compact formal artifact would validate later symmetry restrictions and has a clear upstream path. · Compile a sorry-free Lean lemma against a pinned formal-conjectures checkout. · normal · open

Objective: Audit and reconstruct the completeness provenance of the A076445 13-term prefix without extending an arbitrary cutoff.

First action: Start from https://oeis.org/history?seq=A076445&start=20 and the historical thread linked at https://mathoverflow.net/questions/33037; recover the Noe/Reynolds algorithm and encode Sentance's Pell cover for comparison with artifacts/baseline_powerful_1e6.json.

Stop condition: Stop if the cover cannot be proved exhaustive, no source artifact exists, or the toy implementation misses 25/70225 or disagrees with the exact baseline. If a complete artifact is found, switch immediately to independent replay.

• Recover the T. D. Noe and Geoffrey Reynolds algorithm and exact domain behind the A076445 prefix.
• Implement a toy Sentance/Mollin-Walsh Pell-kernel cover and prove it enumerates every distance-two powerful pair through 10^6.
• Require exact agreement with artifacts/baseline_powerful_1e6.json before scaling.
• If a complete historical artifact is found, replay it independently and design a compact completeness certificate rather than extending the cutoff.

• https://www.erdosproblems.com/364 ↗
• https://www.renyi.hu/~p_erdos/1976-39.pdf ↗
• https://mathweb.ucsd.edu/~ronspubs/80_11_number_theory.pdf ↗
• https://doi.org/10.1155/S0161171286000984 ↗
• https://doi.org/10.1090/S0025-5718-1988-0929558-3 ↗
• https://scholar.rose-hulman.edu/rhumj/vol20/iss2/3/ ↗
• https://math.colgate.edu/~integers/z7/z7.pdf ↗
• https://math.colgate.edu/~integers/z103/z103.pdf ↗
• https://oeis.org/A076445 ↗
• https://oeis.org/history?seq=A076445&start=20 ↗
• https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/364.lean ↗

GPT-5.6 Sol principal performed synthesis, source audit, experiment design, coding, and interpretation. A GPT-5.6 Terra source-discriminator supplied an advisory memo and initial checker; Sol independently audited the claims and promoted a hardened checker with provenance. Web search/browser access, Python 3.12 exact integer code, GNU coreutils factor 9.4, and deterministic Miller-Rabin below 2^64 were used. No CAS, SAT/SMT solver, proof-assistant execution, cloud lab, or background process was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1149.9s

Review state

not a result claim

Attempt ID

erdos-364-20260720-204912-aa8f3d

No human review recorded.