[zhangjun725]

Updated on 2026-10-26: rebased onto c06d67a to resolve the conflict with #5135, which removed the Pending verification state and set JSP-000448 to Eligible to claim: Yes (claim statuses Unclaimed). This PR no longer touches eligibility or claim statuses; it only changes Lean proof to Yes with the source link and adds the Attribution basis row.

Updated on 2026-10-10: the explicit bound k(n-2)+3 is now stated for n ≥ 2, with the n = 1 natural-number-subtraction convention spelled out (raised in review of google-deepmind/formal-conjectures#6028; the linked commit 828ad6f is unchanged, the same docstring fix is in erdos557 9d26a79). A clean replay of the linked commits is at docs/replay-2026-10-10.md.

Rebased on 2026-10-09 onto 1687700 (attribution-basis count is now 85 → 86 after the OpenAI results update). Previously rebased on 2026-09-24 onto 1d1db84 (mathematical-solution evidence now required for Lean submissions; see the new Mathematical solution section below). Previously rebased on 2026-09-22 onto the separate solver/Lean claim-status columns and rewritten against the current PR template. The proof repository and selected commit are unchanged from the original submission on 2026-09-17.

Submission type

• Mathematical solver information
• Lean proof or formalization author information

This is a Lean-only submission. The complete mathematical solution is already recorded in the catalog (JSP-000448 Current status: Solved, with its publication evidence) and is not changed by this PR; it is restated with evidence in the next section as required by 1d1db84.

Mathematical solution (evidence for the Lean submission)

Per the submission requirements, the mathematical solution and its supporting evidence for JSP-000448 are:

1. Already recorded in this repository. The catalog entry for JSP-000448 has Current status: Solved on main before this PR, with Publication details [ReSt26] The Erdős-Sós conjecture in dense graphs (arXiv:2609.05417, 2026). This PR does not change Current status or Publication details.
2. The complete solution for all n. Reed and Stein [ReSt26] prove the Erdős–Sós conjecture for k ≥ εn with n large and deduce R_k(T) ≤ k(n-2)+3 in that range. The unrestricted statement follows from the full Erdős–Sós theorem, which this repository already records as solved with a complete Lean proof at JSP-000439 (Erdos548.erdos_548; tadamcz/erdos548 @ 82ffb751f3d37768927df9239ed08439bbe0dd09, found by GPT-6 Astra, benchmark of Adamczewski and Bloom), combined with the pigeonhole reduction recorded on the problem page erdosproblems.com/557 ("Implied by the Erdős-Sós conjecture [548]"). erdosproblems.com lists JSP-000307: Conditional theorem for strictly decreasing largest prime factors #557 as PROVED (LEAN) on that basis.
3. The reduction, in full. Colour the edges of K_m with k colours, m = k(n-2)+3. Some colour class H has at least binom(m,2)/k edges. Since m ≥ k, 2k|E(H)| ≥ m(m-1) = k(n-2)m + m ≥ k(n-2)m + k, so |E(H)| ≥ (n-2)m/2 + 1, which is the Erdős–Sós edge-density hypothesis for trees on n vertices; hence H ⊇ T. Using the sharp form (2|E| ≤ (n-2)m when the tree is absent) instead gives k(n-2)+2, and k(n-2)+1 for odd n and even k by parity. This argument is exactly what the submitted Lean development formalises, so the mathematical solution and its machine-checked proof coincide here.
4. Independent statement of the sharp bounds. The values k(n-2)+2 and k(n-2)+1 are those recorded by LouisD on the problem page (comment of 2026-09-04), and are best possible (attained by stars K_{1,n-1}).

The mathematical solver credit is unchanged by this PR: it remains with the authors of [ReSt26] and the JSP-000439 record, not with the submitter. This PR claims only the Lean formalization role.

Problem

• Problem ID(s): JSP-000448
• Original problem source and exact location: Erdős and Graham, On partition theorems for finite graphs, Infinite and finite sets (Colloq., Keszthely, 1973), Colloq. Math. Soc. János Bolyai 10 (1975), 515–527, p. 516; catalogued as erdosproblems.com/557 ([ErGr75, p. 516]).
• Current entry and proposed change:
  • Lean proof: Reported; standalone Lean source not located … → Yes — Lean source, with formalization contributors.
  • Attribution basis: new row (mathematical: paper/report authors; Lean: project authorship via formalization.yaml).
  • Eligible to claim: unchanged (Yes, as set in docs: update MathDB pilot, renumber catalog and simplify eligibility #5135).
  • Problem index: Lean proof Reported; standalone source not located → Yes; Eligible (Yes), Solver claim status and Lean claim status (Unclaimed) unchanged.
• Related issue: [Correction] JSP-000448: standalone Lean proof now available (Lean proof / Eligible to claim / Claim status) #569 (correction issue opened before the claim flow existed; this PR supersedes its proposed edits).
• Related PRs and how this contribution differs: no other PR registers a Lean formalization for JSP-000448 (searched open, merged and closed PRs for JSP-000448, 557 and "multicolor Ramsey"). JSP-000439 already records the Erdős–Sós Lean proof; this submission is a separate development that imports it and is not a copy or mirror of it.
• For solver/publication updates: not applicable — Current status and Publication details are unchanged.

Formal statement

• Mathematical solution and review reference: the problem is implied by the Erdős–Sós conjecture (JSP-000439 / erdosproblems.com/548), which is recorded as solved with a Lean proof. The deduction is the pigeonhole argument recorded on erdosproblems.com/557; Reed and Stein (arXiv:2609.05417) derive the same bound k(n-2)+3 from their dense-graph case for n large in terms of k. The submitted formalization establishes it for all n.
• Formal statement location, pinned to a full commit SHA: Erdos557/Basic.lean#L153
• Fully qualified target theorem name: Erdos557.erdos_557

theorem erdos_557 :
    ∃ c : ℕ, ∀ (k n : ℕ) (T : SimpleGraph (Fin n)), T.IsTree →
      multicolourRamsey k T ≤ k * n + c

Supporting targets at the same commit:

Theorem	Location	Statement
Erdos557.erdos_557_explicit	Basic.lean#L96	every k-colouring of K_{k(n-2)+3} has a monochromatic copy of every tree on n vertices
Erdos557.multicolourRamsey_le_of_isTree	Basic.lean#L147	R_k(T) ≤ k(n-2)+3, natural-number subtraction (the ordinary bound for n ≥ 2)
Erdos557.erdos_557_tight / multicolourRamsey_le_tight	Tight.lean#L76, #L108	R_k(T) ≤ k(n-2)+2 for n ≥ 2
Erdos557.erdos_557_tight_odd / multicolourRamsey_le_tight_odd	Tight.lean#L91, #L114	R_k(T) ≤ k(n-2)+1 for odd n, even k ≥ 2

• Statement origin: proposed statement requiring review. The problem had no formalised statement upstream (erdosproblems.com/557 lists "Formalised statement? No"). The same statement shape, with the definition named multicolourGraphRamsey, is proposed to Google DeepMind's Formal Conjectures in google-deepmind/formal-conjectures#6028 (all checks passing; maintainer-labelled solution found; reviewed by a community contributor with no blocking statement mismatch found).
• Correspondence to the original problem:
  • R_k(G) — the original asks for "the minimal m such that if the edges of K_m are k-coloured then there is a monochromatic copy of G". Formalised as Erdos557.multicolourRamsey k G = sInf {n | ∀ C : TopEdgeLabeling (Fin n) (Fin k), ∃ i, G.IsContained (C.labelGraph i)}. SimpleGraph.TopEdgeLabeling (Fin n) (Fin k) is Mathlib's type of functions from the edge set of the complete graph on Fin n to Fin k, i.e. exactly a k-colouring of the edges of K_n; C.labelGraph i is the graph of edges of colour i; T.IsContained H is Mathlib's containment as a (not necessarily induced) subgraph, i.e. a copy of T in H. sInf of the set of sufficient m is the "minimal m", and the explicit theorems exhibit a member of that set, so the infimum is attained and finite.
  • Trees on n vertices — T : SimpleGraph (Fin n) with T.IsTree (Mathlib: connected and acyclic). Quantified over all n and all such T.
  • ≤ kn + O(1) — formalised as a single constant c independent of k, n and T (∃ c, ∀ k n T, …), and c = 3 is exhibited. This is the strongest reading of O(1); a constant depending on k would be weaker, so the submitted statement implies that reading as well.
  • All required cases — k ranges over all naturals including 0 (degenerate: no 0-colouring of a graph with an edge exists, and the bound holds); n ≥ 1 for every tree (IsTree requires a vertex, so n = 0 is vacuous). The explicit bound k(n-2)+3 is meant for n ≥ 2; the Lean statement uses natural-number subtraction, so for the one-vertex tree it reads R_k(T) ≤ 3, which holds (indeed R_k(T) ≤ 2), whereas the ordinary-subtraction formula would fail at n = 1 for k ≥ 3. The main statement R_k(T) ≤ kn + 3 holds for all n. The tight variants additionally require n ≥ 2, stated explicitly in their hypotheses.
  • Scope note — the mathematical difficulty lies in the Erdős–Sós theorem recorded at JSP-000439; this development formalises the reduction and imports that proof unchanged. It is offered as a Lean contribution for JSP-000448, not as a new mathematical result.

Proof submission

[
  {
    "repository": "https://github.com/zhangjun725/erdos557",
    "branch": "main",
    "commit": "828ad6fdb5d0f1a72b8dcd812f4c91c285570ff6"
  }
]

• Proof file at the selected commit and fully qualified theorem name: Erdos557/Basic.lean — Erdos557.erdos_557; tight bounds in Erdos557/Tight.lean.
• How the proof establishes the formal statement: statement and proof share a file (no separate challenge/solution split). exists_labelGraph_choose_two_le_mul_ncard gives the pigeonhole step (some colour class of K_m has at least binom(m,2)/k edges); key_ineq turns that into the edge-density hypothesis of Erdos548.erdos_548 when m = k(n-2)+3, which then contains T. multicolourRamsey_le_of_isTree applies Nat.sInf_le, and erdos_557 weakens k(n-2)+3 to kn+3. The tight variants use the sharp lemma Erdos548.tree_free_edge_bound (2|E| ≤ (n-2)m when the tree is absent) instead of the advertised statement, plus a parity argument for the +1 case.
• The only non-Mathlib dependency is tadamcz/erdos548, pinned to commit 82ffb751f3d37768927df9239ed08439bbe0dd09 — the same Lean source already recorded for JSP-000439. It is imported unmodified as a Lake dependency; no file of it is copied into this repository.

Reproduction

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.28.0, lean-toolchain
• Pinned dependencies and manifest path: mathlib v4.28.0 (8f9d9cff6bd728b17a24e163c9402775d9e6a365) and Erdos548 (82ffb751f3d37768927df9239ed08439bbe0dd09), pinned in lakefile.toml and lake-manifest.json
• Build instructions pinned to the selected commit: README.md#building and docs/verification.md
• Commands for setup, clean build and checking each target theorem:

git clone https://github.com/zhangjun725/erdos557 && cd erdos557
git checkout 828ad6fdb5d0f1a72b8dcd812f4c91c285570ff6
lake exe cache get     # mathlib oleans
lake build             # also builds the pinned erdos548 dependency
lake env lean scripts/check_axioms.lean

• Axiom audit command and output for each target: scripts/check_axioms.lean runs CollectAxioms (the same information as #print axioms) on every target and fails if anything outside propext, Quot.sound, Classical.choice appears. Output at commit 828ad6f, re-run 2026-09-22:

Erdos557.erdos_557_explicit depends on axioms: [propext, Quot.sound, Classical.choice]
Erdos557.erdos_557 depends on axioms: [Classical.choice, propext, Quot.sound]
Erdos557.multicolourRamsey_le_of_isTree depends on axioms: [Classical.choice, propext, Quot.sound]
Erdos557.erdos_547_explicit depends on axioms: [propext, Quot.sound, Classical.choice]
Erdos557.erdos_547 depends on axioms: [propext, Quot.sound, Classical.choice]
Erdos557.erdos_557_tight depends on axioms: [propext, Quot.sound, Classical.choice]
Erdos557.erdos_557_tight_odd depends on axioms: [propext, Quot.sound, Classical.choice]
Erdos557.multicolourRamsey_le_tight depends on axioms: [Classical.choice, propext, Quot.sound]
Erdos557.multicolourRamsey_le_tight_odd depends on axioms: [propext, Classical.choice, Quot.sound]

No target depends on sorryAx; grep -rn sorry Erdos557 Erdos557.lean returns nothing. (Erdos557.erdos_547* are Erdős problem #547, proved by the same reduction; not part of this submission, listed for completeness of the audit.)

Pre-submission Lean verification (optional)

• Method/tool and version: local build and axiom audit only (Lean v4.28.0, mathlib v4.28.0), not the lean-verify skill.
• Checked repository and full commit SHA: https://github.com/zhangjun725/erdos557 at 828ad6fdb5d0f1a72b8dcd812f4c91c285570ff6 — identical to the submitted version.
• Verification date, actual conclusion and limitations: 2026-09-17, re-run 2026-09-22. lake build completes with no errors or warnings; all targets depend only on the three standard axioms. Limitations: this is the author's own build, not an independent replay; the imported Erdős–Sós proof was not independently re-derived, only rebuilt from its pinned commit; correspondence between the informal problem and the Lean statement is argued above but has not been confirmed by the erdosproblems.com curators.
• Summary: statement correspondence as set out under Formal statement; coverage includes all k and all trees on n ≥ 1 vertices (the explicit bound uses natural-number subtraction at n = 1; n ≥ 2 for the tight variants); Lean checks are a clean build plus the axiom audit; trust dependencies are Lean core, mathlib v4.28.0 and the pinned erdos548 commit.
• Report/log links: docs/verification.md (build log, axiom output, reproduction steps). GitHub Actions is unavailable on my account, so the repository's CI workflow has not run; the log is local and reproducible with the commands above.

Attribution

• Mathematical solver(s): unchanged by this PR. Reed and Stein (arXiv:2609.05417) for the dense case; the deduction from the Erdős–Sós theorem is the pigeonhole argument recorded on the problem page. The Erdős–Sós theorem itself is credited at JSP-000439 (GPT-6 Astra; repository prepared by Tom Adamczewski).
• Lean formalization author(s): Jun Zhang (@zhangjun725), with Claude (Anthropic) — I selected the problem, directed and reviewed the development, and take responsibility for it. The AI assistant is credited as a tool in the repository's formalization.yaml under automation, following the mathlib-initiative format.
• Independent verifier(s): none. (A community contributor reviewed the statements in the Formal Conjectures PR linked above; that is not an independent replay of the proof.)
• Public authorship evidence: the repository is owned by my submitting account, zhangjun725/erdos557. All commits are authored by that account; see the commit history — the initial public push and the selected commit are both dated 2026-09-17. Authorship and roles are also recorded in formalization.yaml.

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 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.

[zhangjun725]

The linked Lean development has since been strengthened to the best-possible bounds R_k(T) ≤ k(n-2)+2 (and k(n-2)+1 for odd n, even k) in Erdos557/Tight.lean (commit 828ad6f); the record changes in this PR are unaffected. Details in #569.

[zhangjun725]

Update, 2026-10-12: the formal statements are now merged upstream in Formal Conjectures, google-deepmind/formal-conjectures#6028 (merged 2026-10-11). FormalConjectures/ErdosProblems/557.lean contains erdos_557 and its explicit, tight and tight_odd variants, all tagged research solved with formal_proof links to the Lean development registered here. Erdős #547 is marked research solved as well.

As part of that review, a reviewer independently replayed the linked commits c4e0ab13 and 828ad6fd, including the pinned Erdős–Sós dependency (review):

Bridges reproducing the FC predicates and binders passed Comparator's statement, axiom and kernel checks on the proofs' pinned Lean/Mathlib 4.28.0. All five claims use only propext, Classical.choice and Quot.sound.

This gives third-party verification of the Lean development in addition to my own replay log (docs/replay-2026-10-10.md). This PR is still mergeable against current main, and I'm happy to make any changes needed.

[zhangjun725]

Gentle ping @Federico2014 — this PR is rebased onto current main (fd8fa66) and conflict-free. Following the convention from #5049, it now leaves Eligible to claim at Pending verification and only registers the Lean source and attribution for JSP-000448; the Lean development has been independently replayed in google-deepmind/formal-conjectures#6028. Happy to adjust anything. Thanks!