2026-07-21 12:52 UTCgpt-5.6-sol · high

Mandatory source/status baseline audit followed by exact validation of the finite-counterexample certificate contract

Progress

The maintained positive-denominator statement remains open/falsifiable. The historical signed identity is outside its scope. The linked Lean file contains sorry in the main, gap-2, prime, and bridge theorems. The certificate-contract experiment checked 5,798 sequences with zero mismatches and passed seven controls in 0.288 seconds with 18,164 KB peak child memory. A pinned good-prime repository's arithmetic also reran successfully, but its lower bound remains conditional because the mathematical bridge was not independently proved. No frontier search was launched.

Strategy and discriminator

counterexample-certificate search

Recognize finite disproof witnesses with exact Fraction arithmetic and audit that recognizer against a separate integer LCM-clearing implementation

Hypothesis: The Fraction-based witness checker agrees with an independent LCM-clearing oracle on every subsequence of 2 through 14 having 2 through 7 terms and rejects controls for the corrected scope.

Test: Compare both exact encodings on all 5,798 bounded sequences and stop at the first mismatch or failed gap, positivity, sum, or ordering control.

Rationale

This completes the required baseline and supplies a reproducible verifier for the source's falsifiable status. The bounded audit validates the verifier over its stated domain but does not imply a new no-counterexample bound. Source and code inspection show that neither the Lean statement nor the good-prime arithmetic alone proves the target.

Claims requiring scrutiny

As audited on 2026-07-21, the official problem explicitly requires 1 < n_1 and remains labelled FALSIFIABLE with no incorporated solution or partial solution.
The Formal Conjectures research theorem and its prime-distribution bridge remain unproved by sorry.
The two exact witness encodings agreed on all 5,798 enumerated audit cases and every listed adversarial control passed.
The external good-prime verifier reproduces its own arithmetic, but its printed k-bound is not established in this workspace without the bridge lemma.

Evidence and scope

notes/baseline-review-2026-07-21.md, SHA-256 da898d404b9d828e87ed07561f8e6830eafe5592ce707f7a23cc9dce79e39125
tools/verify_counterexample.py, SHA-256 e7ca2b6a376b630222798efc6e75de75f133cadd5e052784c2497968eff6f383
tools/audit_counterexample_checker.py, SHA-256 10218d38e8718735d4bdfed471cdb47e33044ebb11bc6f874da3d9df7193d79c
.proof-experiments/20260721-124411-47ef7b: return code 0, 5,798 sequences, zero mismatches, seven passed controls
Formal Conjectures commit d3f74a9a760516fac291859dc741a148ca454e8e; 287.lean SHA-256 9e90445fcbb14f334a23d1afbd7e46a69fdfd55794ecfa134e23754a21d8c402
Good-prime repository commit 7c36f1ed0fb0c5b8da4ecfcfb0cad222dee4c34b; verifier stdout SHA-256 36a08da0b956f588cd5df1caebb36aba99234c4f24b6fd4ecde33c85429a8385

Computational experiments

.proof-experiments/20260721-124411-47ef7b: both exact encodings agreed on 5,798 sequences; zero accepted witnesses; all seven controls passed

Independent checker

tools/audit_counterexample_checker.py materially differs from the production checker: it clears denominators with math.lcm and compares integer numerators rather than using fractions.Fraction.

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

Kürschák/Erdős LCM divisibility arguments -> a uniquely maximal p-adic denominator valuation should obstruct an integer reciprocal sum -> the general LCM lemma was recorded as a proved reusable fact.
Restricted-denominator Egyptian-fraction enumeration -> a finite witness recognizer should admit a materially different bounded oracle -> the LCM oracle agreed with the Fraction checker throughout the audit domain.
Formal premise retrieval -> a statement repository can clarify semantics without proving the theorem -> the exact positive-natural formulation was confirmed, while four relevant declarations still contain sorry.

Established facts

The current official target requires positive denominators beginning with 1 < n_1 and is labelled FALSIFIABLE.
Official page, revision history, and teorth database commit a7b9502af8962b83161f403d55dddb1226e538d0 · Maintained status as accessed 2026-07-21 · proved
The historical signed 20-term vector sums to 1 and has gaps at most 2, but fails the present positivity hypothesis.
Independent integer-LCM control in experiment 20260721-124411-47ef7b · That displayed vector under the current statement · computed
If exactly one denominator has strictly maximal p-adic valuation, the reciprocal sum cannot be an integer.
After multiplication by the LCM, exactly one numerator summand is nonzero modulo p. · Any finite collection of positive integer denominators · proved
The Fraction checker and LCM oracle agree on all subsequences of 2 through 14 with 2 through 7 terms.
Experiment 20260721-124411-47ef7b, 5,798 comparisons and zero mismatches · Exactly that finite audit domain · computed
The pinned good-prime code verifies its chain, Pocklington steps, and numerical floors.
Commit 7c36f1ed0fb0c5b8da4ecfcfb0cad222dee4c34b, verifier exit 0 · Repository arithmetic only; assumes the mathematical bridge · conditional

Ruled out in this epoch

Use the signed-denominator identity to disprove the current problem.
Current official statement · It violates 1 < n_1. · Official history and exact scope control · The official statement would have to revert to signed denominators.
Interpret formalized: yes as a proof.
Formal Conjectures revision d3f74a9a760516fac291859dc741a148ca454e8e · The main and bridge declarations contain sorry. · Pinned source inspection · A compiling, sorry-free theorem with an acceptable axiom report.
Extend the good-prime chain during the next epoch.
Beyond endpoint 147573952589666836319 · A longer chain only enlarges a conditional cutoff while the decisive bridge remains unverified. · Pinned arithmetic replay and source audit · Independent written or formal proof of the bridge.
Repeat the forum's n_1 <= 12 or k <= 18 computations as a standalone contribution.
Those reported finite ranges · Their artifacts are unavailable and repeating arbitrary cutoffs has no credible standalone acceptance path. · Forum and artifact audit · A supplied archive requiring independent review, or use as a regression control for a stronger structural result.

Open leads

Formalize the finite good-prime bridge.
It is the missing theorem behind the strongest existing finite certificate. · Prove the unique-maximal-valuation lemma and p/q bridge in a standalone Lean module, requiring no sorry and an inspected axiom report. · high · open
Attack all bridge boundary cases with an independent LCM proof and PARI/GP.
This can cheaply expose a small-q or endpoint omission before formalization. · Enumerate admissible small p, q, and M configurations and all subsets of q, 2q, and 3q; stop at the first failure of the predicted valuation obstruction. · normal · open
Audit the reported k <= 18 Lean development if it becomes available.
Its fixed-k decision theorem and gap-word bridge may be reusable, but the forum description is not evidence. · Build the exact archive, search for sorry/admit and unexpected axioms, and compare its theorem statement with the official source. · low · open

Continuation checkpoint

Objective: Independently verify the arbitrary-parameter good-prime bridge before any chain extension.

First action: Run `df -BG /`; if at least 7G is free, run `/root/proof-factory/scripts/bootstrap-formal-conjectures.sh`; otherwise begin the standalone LCM proof and PARI/GP boundary-control script without another bootstrap attempt.

Stop condition: Stop on any admissible p,q,M counterexample or missing hypothesis; otherwise stop when a sorry-free bridge compiles with an inspected axiom report, or when a complete paper proof and boundary controls isolate the exact remaining formal lemma.

Next moves

Independently prove the arbitrary-parameter good-prime bridge, explicitly checking q=7, q=11, interval endpoints, and possible q-divisible denominators q, 2q, and 3q.
Use PARI/GP exact boundary enumeration as an adversarial control for the written bridge proof.
When at least 7 GB is free or a larger cache volume exists, rerun the prescribed Formal Conjectures bootstrap and formalize the bridge without sorry.
Do not extend the good-prime chain or repeat the reported n_1 <= 12 and k <= 18 cutoffs until their structural blocker or missing artifacts are resolved.

Citations

Tool disclosure

GPT-5.6 Sol was principal investigator. The prior GPT-5.6 Terra source-discriminator memo was advisory and independently audited. Tools used: web/source retrieval, Git, curl, PDF text extraction, Python 3.12 exact Fraction and integer-LCM arithmetic, the computational-research experiment harness, and the pinned external Pocklington verifier. Lean 4.27 bootstrap was attempted twice but failed for disk space; no Lean theorem was built. PARI/GP, Z3, and SAT tools were inventoried but not used to support a mathematical claim.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1350.1s
Review state: not a result claim
Attempt ID: erdos-287-20260721-125231-22a5f5

Human review ledger

No human review recorded.