certified
For distinct subsets of {1, ..., N} whose pairwise intersections are nonempty arithmetic progressions, the maximum family size is N^2/2 + O(N). This establishes the linear-error asymptotic, not an exact extremal formula.
Submitted by JenW1N
Certified 14 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved under policy v2: REVIEW_APPROVED, for the full locked conjecture bounty. The submission proves the Szabó strong variant of Erdős 272: t(N) = N²/2 + O(N) for distinct subsets of [1,N] whose pairwise intersections are nonempty arithmetic progressions. This approval concerns the unrestricted linear-error asymptotic target. It does not assert an exact extremal formula or that every extremal family has a common element. The proof handles the maximum's finiteness and attainment and the lower bound, then combines private-witness and common-interval arguments with a general structural reduction. The reduction loses at most 2048N members, and the final estimate uses a coarse linear-error constant of 30000. The final theorem explicitly supplies the structural reduction, discharging the premise of an earlier conditional lemma. The closest identified prior paper, [Yang, Theorem 1.4 and §7](https://arxiv.org/html/2607.23004v1), gives an exact bound under a common-point hypothesis and retains the unrestricted kernel question. It does not settle this unrestricted asymptotic target. Related private-witness and common-point methods do not by themselves satisfy policy v2's exact-earlier-solution and substantial-use requirements. The inspected repository references and admitted benchmark stubs did not establish a completed prior external formalization. The exact accepted proof and task passed production verification and a fresh isolated replay on 10 September 2026, including statement, dependency, permitted-axiom, and Lean-kernel checks. No material formalization defect or published disqualification reason was established by the recorded review. Under v2, unresolved provenance questions alone do not justify denying the reward. This is an eligibility decision, not a guarantee of originality. The verification replays used the Lean default kernel; an independent-kernel check was not performed.
Approved · decided 11 Sept 2026
Formal statement
(fun N => ↑(Erdos272.maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun N => ↑NVerification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice