2026-07-21 14:47 UTCgpt-5.6-sol · high

Baseline source and literature audit followed by validation of an exact Hall-certificate counterexample harness on a predeclared finite domain

Progress

The exact statement and current open status were audited. Historical methods, accepted and provisional computations, Lean semantics, software, verification contract, and external acceptance path were mapped. A mislabeled positive control inherited from the Terra delegate was corrected because its graph was actually deficient. The recorded experiment passed all seven controls, independently agreed through 1000, and found no failure among 779987 windows from 90407 composite starts with n+k<=100000. This is not a new bound or evidence for the universal conjecture.

Strategy and discriminator

counterexample and witness search

Factor each composite interval, construct its position-to-prime-divisor bipartite graph, test for a perfect matching, and emit a Hall-deficient subset on failure; compare against trial division plus exhaustive Hall-subset enumeration on a smaller domain.

Hypothesis: The SPF/matching discriminator agrees with an independent trial-division/exhaustive-Hall oracle through 1000 and finds no Hall-deficient all-composite window for n+k<=100000.

Test: Require seven positive and adversarial controls, exact count agreement between materially different encodings at limits 3, 4, 10, 30, 100, and 1000, then stop the production scan at endpoint 100000 or immediately on a Hall certificate.

Rationale

Hall's theorem gives an exact finite disproof contract, making matching the cheapest legitimate discriminator. The independent oracle exercises different factorization and decision mechanisms on a bounded shell. The successful scan establishes only its declared finite result; accepted literature already covers a vastly larger range.

Claims requiring scrutiny

A finite counterexample is certified by n,k>=1, complete factorizations of n+1 through n+k, and a subset S of positions whose union of prime divisors has cardinality less than |S|.
The SPF/matching and trial-division/exhaustive-Hall implementations agreed at every declared boundary through endpoint 1000.
No Hall-deficient all-composite window was found for n>=1, k>=1, and n+k<=100000.
The Formal Conjectures statement is semantically faithful up to a harmless vacuous k=0 extension, but the main theorem and several variants still contain sorry.

Evidence and scope

.proof-experiments/20260721-143839-1180de/experiment.json, SHA-256 d36c520951056e3497e6c99a1e1e0e6d17dbc5984eb58ed79cb4dc9f51dce7b4
artifacts/baseline-N100000.json, SHA-256 b7d09845daba92050b2b0a9ae4011926521b109f3ae345eb9d5eae196793f3ee
tools/run_baseline_experiment.py, SHA-256 4efb3de78351b64b9a6da89cb998b239618eeeef3a62a3a3b09ccaef9d23b6b1
tools/grimm_discriminator.py, SHA-256 fb8d3fb7ec1dbff5df806833666e8feb410db2e3d118477fb71fcedd8a6c061f
tools/verify_grimm_certificate.py, SHA-256 9403e91fffd59ca76b10525caf6f5521422df3263f5a176f263e343682d3fb97
notes/baseline-audit.md, SHA-256 c3b4256ac15e8443b0a4d4183f07cd719669bb170d79ab517a02c8693c3ddaa9

Computational experiments

.proof-experiments/20260721-143839-1180de: return code 0 in 17.344 seconds, peak child memory 21120 KB, seven controls passed, oracle agreement through 1000, and OK_FINITE_ONLY for 779987 windows with n+k<=100000.

Independent checker

tools/run_baseline_experiment.py uses trial division and exhaustive Hall-subset enumeration rather than the production SPF sieve and matcher through endpoint 1000. tools/verify_grimm_certificate.py separately refactors a claimed counterexample and verifies its Hall inequality. The full endpoint-100000 scan was not independently reimplemented at that entire range.

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

Hall-certificate methods from bipartite matching -> any failed prime assignment must expose a deficient proper subset, not merely too few primes globally -> the deceptive graph [[2],[2],[3,5]] passed the intended adversarial control by rejecting the whole-product proxy.

Established facts

The maintained database labels Erdős #375 open/falsifiable and warns that this is not a complete literature guarantee.
https://www.erdosproblems.com/375, audited 2026-07-21 · Maintained source status · proved
Laishram and Shorey's archival abstract states verification for all k when n<=1.9e10.
https://repository.ias.ac.in/67716/ · Reported 2006 numerical result · proved
No failure occurred in the local production scan of 779987 windows with n+k<=100000.
artifacts/baseline-N100000.json and recorded experiment 20260721-143839-1180de · n>=1, k>=1, n+k<=100000 only · computed
The independent oracle agreed with production counts and decisions at limits through 1000.
artifacts/baseline-N100000.json · Declared boundary limits 3,4,10,30,100,1000 · computed

Ruled out in this epoch

Treat a larger arbitrary local cutoff as a contribution.
Any extension that neither exceeds a validated frontier nor yields a structural result. · The accepted 2006 range and later provisional claims are vastly larger. · notes/baseline-audit.md literature map · A counterexample, expert-requested range, validated best-bound improvement, or new structural theorem.
Use only the number of distinct prime factors in the whole interval product.
All finite intervals. · This checks Hall's inequality only for the full left set; a proper subset can still be deficient. · The controlled graph [[2],[2],[3,5]] has three global primes for three vertices but fails Hall on its first two vertices. · A proof that the special consecutive-integer divisor graphs make the whole-set condition sufficient for every subset.
Compile or extend the Lean formalization in the current host state.
Formal Conjectures bootstrap attempted 2026-07-21. · Cache unpacking failed with only 64 KB free disk; cleanup restored only 369 MB. · notes/baseline-audit.md system audit · Verify several GB of free disk, rerun the prescribed bootstrap, and compile without sorry.

Open leads

Recover and audit the Brox-Paseman provisional computation artifacts.
This resolves the closest-prior-work ambiguity and may expose reusable exceptional-interval data or code before new compute is spent. · Follow the EACA slides and MathOverflow links; inventory code, logs, exact failures, cover semantics, and replay the smallest failure if runnable artifacts exist. · high · open
Formalize the Hall-certificate contract or a finite interval checker in Lean.
A small kernel-checked certificate layer would be reusable even without solving the conjecture. · After disk repair, bootstrap Formal Conjectures and compile a minimal Hall-equivalence lemma with no sorry. · normal · open

Continuation checkpoint

Objective: Resolve the closest-prior computational artifact trail before allocating further computation.

First action: Inspect https://mathoverflow.net/questions/248146/on-comparing-two-almost-injective-divisor-maps and its EACA-slide link, including archived targets, and record every source-code, data, range, and exception artifact.

Stop condition: Stop when a runnable artifact permits independent replay of the smallest claimed failure and repair, or when the public trail ends without code or certificates and park the bound-extension lane.

Next moves

Audit the Brox-Paseman EACA slides, linked sources, and archives for public code, exact S-algorithm exceptions, range semantics, and validation artifacts.
If code is located, replay the smallest reported S failure and verify its proposed repair using the independent Hall checker.
Do not enlarge the local 100000 cutoff unless a counterexample, expert-requested range, validated frontier improvement, or structural theorem creates a legitimate contribution path.
Retry the Formal Conjectures bootstrap only after verifying several gigabytes of free disk space.

Citations

Tool disclosure

GPT-5.6 Sol principal performed synthesis, source audit, artifact review, control repair, and checkpointing. A GPT-5.6 Terra delegate supplied the inherited reconnaissance memo and initial Python artifacts; the Sol principal independently audited them and corrected one mislabeled control. Python 3.12.3 ran the deterministic SPF/matching search, trial-division/exhaustive-Hall oracle, certificate rejection controls, and prescribed experiment recorder. Internet search and primary-source retrieval were used. The Formal Conjectures Lean bootstrap was attempted but failed for disk capacity before target compilation; no Lean kernel result, CAS, SAT solver, or external expert validation was obtained.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1032.6s
Review state: not a result claim
Attempt ID: erdos-375-20260721-144714-02603d

Human review ledger

No human review recorded.