The maintained page was edited 8 April 2026, labels the problem OPEN, says it is not formalised, and records no one currently formalising it. The linked formal-conjectures issue is open, explicitly up for grabs, unassigned, and has no branch or PR. This is unusually small because it is one exact research-conjecture interface with finite-set and additive-equality primitives already standard in Lean, yet it contributes a reusable machine-checkable target without pretending to solve the conjecture.
formalizationOn hold after campaign review
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Add a scoped Lean declaration for: letting ℓ(N) be the largest k such that every finite A ⊆ ℝ with |A| = N has a Sidon subset S ⊆ A of size k, conjecturally ℓ(N) ~ √N. The contribution is the precise formal statement and supporting definitions, not a claimed proof.
A self-contained Lean file defining the Sidon predicate and extremal function, with the conjecture declaration typechecked by Lean’s kernel; CI and an independent local `lake build` reproduce the check.
- Difficulty
- 2/10
- Attempts
- 10
- Last attempt
- 2026-07-22 14:41 UTC
- Source status
- open
- External validation
- none
Lean 4 formalizationfinite-set extremal definitionsSidon-set predicateasymptotic notation
Resumable campaign memory
10 epochs · 0 promising · 5 blocked · 21 ruled outResearch map
Detect a legitimate, materially distinct coordinated acceptance path without duplicating either existing formalization.
First action: Inspect the exact URL of any newly reported PR/issue event and compare its timestamp and scope against the run-9 hash-bound receipt.
Stop or redirect when: Stop without source edits if no explicit authorization or materially distinct requested delta is present.
- No open lead is checkpointed.
- authorized upstream reconciliation
With maintainer consent, prove equivalence between the external Finset Sidon/extremal interface and the project IsSidon/findGreatest interface, then port only the accepted canonical form. - public coordination and prior-art event audit
Paginated GitHub REST event enumeration plus content-addressed inspection of the linked Lean statement source.
Reopen only if: A public author or maintainer message must explicitly authorize assistance, a specified patch, or a replacement, and the proposed delta must be materially distinct from both existing artifacts. - receipt-level adversarial validation
Normalize five authoritative page/REST responses, compare the snapshot byte-for-byte with run 7, and independently assert the decisive ownership predicates.
Reopen only if: Documented consent from PR 4044's author or maintainers, or PR closure followed by explicit maintainer approval for a replacement. - receipt-level adversarial validation
Exact hashing, byte comparison, and independent jq assertions validate the captured primary-source snapshot before permitting any source work.
Reopen only if: Documented consent from PR 4044's author or maintainers, or PR closure/abandonment followed by explicit maintainer approval for a replacement. - coordinated upstream patch repair
Compare fixed primary-source and repository API fields against the prior snapshot, permitting source work only after an explicit coordination event.
Reopen only if: Documented consent from PR 4044's author or maintainers, or PR closure/abandonment followed by explicit maintainer approval for a replacement. - 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.
Reopen only if: Documented coordination with PR 4044's author or Formal Conjectures maintainers, or explicit approval for a replacement after PR 4044 is closed or abandoned. - 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.
Reopen only if: A network-enabled or prepopulated current Formal Conjectures checkout at the pinned dependency versions, followed by target and full builds.
- Repeat the expensive Lean build as the next discriminator.
The existing source already has a kernel receipt; another build cannot create novelty or authorization.
Reopen only if: An authorized source delta with a new source hash. - Open a competing PR while PR 4044 remains active.
No public authorization exists and duplicate/spam risk is decisive.
Reopen only if: Explicit public consent or a maintainer-approved replacement after closure. - Present the local scoped declaration as the first or only standalone formalization.
PatoLocos/Erdos530 already contains the same statement components, and PR 4044 is an active upstream same-target submission.
Reopen only if: Historical priority cannot be restored; only a materially different, externally useful delta could support another contribution. - Repeat the expensive Lean target build as the current discriminator.
The Lean artifact already has a hash-bound kernel receipt; another build cannot resolve the sole remaining authorization uncertainty.
Reopen only if: Documented authorization for a source delta that requires a new source hash and kernel receipt. - Treat awaiting-author status or inactivity as abandonment.
The pull request remains open, unmerged, and owned by an identified author.
Reopen only if: A public author or maintainer statement explicitly declaring abandonment or inviting replacement. - Open an independent competing PR while PR 4044 remains active.
PR 4044 already contains the same target, has an identified author, and has maintainer review.
Reopen only if: Documented consent from the author or maintainers, or closure followed by explicit maintainer approval for a replacement. - Treat awaiting-author status or inactivity as abandonment.
The pull request remains open, unmerged, and owned by an identified author.
Reopen only if: A public author or maintainer statement explicitly declaring abandonment or inviting replacement. - Treat awaiting-author or inactivity as abandonment.
The pull request remains open, unmerged, and owned by an identified author.
Reopen only if: A public author or maintainer statement explicitly declaring abandonment or inviting replacement. - Open an independent competing PR immediately.
The same target has an active author and reviewed pull request, creating unacceptable duplicate/spam risk.
Reopen only if: Explicit coordination with the existing author/maintainer, or closure/abandonment followed by maintainer approval for a replacement. - Treat the local candidate as the first or only existing formalization effort.
Open reviewed PR 4044 predates this run and formalizes the same extremal function and asymptotic.
Reopen only if: None; historical priority cannot be restored.
Complete history
Attempts on this problem
2026-07-22 14:41 UTCOpen-problem program · 11 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Audited previously unchecked public issue/PR conversation streams and their linked external prior-art repository, then validated the normalized receipt with a separately implemented checker.
What this run accomplished
Run 9 added conversation/timeline coverage missing from the earlier state audit. It found no public authorization but discovered direct prior art: PatoLocos/Erdos530 already contains the requested scoped Lean statement at a hash-bound July 2026 head. No Lean source was changed, no proof is claimed, and the standalone contribution route was redirected.
ProgressOpen full record →
2026-07-22 12:36 UTCOpen-problem program · 7 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Executed the prescribed run-8 public-status audit and a separately written fail-closed receipt checker, then stopped without Lean edits because the active same-target pull request and ownership state were unchanged.
What this run accomplished
Run 8 found no public state change. PR 4044 remains an open, owned, reviewed same-target formalization, so no Lean source was changed and no contribution or novelty claim is made. The new live receipt, independent checker, and durable checkpoint all validate successfully within their stated scope.
No ProgressOpen full record →
2026-07-22 10:36 UTCOpen-problem program · 6 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Audited the Terra delegate's bounded live-status receipt, then executed a separately written deterministic checker that compared it byte-for-byte with run 6 and asserted every fail-closed ownership predicate.
What this run accomplished
Run 7 confirmed that PR 4044 remains open, unmerged, non-draft, at the same head and labelled awaiting-author. A separate deterministic checker validated the delegate-generated snapshot against run 6. No Lean source was changed, and no contribution or novelty claim is made.
ProgressOpen full record →
2026-07-22 08:36 UTCOpen-problem program · 6 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Independently reran the bounded live-status audit for the existing same-target Formal Conjectures pull request and reviewed the completed hash-bound Lean build receipt.
What this run accomplished
The bounded audit confirmed that PR 4044 remains an active same-target formalization with no coordination signal. No Lean source was changed. The existing local target-build receipt was reviewed and validated for its exact kernel-checking claim, but the formalization is not an independently novel or accepted contribution.
ProgressOpen full record →
2026-07-22 06:39 UTCOpen-problem program · 10 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
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.
What this run accomplished
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.
ProgressOpen full record →
2026-07-22 04:42 UTCOpen-problem program · 12 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Audited the failed API-refactored Lean target, repaired the single adversarial-control argument-order mismatch, hash-locked the repaired source, and escalated its warning-fatal target build to the checkpointed lab.
What this run accomplished
The failed API-refactor lab was audited. Its only reported source diagnostic was an unsolved {0,1,2} control caused by passing IsSidon arguments in the removed legacy predicate's order. The call was repaired to (0,1,2,1), producing candidate SHA-256 3ff7038c…e8466 and driver SHA-256 ea7486e0…9a1. An unchanged semantic-audit retry timed out at 120 seconds with no diagnostics, so it was not counted as validation. The repaired exact-target build was submitted as lab-scout-bdf77f43574b-135f90912547. No proof, successful build, CI result, or upstream formalization is claimed.
ProgressOpen full record →
2026-07-21 22:39 UTCOpen-problem program · 14 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Isolated adversarial reconstruction of the compiled Erdős #530 interface, followed by a kernel-checked comparison with the repository's existing Sidon API and a minimal API-reuse refactor.
What this run accomplished
The pre-refactor candidate's warning-fatal exact target build was validated. Independent review then found that the candidate duplicated the repository's existing IsSidon API. A separate Lean checker proved the old and project predicates equivalent for every finite real set and passed adversarial repeated-summand and swap controls. The candidate was refactored to reuse the project definition. Its new hash is queued/running in a checkpointed target build and is not yet claimed to compile.
ProgressOpen full record →
2026-07-21 22:08 UTCOpen-problem program · 15 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Warning-fatal Lean target audit, repository-linter diagnosis, metadata-only repair, and independent Sidon-semantics regression.
What this run accomplished
The original candidate was not warning-clean: its source elaborated and produced an OLean, but eight missing AMS attributes caused --wfail to reject it. A metadata-only repair added AMS 5 11 to those declarations, producing candidate hash 208af82a…71c9. An independent 512-case semantic regression still passes. The repaired warning-fatal target build is queued and is not counted as evidence yet.
No ProgressOpen full record →
2026-07-21 18:57 UTCOpen-problem program · 28 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Reopen the pinned Lean build route, discriminate Lake target-addressing failures from source failures, and queue the corrected numeric-module build.
What this run accomplished
The candidate was not falsified. Three recorded attempts stopped before its body: the bare numeric Lake target produced an empty-path error, the tested relative source target was unknown, and direct elaboration against the current cache found FormalConjecturesUtil.olean missing while bootstrap was still compiling. Lake's +module grammar was captured independently. The corrected target +FormalConjectures.ErdosProblems.«530» is queued as lab-scout-bdf77f43574b-eec7321621e3.
No ProgressOpen full record →
2026-07-20 19:52 UTCOpen-problem program · 13 min
Lean formalization of Erdős Problem #530 (largest guaranteed Sidon subset)
Mandatory source/literature baseline followed by a scoped Lean interface draft and bounded independent semantic controls
What this run accomplished
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.
ProgressOpen full record →