Mandatory source/literature baseline followed by a scoped Lean interface draft and bounded independent semantic controls

Progress

The mandatory baseline was completed. A May 2026 preprint postdating the official page's last edit was identified and incorporated. A Lean candidate defines IsSidon, GuaranteedSidonSize, ell via Nat.findGreatest, maximality API lemmas, three controls, and the answer(sorry)-scoped asymptotic declaration. Two independent semantic encodings agreed on all 512 subsets of {-4,...,4}; all seven adversarial controls passed. The Lean candidate was not elaborated because this environment lacks FormalConjectures and Mathlib. Two low-memory diagnostics also failed while creating a Lean thread; a controlled 4096 MB single-thread run reached the actual unknown-module error.

Strategy and discriminator

formal proof with premise retrieval

Translate the maintained min-max statement using Finset, Nat.findGreatest, and Mathlib asymptotic equivalence; test the Sidon semantics independently before repository-pinned elaboration.

Hypothesis: The proposed four-variable Sidon predicate represents uniqueness of unordered pair sums with repetition, and the resulting bounded extremal interface can express the explicit conjecture ell(N) ~ sqrt(N).

Test: Compare the four-variable predicate with an independently implemented unordered-pair-sum encoding on every subset of {-4,...,4}, then attempt Lean elaboration far enough to identify whether the local environment contains the required repository dependencies.

Rationale

The source and current literature audit identifies a legitimate unfilled formalization target, and the bounded checker rejects the two most likely semantic mistranslations. However, finite semantic agreement is not kernel validation, and no repository build, CI, or human statement review has occurred. Progress rather than candidate status is therefore warranted.

Claims requiring scrutiny

As accessed on 2026-07-20, Erdős Problem #530 is marked open, asks whether ell(N) ~ sqrt(N), and reports no formalised statement.
Bailleul and Riblet's arXiv:2605.03181v1 reports the lower bound (1/(3 sqrt 3)+o(1)) sqrt(n) for arbitrary finite subsets of the integers and reals, without reaching the conjectured leading constant 1.
The literal four-variable Sidon predicate and unordered-pair uniqueness agree on every subset of {-4,...,4}; this is a finite computed fact only.
FormalConjectures/ErdosProblems/530.lean is a drafted, unelaborated candidate and is not yet a completed formalization.

Evidence and scope

FormalConjectures/ErdosProblems/530.lean; SHA-256 c9da31e92b035492d163a85fd74d6e26bf8b9b2fd22d9e7b90a9eb4dba2f8b2d
checks/check_sidon_semantics.py; SHA-256 61e1779dcad8af8eca614d1f3c87755ea55605ea6e69a748a6803db6d0d82304
.proof-experiments/20260720-194758-ee6344/stdout.txt: 512 subsets, 140 Sidon subsets, zero mismatches, seven controls true
.proof-experiments/20260720-194925-0f2242/stdout.txt: unknown module prefix FormalConjectures
research/baseline_audit.md and research/state.json
Terra memo SHA-256 verified as a84aafb6c27cf9ae1dc1e0820d1ddf60ea350d8dff9dd334f9e6c52fcbdcb3af

Computational experiments

.proof-experiments/20260720-194758-ee6344: successful semantic comparison on all 512 subsets of {-4,...,4}
.proof-experiments/20260720-194849-f1733c: failed resource control at 256 MB; Lean could not create a thread
.proof-experiments/20260720-194914-3f029d: failed resource control at 2048 MB; Lean could not create a thread
.proof-experiments/20260720-194925-0f2242: with LEAN_NUM_THREADS=1 and 4096 MB, reached the decisive missing FormalConjectures module error

Independent checker

checks/check_sidon_semantics.py uses unordered pairs with repetition, materially different from the candidate's four-variable implication. It exhaustively compared both encodings on all subsets of {-4,...,4}. It does not elaborate Lean or validate the asymptotic statement.

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

Mathlib's Ruzsa-Szemeredi extremal-number definition uses Nat.findGreatest -> prediction: the same bounded idiom gives a short maximality API for ell -> drafted successfully but repository elaboration remains pending.
Weak-Sidon literature excludes repeated summands -> prediction: that encoding will miss 0+2=1+1 in {0,1,2} -> observed, so the transfer was rejected for Problem #530.

Established facts

The two exact finite Sidon encodings agree on every subset of {-4,...,4}.
.proof-experiments/20260720-194758-ee6344/stdout.txt · Exactly 512 subsets of the nine-element integer domain · computed
The maintained source marks Problem #530 open and not formalised.
https://www.erdosproblems.com/530 accessed 2026-07-20 · Maintained-site status, which explicitly disclaims literature completeness · conditional
The May 2026 preprint reports a 1/(3 sqrt 3) asymptotic lower-bound constant over arbitrary finite subsets of R^d.
https://arxiv.org/abs/2605.03181 · Claim of arXiv v1; proof not independently reconstructed this epoch · conditional

Ruled out in this epoch

Formalize weak Sidon uniqueness while ignoring repeated summands.
Statement design for Problem #530 · It wrongly accepts {0,1,2}, despite 0+2=1+1. · .proof-experiments/20260720-194758-ee6344/stdout.txt · An authoritative source explicitly changes the target to weak Sidon sets.
Demand uniqueness of ordered pair representations.
Statement design for Problem #530 · It wrongly rejects swapped representations (a,b) and (b,a). · .proof-experiments/20260720-194758-ee6344/stdout.txt · None for the present source statement.
Treat the official page's April 2026 literature summary as current-complete.
Baseline literature audit · arXiv:2605.03181 was submitted after the page edit and improves the lower-bound constant. · https://arxiv.org/abs/2605.03181 · Not applicable; future audits must search beyond the page edit date.
Increase the finite checker cutoff as a contribution.
Bounded semantic testing · A larger arbitrary cutoff would neither validate Lean nor advance the mathematical bound. · The successful 512-case test already meets its control purpose. · Only a newly identified semantic ambiguity requiring a specifically targeted finite control.

Open leads

Pinned Lean elaboration and full repository build
This is the cheapest decisive verification of the drafted artifact. · Run the exact build command recorded in CHECKPOINT.md inside a current Formal Conjectures checkout. · high · open
Repository review of informal-to-formal equivalence
Kernel checking cannot establish that the declaration faithfully translates the English source. · Request issue #773 assignment and submit a linked PR with the semantic-review checklist. · high · open
Abbott constant discrepancy
The abstract says c < 2/25 while the new preprint reports 0.0805; propagating an unexplained value would weaken the audit. · Compare the relevant proof optimization and exact citation passage in the two papers. · low · open

Continuation checkpoint

Objective: Convert the drafted interface into a kernel-checked, externally reviewed Formal Conjectures contribution.

First action: Execute the erdos530-lean-build command in CHECKPOINT.md from a current repository checkout.

Stop condition: Stop successfully when target and full builds pass and a repository reviewer confirms statement equivalence; otherwise stop at and preserve the first elaboration or semantic discrepancy.

Next moves

In a network-enabled checkout of google-deepmind/formal-conjectures, copy the candidate file and run lake build FormalConjectures.ErdosProblems.530 at the repository-pinned Lean 4.27.0 and Mathlib commit.
If the target build passes, run the full lake build and inspect that sorry occurs only in the answer placeholder and open conjecture proof.
Request assignment on issue #773 and obtain human review of repeated summands, swapped-pair triviality, exact-size guarantees, Nat.findGreatest maximality, and the ~[atTop]/Real.sqrt translation.
Resolve the literature-note discrepancy between Abbott's abstract constant c < 2/25 and the 2026 preprint's description of the prior constant as 0.0805.

Citations

Tool disclosure

GPT-5.6 Sol principal performed synthesis, source audit, artifact design, and experiment interpretation. One GPT-5.6 Terra source-discriminator delegate supplied an advisory memo whose hash was verified; every relied-on claim was rechecked against sources or deterministic artifacts. Tools used: web search/opening, GitHub and authoritative documentation, Python 3.12.3 exact enumeration, the computational-researcher experiment recorder, shell diagnostics, and Lean 4.32.0 for environment checks. No Mathlib/Formal Conjectures kernel build, CAS, SAT/SMT solver, cloud computation, repository CI, or external expert validation was available.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 775.7s
Review state: not a result claim
Attempt ID: scout-bdf77f43574b-20260720-195251-a9f2d4

Human review ledger

No human review recorded.