373.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 373

Reference: erdosproblems.com/373

Imports (1)

FormalConjecturesUtil

abbrev Erdos373.S Let S be the set of non-trivial solutions to the equation `n! line 36 source
Source documentation
Let S be the set of non-trivial solutions to the equation n! = a₁! ··· aₖ! such that a₁ ≥ ... ≥ aₖ and n-1 > a₁.

no axioms what this means
Statement uses: Set, Prod, Nat, List
Proof uses: Set.ofPred, Erdos373.S.match_1, And, Eq, Nat.factorial, List.prod, List.map, List.Pairwise, GE.ge, LT.lt, List.headI, HSub.hSub, OfNat.ofNat, Membership.mem
9 instances, coercions and auxiliary constants left out.
```
abbrev S : Set (ℕ × List ℕ) :=
…
```
theorem Erdos373.erdos_373 Show that the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions sorry line 45 source
Source documentation
Show that the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

depends on sorry what this means
Statement uses: Set.Finite, Prod, Nat, List, Erdos373.S
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_373 : S.Finite := by
…
```
theorem Erdos373.erdos_373.variants.of_limit Documented declaration: of_limit sorry line 54 source
Source documentation
Show that if P(n(n+1)) / log n → ∞ where P(m) denotes the largest prime factor of m, then the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

depends on sorry what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Nat.maxPrimeFac, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Real.log, Filter.atTop, Set.Finite, Prod, List, Erdos373.S
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_373.variants.of_limit
    (H : Filter.atTop.Tendsto (fun (n : ℕ) => (n*(n+1)).maxPrimeFac / (n : ℝ).log) Filter.atTop) :
    S.Finite := by
…
```
theorem Erdos373.erdos_373.variants.of_lower_bound Documented declaration: of_lower_bound sorry line 71 source
Source documentation
Show that if P(n(n−1)) > 4 log n for large enough n, where P(m) denotes the largest prime factor of m, then the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, LT.lt, Real, HMul.hMul, OfNat.ofNat, Real.log, Nat.maxPrimeFac, HSub.hSub, Filter.atTop, Set.Finite, Prod, List, Erdos373.S
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_373.variants.of_lower_bound
    (H : ∀ᶠ (n : ℕ) in Filter.atTop, 4*(n : ℝ).log < (n*(n-1 : ℕ)).maxPrimeFac) :
    S.Finite := by
…
```
theorem Erdos373.erdos_373.variants.maximal_solution Hickerson conjectured the largest solution the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is 16!=14!5!2! sorry line 81 source
Source documentation
Hickerson conjectured the largest solution the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is 16!=14!5!2!.

depends on sorry what this means
Statement uses: And, Membership.mem, Prod, Nat, List, Set, Erdos373.S, Prod.mk, OfNat.ofNat, List.cons, List.nil, LE.le, Prod.fst
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_373.variants.maximal_solution :
    (16, [14, 5, 2]) ∈ S ∧ ∀ s ∈ S, s.fst ≤ 16 := by
…
```
Mentions: Erdos373.S
theorem Erdos373.erdos_373.variants.suranyi Surányi was the first to conjecture that the only non-trivial solution to a!b!=n! is 6!7!=10! sorry line 90 source
Source documentation
Surányi was the first to conjecture that the only non-trivial solution to a!b!=n! is 6!7!=10!.

depends on sorry what this means
Statement uses: Eq, Set, Prod, Nat, Set.ofPred, Erdos373.erdos_373.variants.suranyi.match_1, And, Nat.factorial, HMul.hMul, LT.lt, OfNat.ofNat, LE.le, Ne, HAdd.hAdd, Singleton.singleton, Prod.mk
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_373.variants.suranyi :
    {(n, a, b) : ℕ × ℕ × ℕ | n ! = a ! * b ! ∧ 1 < n ∧ 1 < a ∧ 1 < b ∧ b ≤ a ∧ a + 1 ≠ n}
      = {(10, 7, 6)} := by
…
```