2026-07-21 04:53 UTCgpt-5.6-sol · high

Mandatory source/status baseline, adversarial reconstruction of postdated claims, and differential validation of finite-witness checkers.

Progress

The problem remains open. Dense marking and direct streaming congruence evaluation agreed on all 1919 controls and failed closed at the period cap. The May 2026 Lean claim depends on custom axioms extending beyond BBMST's hypotheses. The April 2026 few-prime manuscript asserts a false Step 2 equality: tower classes 0 mod 3 and 0 mod 9 leave 6 residues, not 9/2. A normalized-ratio repair remains open.

Strategy and discriminator

isolated adversarial reconstruction

Compare exact source hypotheses with claimed encodings, isolate the smallest exact discrepancy, and validate witness tooling using independent algorithms.

Hypothesis: The maintained problem remains open, the two postdated self-published claims do not establish an unconditional resolution, and independent finite-period checkers agree on a complete bounded control corpus.

Test: Audit original and current sources, compare cited theorem hypotheses with claimed formal axioms, enumerate the smallest disputed weight-region example, and compare dense versus streaming coverage on 1919 prescribed candidates.

Rationale

The status audit used original, maintained, and current primary literature. The verifier result is exhaustive only for its declared corpus. The manuscript discrepancy is an exact human-checkable counterexample to a displayed equality, without claiming that the headline theorem is false.

Claims requiring scrutiny

As of 2026-07-21, no audited accepted source settles Erdős Problem 7.
The dense and streaming algorithms return identical first uncovered residues on all 1919 residue assignments over every nonempty subset of moduli {3,5,7,9}.
The April 2026 manuscript's Step 2 cardinality equality fails for the allowed tower {0 mod 3, 0 mod 9}.
The audited May 2026 Lean theorem is conditional on two custom axioms.

Evidence and scope

notes/baseline-audit-2026-07-21.md
.proof-experiments/20260721-044214-bde719: return code 0 and transcript SHA-256 d8223537fba684e951936ea8a893c1b7be98f4268a9c7a5bd632515b9db41dca
.proof-experiments/20260721-044556-444ba6: actual cardinality 6 versus asserted 9/2
tools/check_odd_cover.py SHA-256 b40f9c2ba8c74b3a349131c53758eb4ea75b6cc8e9ee78eb81644f370a0c6e7c
tools/check_odd_cover_stream.py SHA-256 43bed3af388dc696fa8a993ffaaa3071e4cf438d0ebb3ab351b186fd80235b6c
Audited Lean claim commit fe530b2cedd3a71c2cdb47cc36ed0c3cb047b086

Computational experiments

.proof-experiments/20260721-044214-bde719: 1919 differential controls and boundary tests passed
.proof-experiments/20260721-044556-444ba6: exact counterexample to the manuscript equality

Independent checker

tools/check_odd_cover_stream.py evaluates the original congruence predicates residue by residue, materially differing from tools/check_odd_cover.py's bytearray marking algorithm.

Contribution gate

not_requested

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

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

Counterexample-certificate search -> independent encodings should agree before generation -> both algorithms agreed on all 1919 controls.
Formal premise retrieval -> a claimed kernel proof may expose its missing step as an axiom -> the Lean claim's sieve_criterion exceeds BBMST's no-parallel-hyperplane scope.
Weight-function audit -> overlapping prime-power towers should test the asserted exact cardinality -> the smallest example falsified it.

Established facts

Every distinct covering has a modulus divisible by 2 or 3.
Hough–Nielsen Theorem 1, DOI 10.1215/00127094-2019-0058 · All finite distinct covering systems. · proved
No distinct odd covering exists if every prime p <= 73 occurs only to exponent at most one in all moduli.
BBMST Theorem 1.1 and final Section 5 remark, DOI 10.2140/ant.2021.15.609 · All finite systems satisfying that exponent restriction. · proved
A hypothetical distinct odd cover has LCM divisible by 9 or 15.
BBMST Theorem 1.4, DOI 10.1007/s00222-021-01087-5 · All finite distinct odd covering systems. · proved
Dense and streaming verification agree throughout the 1919-case control corpus.
.proof-experiments/20260721-044214-bde719 · Every residue assignment over every nonempty subset of {3,5,7,9}. · computed
The few-prime manuscript's displayed Step 2 equality fails on an allowed tower.
.proof-experiments/20260721-044556-444ba6 and direct counting modulo 9 · The equality as written, not the headline four-prime theorem. · proved

Ruled out in this epoch

Square-free or p<=73-square-free candidate search.
Systems with no p^2 dividing a modulus for p<=73. · Published BBMST work excludes the entire scope. · https://doi.org/10.2140/ant.2021.15.609 · A demonstrated error in the published theorem.
Odd LCM search avoiding both 9 and 15.
All finite distinct odd systems in that LCM class. · Published BBMST work excludes the entire scope. · https://doi.org/10.1007/s00222-021-01087-5 · A demonstrated error in the published theorem.
Treat the May 2026 Lean repository as an unconditional resolution.
Commit fe530b2cedd3a71c2cdb47cc36ed0c3cb047b086. · Its main theorem depends on two custom axioms not supplied by the cited BBMST results. · Source audit recorded in notes/baseline-audit-2026-07-21.md. · Replace both custom axioms with faithful proofs.
Use the April 2026 four-prime proof as written to prune search.
Its Step 2 and Step 3 weight-region derivation. · The asserted exact cardinality is false for overlapping tower congruences. · .proof-experiments/20260721-044556-444ba6 · Supply and independently audit a corrected actual-region or weighted-region proof.

Open leads

Repair or refute the four-prime weight-region argument using normalized intersection ratios.
It is a short structural lemma that can be killed by a small finite counterexample before significant work. · Exhaust tower assignments at primes 3,5,7 and exponents at most 3 using exact Fractions. · high · open
Machine-check published condensed covering trees.
This would create the missing reusable dataset and support disciplined repeated-modulus replacement. · Define a JSON split-tree schema and encode the published t_15 <= 4 construction. · normal · open
Seek a square-free near-cover with one prime repeated exactly twice.
Harrington–Sun–Wong prove that such an object transforms into a genuine distinct odd covering. · After tree tooling exists, encode the published tau_7 <= 6 tree and test a bounded replacement grammar. · normal · open

Continuation checkpoint

Objective: Decide whether the four-prime weight-function theorem can be rigorously repaired.

First action: Test and then prove or falsify |C_d intersection W|/|W| <= product over support of p^(-b)(p-1)/(p-2), beginning with exact exhaustive controls for primes {3,5,7} and exponents <=3.

Stop condition: Stop at the first exact counterexample; otherwise stop after a complete proof and novelty audit determine whether the resulting theorem is valid and new.

Next moves

Prove or falsify the normalized actual-weight-region cylinder inequality using exact small controls.
If it survives, write a complete repaired four-prime proof and compare it with accepted older necessary-condition results.
Create a machine-readable condensed-tree certificate format before attempting repeated-modulus replacement.
Retain square-free near-covers with one prime repeated twice, tau_p <= 2, as a recognized sufficient constructive subproblem.

Citations

Tool disclosure

GPT-5.6 Sol principal; GPT-5.6 Terra source-discriminator supplied the initial memo and dense checker, independently audited by Sol. Python 3.12.3, Bash 5.2, curl, pdftotext, Crossref, OpenAlex, Git, and exact integer/Fraction scripts were used. Third-party Lean source was inspected, but no proof assistant, SAT/SMT solver, or CAS was run.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1387.9s
Review state: not a result claim
Attempt ID: erdos-7-20260721-045309-4d8aa9

Human review ledger

No human review recorded.