Reviewed the completed hash-bound Lean target lab, then performed a reproducible matched prior-art audit against the official problem, Formal Conjectures issue 773, and open PR 4044.

Progress

The repaired scoped declaration is kernel-valid for its exact source hash. A fresh primary-source audit then found an older open reviewed PR for the same formalization, contradicting the supplied novelty baseline. No helper relocation or external submission was performed.

Research-policy redirect

Automated lab review may recommend validate/promote, but only an operator may apply it with an independent validation receipt.

Strategy and discriminator

isolated adversarial reconstruction

Use the pinned Lean kernel to validate exact source hashes, independently audit Sidon semantics, and fail closed when a live primary-source search reveals overlapping upstream work.

Hypothesis: The repaired source kernel-checks on current pinned main, but it cannot qualify as a novel independent formalization if live upstream records contain a same-target reviewed pull request.

Test: Validate the completed warning-fatal target receipt and query the official page plus GitHub issue, pull-request, comment, and review APIs for a same-target active contribution.

Rationale

Kernel acceptance satisfies the bounded technical discriminator, while the live PR is decisive against an independent novelty claim. Continuing source work without coordination would increase duplicate risk without improving the acceptance path.

Claims requiring scrutiny

Local source SHA-256 3ff7038c3c08f48408f48d53c4503182944cfd8c51b549cbab570a3b062e8466 builds warning-fatally under Lean 4.27.0 for FormalConjectures.ErdosProblems.«530».
The generated nonempty 530.olean has SHA-256 0ba42a02ee4fd1fed5b19d584dbae21cb4f8dde7cffc8b2c432f4cb0befdcb37.
As of 2026-07-22, official Problem 530 remains OPEN and marked not formalised.
As of 2026-07-22, Formal Conjectures PR 4044 is open, unmerged, labelled awaiting-author, and targets the same formalization.
The local candidate is a material cleanup of PR 4044 rather than a net-new scholarly target.

Evidence and scope

Lab record jq checks: returncode=0, correctness_checks_passed=true, and exact source hash matched.
Lab stdout: Built FormalConjectures.ErdosProblems.«530»; Build completed successfully (8038 jobs); OLean hash recorded.
Experiment 20260722-063653-310bb7 returned 0 in 2.231 seconds with empty stderr and preserved official/GitHub status data.
Experiment 20260721-223233-e53846 returned 0 in 10.082 seconds for the independent Lean semantic audit.
git diff --check and bash -n checks/audit_erdos530_live_status.sh both passed.

Computational experiments

lab-runs/lab-scout-bdf77f43574b-135f90912547/segment-000001/20260722-044206-6702a3: exact target returned 0 and emitted OLean hash 0ba42a02ee4fd1fed5b19d584dbae21cb4f8dde7cffc8b2c432f4cb0befdcb37.
.proof-experiments/20260722-063653-310bb7: live status audit returned 0 and found open same-target PR 4044.
.proof-experiments/20260721-223233-e53846: independent Lean semantic audit returned 0.

Independent checker

checks/Erdos530SemanticAudit.lean independently restates the discarded finite-set predicate, proves it equivalent for every finite set of reals to project IsSidon, and checks the repeated-summand collision; experiment 20260721-223233-e53846 returned 0.

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

None recorded.

Established facts

The repaired exact target is warning-clean for source hash 3ff7038c3c08f48408f48d53c4503182944cfd8c51b549cbab570a3b062e8466.
Validated lab 135f90912547, return code 0, empty stderr, and hashed OLean. · Pinned Formal Conjectures checkout 8f6e745798379104379da0b5c28c25315489890f with Lean 4.27.0. · computed
The discarded local Sidon predicate and project IsSidon agree on every Finset ℝ.
Kernel-checked theorem legacyFinsetIsSidon_iff_projectIsSidon in checks/Erdos530SemanticAudit.lean. · All finite sets of real numbers. · proved
PR 4044 is a same-target open upstream formalization.
Hash-recorded GitHub API output in experiment 20260722-063653-310bb7. · Repository status observed on 2026-07-22. · computed

Ruled out in this epoch

Treat the local candidate as the first or only existing formalization effort.
Novelty and upstream-submission claims as of 2026-07-22. · Open reviewed PR 4044 predates this run and formalizes the same extremal function and asymptotic. · .proof-experiments/20260722-063653-310bb7/stdout.txt · None; historical priority cannot be restored.
Open an independent competing PR immediately.
Current Formal Conjectures contribution route. · The same target has an active author and reviewed pull request, creating unacceptable duplicate/spam risk. · PR 4044 status, review, and awaiting-author label. · Explicit coordination with the existing author/maintainer, or closure/abandonment followed by maintainer approval for a replacement.

Open leads

Coordinate the verified IsSidon-reusing cleanup with PR 4044.
It directly addresses the maintainer's principal semantic/API comment and preserves the current-main kernel receipt. · After human authorization, apply the smallest approved delta to the designated branch and run the hash-bound exact target. · high · open
Monitor PR 4044 status.
Its author activity and maintainer disposition determine whether any further local implementation is legitimate. · Run checks/audit_erdos530_live_status.sh and compare state, head SHA, label, and review threads. · normal · open

Continuation checkpoint

Objective: Preserve the verified local cleanup while avoiding duplicate submission and detect whether a coordinated acceptance path opens.

First action: Run checks/audit_erdos530_live_status.sh and compare PR 4044 state, head SHA, awaiting-author label, and review threads.

Stop condition: Stop source work if PR 4044 remains active without coordination; redirect to a coordinated patch if authorization is documented.

Next moves

Recheck PR 4044 state, head SHA, label, and unresolved review threads without modifying source.
Ask the human owner to coordinate with PR 4044's author or maintainers before offering the local cleanup.
If coordinated work is authorized, port IsSidon reuse and narrowed scope into the approved branch, relocate/index helpers as required, then run a hash-bound target build followed by clean-checkout CI.

Citations

Tool disclosure

Sol principal role: Codex based on GPT-5. Terra delegate role: gpt-5.6-terra supplied an advisory source-discriminator memo; its no-PR premise was independently checked and rejected. Deterministic tools used: Lean 4.27.0, Lake 5.0.0, Bash, curl, jq, rg, sha256sum, Git, and the computational-researcher run_experiment.py harness. No CAS, SAT/SMT solver, proof assistant other than Lean, external publication, or repository submission was used.

Duration: 577.5s
Review state: not a result claim
Attempt ID: scout-bdf77f43574b-20260722-063944-5d5057

Human review ledger

No human review recorded.