[Award claim] JSP-001018 — CN-F90 independent Lean formalization #1727

Entry: JSP-001018 (Erdős problem #1213 — consecutive block sums with equal values)

Recipient placeholder / public ID: @CN-F90 (public GitHub account; personal identity pending written confirmation — placeholder RECIPIENT-JSP-001018-A until then)

Proof repository (our independent formalization): https://github.com/CN-F90/JSP-001018-Lean — pinned commit d21ae5ec35c36122ca0ac2b6d226fa42c2c47bcc. Top theorem JSP001018.erdos_1213. Lean 4.34.0, mathlib v4.34.0. #print axioms = [propext, Classical.choice, Quot.sound]; 0 sorry, 0 admit. Catalog correction PR: #827 (OPEN, MERGEABLE).

Contributions and evidence (distinguish proof / formalization / exposition):

• Mathematics (NOT ours): affirmative answer due to Norbert Hegyvári (Acta Math. Hungar. 48 (1986), 193–200).
• Lean formalization (our contribution): an independent Lean 4 + mathlib certification of Hegyvári's result. We claim ONLY the independent Lean contribution, not the mathematical discovery.
• Identity / attribution basis: the repository CN-F90/JSP-001018-Lean is owned by this account; the pinned commit is authored by CN-F90. If maintainers need more, we can answer a fresh challenge from this account.

Prior art / earlier-parallel formalizations (fully disclosed per policy):

• plby/lean-proofs (src/latest/ErdosProblems/Erdos1213.lean, credited "Codex / GPT-5.6 Sol") contains an earlier, independent complete formalization of this entry.
• PR problems, candidates: add Lean proof and observation candidate for JSP-001018 #45 (Sixtimenight) puts a Lean source directly into the awards repo.
• PR JSP-001018: complete Lean proof with explicit integer interface #723 (CHENLexiao8848) is a further independent complete formalization (external repo).
• PR JSP-001018: complete Lean proof with a harmonic-counting threshold #755 (zjukop3) is a further independent formalization (external repo).
• Issues [Correction] JSP-001018: register existing Lean proof and replay evidence #27 and [Correction] Batch 4: register reproduced existing Lean proof evidence #24 register/request the existing Lean-proof evidence.
• None of these is ours; our formalization shares no code with them. We do not claim first-formalization priority; earlier/parallel complete formalizations have priority. This claim is filed in parallel/independently and does NOT wait for PR JSP-001018: add independent Lean formalization by CN-F90 #827 to merge.

Confirmation status: pending written confirmation (placeholder used; public identity not yet confirmed).

Attribution questions and conflicts: no known personal or professional conflict with the mathematical solver, the maintainers, or the authors of the other formalizations.

Contact (user-authorized public email for this Award Claim form): 2698837476@qq.com

Claim-field conformance update 2026-09-29 (CN-F90, amending our own claim text)

The claim form gained fields after this issue was opened. This section supplies them
without opening a duplicate claim. Nothing here changes what is claimed: the
independent Lean formalization only, never the mathematical discovery.

• Problem link: https://github.com/TheJustinSunPrize/awards/blob/main/problems/README.md (JSP-001018 entry)
• Merged submission PR: contribution PR JSP-001018: add independent Lean formalization by CN-F90 #827 — currently OPEN, not yet merged.
  Under the rule added in PR docs: clarify submission checks and award claim prerequisites #2190 a Lean claim requires a merged contribution PR; we
  therefore do not request acceptance yet and ask that review remain deferred until
  JSP-001018: add independent Lean formalization by CN-F90 #827 merges. A pending PR is stated plainly, not presented as if merged.
• Contribution being claimed: Lean formalization only (not the mathematical solution).
• Original Lean proof repository: https://github.com/CN-F90/JSP-001018-Lean, pinned commit d21ae5ec35c36122ca0ac2b6d226fa42c2c47bcc
  (owned by this same account; not a mirror or copy of another person's proof).
• Follow-up contact email: 2698837476@qq.com (user-authorized, public).
• Identity verification method: GitHub-account control of CN-F90/JSP-001018-Lean and of PR JSP-001018: add independent Lean formalization by CN-F90 #827.
  Status of the mandatory email: NOT YET SENT. The identity-verification email from
  2698837476@qq.com to thejustinsunprize@hejustinsun.com (required by every applicant,
  including Lean-only) is performed by the human owner of that mailbox, not by any
  automation; it is recorded here as outstanding rather than as completed.
• Contribution evidence and attribution clarification: repository ownership by this
  account plus authorship of PR JSP-001018: add independent Lean formalization by CN-F90 #827; no shared or bot account is involved.
• Related claims, attribution questions and conflicts: disclosed above in the original
  body (earlier/parallel formalizations named explicitly); no known conflict. This issue is
  updated in place rather than duplicating it.
• Applicant declarations: we accept declarations 2, 3, 4 and 6 as written. Declaration 1
  (merged contribution PR linked) and declaration 5 (identity-verification email sent) are
  claimed only once those external events occur — today neither has happened, and we do
  not represent otherwise.

Disclosure completeness update 2026-10-22 (CN-F90, amending our own claim text)

For completeness of the disclosure the rules ask for: as of this update the awards corpus contains 16 dedicated public record(s) for JSP-001018, of which 10 were created before our own public record for this problem (2026-09-19T09:48:45Z). The five earliest of those earlier records are listed below as they appear in the public corpus (record number, author, creation time, repository if that record states one). The remaining records are not named individually here, and none of them is adopted as prior art by us: this is a register of what exists, not an adjudication of it.

We have not verified the completeness, validity or kernel status of each listed record, and listing one is not a statement that it is a correct or complete formalization. No priority is asserted, conceded or disputed here beyond what is stated above, and no commit-level timestamp was verified for the records below. This claim continues to request only our own independent Lean formalization.

Creation times are given as recorded; we have not verified commit-level timestamps for every record above and therefore make no priority claim about them. We do not ask maintainers to adjudicate priority here.