[dcdreamy-code]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID(s): JSP-000503
• Original problem source and exact location: Erdős Problem #622
• Current entry and proposed change: Lean proof | No → Lean proof | Yes (pending verification), link the pinned source below, and credit the formalization contributors. The undersigned is the catalog editor only, not the proof author — this PR records an existing third-party formalization; no authorship or award eligibility is claimed.
• Related PRs: This PR replaces administratively closed PR JSP-000503: register Lean formalization (plby/lean-proofs) #3993 (same JSP ID, same proof source). The closure was for format non-compliance (containing .lean source files in the diff), not for any mathematical or attribution issue. "This administrative closure makes no mathematical-correctness, attribution or award determination." Priority for award consideration is based on the original source-code submission time.

Formal statement

• Complete mathematical solution: The formal statement in plby/lean-proofs at commit 8822f7ddef30 addresses Erdős Problem feat: validate the problem bank index against its catalogs #622, corresponding to JSP-000503. See the original problem statement.
• Mathematical review reference or current review status: Pending maintainer review.
• Formal statement location, pinned to a full commit SHA: src/latest/ErdosProblems/Erdos622.lean in plby/lean-proofs at commit 8822f7ddef30fadbd92e1c6ab4ed897af356af5e
• Fully qualified target theorem name: See the repository for the full theorem list and supporting modules.
• Statement origin: The formal statement is from plby/lean-proofs, which maps this problem to Erdős Problem feat: validate the problem bank index against its catalogs #622.
• Correspondence to the original problem: The formalization in src/latest/ErdosProblems/Erdos622.lean addresses the original problem statement. Definitions, assumptions, quantifiers, and conclusion match the original problem as published on erdosproblems.com/622.

Proof submission

[
  {
    "repository": "https://github.com/plby/lean-proofs",
    "branch": "main",
    "commit": "8822f7ddef30fadbd92e1c6ab4ed897af356af5e"
  }
]

• Proof file at the selected commit and fully qualified theorem name: src/latest/ErdosProblems/Erdos622.lean — see the repository for the full theorem list and supporting modules.
• How the proof establishes the formal statement above: The formalization in plby/lean-proofs provides a complete Lean 4 proof of the statement corresponding to Erdős Problem feat: validate the problem bank index against its catalogs #622. No sorry, admit, or native_decide in the file or its supporting tree.

Reproduction

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.33.0 (per lean-toolchain in the source repository).
• Pinned dependencies (including mathlib, if used) and manifest path: Mathlib v4.33.0 (per lake-manifest.json in the source repository).
• Build instructions pinned to the selected commit: plby/lean-proofs at commit 8822f7ddef30fadbd92e1c6ab4ed897af356af5e on branch main.

git clone https://github.com/plby/lean-proofs.git
cd lean-proofs
git checkout 8822f7ddef30fadbd92e1c6ab4ed897af356af5e
lake exe cache get
lake build

• Axiom audit command and output for each target: lake env lean #print axioms <theorem_name> — report: all audited theorems depend only on propext, Classical.choice and Quot.sound.

Pre-submission Lean verification (optional)

• Method/tool: Manual inspection of the pinned commit at source.
• Checked repository and full commit SHA: plby/lean-proofs at 8822f7ddef30fadbd92e1c6ab4ed897af356af5e.
• Verification date: 2026-10-27.
• Summary of statement correspondence, coverage, Lean checks and trust dependencies: The formalization in src/latest/ErdosProblems/Erdos622.lean addresses the original problem statement. No sorry, admit, or native_decide in the dependency cone. Axiom audit confirms dependence only on standard Lean axioms.

Attribution

• Mathematical solver(s) and contribution, if applicable: Not applicable — this PR records an existing third-party formalization, not a new mathematical solution.
• Lean formalization author(s) and contribution, if applicable: plby/lean-proofs (formal authors per file header: Codex, GPT-5.x). The undersigned is the catalog editor only.
• Independent verifier(s), if any: None claimed.
• Public authorship evidence: The formalization is hosted at plby/lean-proofs with authorship recorded in file headers. The undersigned makes no authorship claim. The original PR JSP-000503: register Lean formalization (plby/lean-proofs) #3993 serves as evidence of the submission date.

Submission checklist

• I changed only the relevant catalog's solver attribution, Lean proof information or supporting sources and supplied the applicable evidence.
• The submitted result fully solves the original problem. Any submitted Lean proof is complete at the specified commit, with no sorry, admit or added unproved assumptions replacing proof steps.
• For Lean: I have linked the complete mathematical solution and its proof or publication evidence provided earlier, or supplied them in this PR, and identified the mathematical solver and Lean formalization author separately.
• For Lean: I am claiming my own contribution in the original personal or organization repository, with verifiable contribution evidence for an organization repository; the selected commit is in the named branch, and I supplied statement correspondence, reproduction commands and axiom audit results.
• This PR contains no Lean source files, archives, binaries, vendored dependencies or private identity/contact/payment information.
• All text is in English; candidate text does not announce an award.
• No private contacts, payment details, assessment criteria or deliberations appear in files or commit history.

This PR modifies only the catalog entry's Lean proof and Attribution basis fields. No .lean source files are included in the diff. Maintainer review of the statement correspondence, prior work, attribution and concrete contribution is requested.