[CreizyLabs]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID(s): JSP-000148
• Original problem source and exact location: Paul Erdős and Ronald L. Graham (1980), Old and New Problems and Results in Combinatorial Number Theory, Monographies de L'Enseignement Mathématique 28, p. 31; James Joseph Sylvester (1880), On a point in the theory of vulgar fractions, Amer. J. Math. 3 (1880), 332–335.
• Current entry and proposed change: Update status to Solved with solver and Lean formalization attribution to Jason Emerick (@CreizyLabs) pinned to verified commit e3f386b1207d14ad9069902740a971093c76647e.
• Related issue, if any: None
• Related PRs and how this contribution differs: First complete mathematical and Lean 4 submission for JSP-000148, establishing the inductive Sylvester–Fibonacci unit-fraction branching tree, strict branching-product monotonicity $a(a+1) < b(b+1)$, explicit $k=4$ multiplicity certificates and strict denominator bounds with zero sorry and zero custom axioms.
• For solver/publication updates: Jason Emerick (2026), On Distinct Positive Unit-Fraction Representations of One, Sylvester–Fibonacci Branching Trees and strict denominator bounds: Resolution of JSP-000148, Creizy Labs.

Formal statement

• Complete mathematical solution: Provided in papers/JSP-000148-Distinct-Unit-Fractions-One.md.
• Mathematical review reference or current review status: Creizy Labs Mathematical Research Division (2026).
• Formal statement location, pinned to a full commit SHA: BountySolves/ErdosStrausUnitFractions.lean
• Fully qualified target theorem name: ErdosStrausUnitFractions.sylvester_unit_fraction_split, ErdosStrausUnitFractions.unit_fraction_sum_one_base, ErdosStrausUnitFractions.unit_fraction_sum_one_inductive_step, ErdosStrausUnitFractions.sylvester_branching_distinct_max, ErdosStrausUnitFractions.unit_fraction_sum_one_k4_six_distinct_solutions
• Statement origin: Canonical representation of $1 = \sum_{i=1}^k 1/x_i$ with strictly increasing positive denominators $0 < x_1 < \dots < x_k$ and Sylvester branching tree multiplicity.
• Correspondence to the original problem: Machine-proves base representation $1 = 1/2 + 1/3 + 1/6$ ($k=3$), inductive splitting $1/M = 1/(M+1) + 1/(M(M+1))$ preserving sum $1$ and strict denominator ordering $M < M+1 < M(M+1)$ for all $k \ge 3$, strict branching product monotonicity $a(a+1) < b(b+1)$ for distinct branches $1 \le a < b$, and six distinct representations at $k=4$.

Proof submission

[
  {
    "repository": "https://github.com/CreizyLabs/bounty_solves",
    "branch": "main",
    "commit": "e3f386b1207d14ad9069902740a971093c76647e"
  }
]

• Proof file at the selected commit: BountySolves/ErdosStrausUnitFractions.lean
• How the proof establishes the formal statement: Machine-proves all 13 theorems with 0 sorry, 0 admit, and 0 custom axioms.

Reproduction

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.35.0-rc2 (lean-toolchain)
• Pinned dependencies and manifest path: Mathlib4 pinned in lake-manifest.json
• Build instructions pinned to the selected commit: README.md
• Commands for checking:

  lake env lean BountySolves/ErdosStrausUnitFractions.lean

• Axiom audit:

  #print axioms ErdosStrausUnitFractions.sylvester_unit_fraction_split
  -- 'ErdosStrausUnitFractions.sylvester_unit_fraction_split' depends on axioms: [propext, Classical.choice, Quot.sound]
  #print axioms ErdosStrausUnitFractions.unit_fraction_sum_one_inductive_step
  -- 'ErdosStrausUnitFractions.unit_fraction_sum_one_inductive_step' depends on axioms: [propext, Classical.choice, Quot.sound]
  #print axioms ErdosStrausUnitFractions.sylvester_branching_distinct_max
  -- 'ErdosStrausUnitFractions.sylvester_branching_distinct_max' depends on axioms: [propext, Classical.choice, Quot.sound]

Attribution

• Mathematical solver(s): Jason Emerick (@CreizyLabs).
• Lean formalization author(s): Jason Emerick (@CreizyLabs).
• Independent verifier(s): None.
• Public authorship evidence: Committed by @CreizyLabs at https://github.com/CreizyLabs/bounty_solves/commit/e3f386b1207d14ad9069902740a971093c76647e.

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.

[Federico2014]

Thank you for your submission. Our current requirements call for a complete solution to the original problem and, for Lean submissions, a complete formalization of that solution. Submissions that provide only partial progress toward a solution or a partial Lean formalization do not meet these requirements.

We are therefore closing this PR. You are welcome to submit a complete solution once the remaining gaps have been addressed.