[xinkuangsi-spec]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem and proposed change

Problem ID(s): JSP-000503

Current entry: Lean proof | No. Proposed change: mark Lean proof | Yes, 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 upstream formalization; no authorship or award eligibility is claimed.

Proof source

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

• Theorem/file: src/latest/ErdosProblems/Erdos622.lean
• Formalization authors: plby/lean-proofs contributors (per file headers)
• Build instructions: standard Lean 4 + Mathlib project; see the repository's lakefile/lean-toolchain and README.
• Scope: see the linked file for the precise theorem statement covering this catalog entry.

Submission checklist

• I changed only solver attribution, Lean proof information or supporting sources in the relevant catalog.
• I supplied the evidence required for the type of change above.
• The mathematical result fully solves the original problem as stated in the linked source; the Lean proof is complete at the specified commit, with no sorry, admit or added unproved assumptions.
• This PR contains no proof source files, archives, binaries or vendored dependencies.
• The Lean reference identifies a commit contained in the named branch and the exact version for review.