2026-07-21 01:01 UTCgpt-5.6-sol · high

Mandatory source-and-method baseline, exact structural reduction, bounded formulation calibration, fail-closed certificate verification, and attempted reproduction of the strongest reported Lean barrier

Progress

The source audit confirms that Erdős Problem 307 remains open. Exact arithmetic independently reproduced the known 59-prime threshold and both encodings agreed on all 57002 assignments in the bounded control shell, with no solution there. A dependency-free exact certificate verifier rejected four adversarial controls. The finite numerical input behind the reported side-product barrier was checked exactly. The universal Lean barrier was not locally reproduced: the first build stopped at ENOSPC and the single post-repair retry stopped during mathlib cache retrieval with failed to create thread under a 4096 MB limit, before theorem compilation.

Strategy and discriminator

counterexample and witness search with formal barrier audit

Reduce every candidate to exact integer forcing equations, validate a fixed finite shell under independent encodings, provide a fail-closed verifier, and audit the pinned formal lower-bound source before permitting search

Hypothesis: The exact smallest-prime reciprocal threshold is 59, the rational identity agrees with the forced integer equations throughout the first-ten-prime shell, and the tagged Bonfioli barrier can be independently rebuilt with its claimed axiom footprint.

Test: Compute the 58/59 threshold with exact fractions, exhaust all 57002 nonempty disjoint assignments of the first ten primes under two encodings, and run the clean tagged Lean source through lake build and Check.lean.

Rationale

The completed baseline supplies independently reproducible exact controls, corrects the working search specification to the already-known 59-prime bound, identifies the forced-partner interface, distinguishes reported formal evidence from locally checked evidence, and leaves an executable continuation without asserting a new solution or bound.

Claims requiring scrutiny

For M(S)=product(S) and A(S)=sum over s in S of M(S)/s, gcd(A(S),M(S))=1 for every finite set of primes S.
A pair P,Q solves the target exactly if and only if A(P)=M(Q) and A(Q)=M(P); consequently P and Q are disjoint and either side forces the other.
The reciprocal sum of the first 58 primes is less than 2 and that of the first 59 primes is greater than 2, so every solution has at least 59 union primes.
No solution occurs among disjoint nonempty subsets of the first ten primes; this statement is limited to exactly 57002 checked assignments.
Bonfioli v1.0.0 reports a stronger universal side-product barrier, but it was not locally kernel-reproduced in this epoch.

Evidence and scope

notes/baseline-audit-2026-07-21.md, SHA-256 c1d5c098767e83a82c1a70141494437ca10a7001ac2e7ee74ca6ee628680f07e
.proof-experiments/20260721-004424-f76e4e: exact threshold and 57002-assignment enumeration; canonical payload SHA-256 3bc0172e352980bdb563aba82b859122a55047cee3f654fa75ddbcad77152de4
.proof-experiments/20260721-004437-ff8f64: independent sieve-based regeneration accepted the same payload
.proof-experiments/20260721-004455-4c7701: duplicate, nonprime, overlap, and exact nonsolution controls were all rejected for the intended reasons
.proof-experiments/20260721-005307-efbf19: exact finite first-59-prime barrier ratio and integer square-root boundary
.proof-experiments/20260721-004711-d73ced: first Lean attempt failed before compilation with ENOSPC
.proof-experiments/20260721-005600-413631: clean tag and source hashes passed, but cache retrieval aborted before compilation with failed to create thread under the enforced 4096 MB limit

Computational experiments

.proof-experiments/20260721-004424-f76e4e — exact 58/59 threshold, 57002 assignments, zero encoding mismatches and zero solutions
.proof-experiments/20260721-004437-ff8f64 — independent checker reproduced payload SHA-256 3bc0172e352980bdb563aba82b859122a55047cee3f654fa75ddbcad77152de4
.proof-experiments/20260721-004455-4c7701 — all four certificate-verifier negative controls rejected
.proof-experiments/20260721-005307-efbf19 — exact finite numerical barrier input checked
.proof-experiments/20260721-004711-d73ced — Lean build stopped at ENOSPC before compilation
.proof-experiments/20260721-005600-413631 — retry stopped at thread creation during cache retrieval before compilation

Independent checker

scripts/check_baseline_output.py independently regenerates primes with a sieve and checks the canonical audit payload. scripts/verify_certificate.py independently checks exact integer forcing and Fraction identities for explicit P,Q certificates. Large-prime scalability still requires proof-carrying primality.

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

Arithmetic-derivative two-cycles -> predict that searching P and Q independently wastes the exact forcing structure -> direct rational and derivative/forcing encodings agreed on all 57002 bounded controls.
Proof-carrying witness search -> predict that decimal near-equality is an unreliable objective -> published genetic search reports only near misses, while the exact verifier rejects ordinary prime-set near candidates unless both integer equalities close.

Established facts

Every solution satisfies A(P)=M(Q), A(Q)=M(P), and P intersect Q is empty.
Elementary reduced-fraction proof in notes/baseline-audit-2026-07-21.md, consistent with Bado 2026 and Bonfioli v1.0.0. · All finite sets of primes P,Q. · proved
Every solution has at least 59 primes in P union Q.
AM-GM, distinct-prime reciprocal extremality, and two independent exact computations of the 58/59 boundary. · All finite prime-set solutions; this is an established correction already public in 2019, not a new result. · proved
No solution exists in the first-ten-prime assignment shell.
Exhaustive enumeration and independent payload checker in experiments 20260721-004424-f76e4e and 20260721-004437-ff8f64. · Exactly all 57002 assignments of the first ten primes to neither/P/Q with P,Q nonempty. · computed
The ceiling of the exact finite barrier ratio's square root is 209298852061282362260655116218815858656815144494074532631.
.proof-experiments/20260721-005307-efbf19 checks this integer and its predecessor by exact arithmetic. · Finite numerical input only; it does not independently establish the universal barrier. · computed

Ruled out in this epoch

Independent two-sided subset search or floating-point genetic optimization as a proof-bearing route.
The exact prime-set existence problem. · Q is forced by A(P), while decimal proximity does not certify either integer forcing equality. · Reduced-fraction forcing theorem, exact verifier, and comparison with the reported Rubbens search. · An exact theorem or construction showing that the proxy preserves or efficiently predicts forced-partner closure.
Reporting 60 as the sharp consequence of the elementary reciprocal-sum argument.
All future statements of that argument. · The exact crossing occurs at the 59th prime. · Independent exact computations and the 2019 MathOverflow correction. · None; the argument yields 59.
Another arbitrary bounded search beneath the reported 2e56 side-product scale.
A claimed contribution or solution search relying on Bonfioli's reported theorem. · It would repeat a range already excluded by the closest source and would not improve its result. · Bonfioli v1.0.0 source and Formal Conjectures annotation; local kernel reproduction remains pending. · The formal barrier fails an independent kernel audit, or the computation targets a separately motivated structural statistic with an explicit acceptance path.

Open leads

Complete the pinned Lean barrier and axiom audit under adequate or serialized memory.
This determines whether the strongest current exclusion can be promoted from externally reported to locally kernel-reproduced. · Run scripts/check_bonfioli_barrier.sh once through the experiment recorder with memory above 4096 MB or a documented supported single-thread cache configuration. · high · open
Add proof-carrying primality to the exact certificate format.
Trial division is exact but infeasible for the enormous primes expected in any witness. · Define a Pratt or Pocklington JSON schema, accept one known certified prime under two implementations, and reject every one-field mutation. · high · open
Test construction families solely through squarefree arithmetic-derivative closure.
A candidate is determined by one squarefree a with squarefree a' and a''=a; independent P,Q generation is unnecessary. · Specify a family reaching a greater than 2e56, evaluate exact squarefreeness and closure on a fixed small parameter sample, and stop if it cannot reach the scale or only optimizes decimal proximity. · normal · open

Continuation checkpoint

Objective: Independently reproduce or precisely reject the Bonfioli v1.0.0 universal barrier, then harden certificate verification.

First action: Reuse /root/.cache/proof-factory/erdos307-v1.0.0 and invoke scripts/check_bonfioli_barrier.sh once through run_experiment.py with memory above 4096 MB, or first document a supported single-thread setting; do not reclone.

Stop condition: Stop after one successful lake build plus Check.lean axiom audit, or the first new precisely diagnosed failure. If successful, proceed only to one proof-carrying primality control.

Next moves

Reuse the pinned Bonfioli v1.0.0 checkout and run one recorded build with memory above 4096 MB or a documented supported single-thread cache configuration; capture Check.lean axiom output.
After a successful formal audit, extend the certificate verifier with a minimal Pratt or Pocklington primality-certificate schema and test one positive control plus mutated negative controls.
Do not begin a frontier search until a construction family reaches the reported barrier scale and uses the one-sided forced-partner closure predicate.

Citations

Tool disclosure

GPT-5.6-class Codex acted as Sol principal for synthesis, derivations, code, execution, and audit. A prior GPT-5.6 Terra source-discriminator memo was advisory only and was checked against sources and deterministic artifacts. Tools used were web search/browser, Git, curl, Poppler, Bash, Python 3.12 exact integers and Fraction, the computational-researcher experiment recorder, and Lean/elan/lake bootstrap tooling. No model agreement was treated as validation; no external publication or message was sent.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1892.1s
Review state: not a result claim
Attempt ID: erdos-307-20260721-010133-c85502

Human review ledger

No human review recorded.