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

2 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 389

Reference: erdosproblems.com/389

Imports (1)

FormalConjecturesUtil

theorem Erdos389.erdos_389 Is it true that for every $n \geq 1$ there is a $k$ such that $$ n(n + 1) \cdots (n + k - 1) \mid (n + k) \cdots (n + 2k - 1)? $$ sorry line 37 source
Source documentation
Is it true that for every $n \geq 1$ there is a $k$ such that $$ n(n + 1) \cdots (n + k - 1) \mid (n + k) \cdots (n + 2k - 1)? $$

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, And, Dvd.dvd, Finset.prod, Finset.range, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_389 : answer(sorry) ↔
    ∀ n ≥ 1, ∃ k ≥ 1, ∏ i ∈ Finset.range k, (n + i) ∣ ∏ i ∈ Finset.range k, (n + k + i) := by
…
```
theorem Erdos389.erdos_389.variants.mehta_four Bhavik Mehta has computed the minimal such $k$ for $1 \leq n \leq 18$ line 46 source
Source documentation
Bhavik Mehta has computed the minimal such $k$ for $1 \leq n \leq 18$. For example, the minimal $k$ for $n = 4$ is $207$.

extra axioms: _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_1, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_10, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_100, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_101, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_102, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_103, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_104, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_105, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_106, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_107, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_108, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_109, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_11, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_110, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_111, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_112, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_113, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_114, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_115, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_116, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_117, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_118, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_119, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_12, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_120, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_121, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_122, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_123, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_124, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_125, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_126, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_127, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_128, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_129, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_13, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_130, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_131, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_132, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_133, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_134, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_135, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_136, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_137, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_138, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_139, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_14, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_140, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_141, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_142, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_143, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_144, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_145, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_146, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_147, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_148, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_149, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_15, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_150, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_151, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_152, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_153, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_154, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_155, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_156, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_157, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_158, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_159, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_16, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_160, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_161, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_162, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_163, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_164, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_165, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_166, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_167, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_168, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_169, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_17, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_170, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_171, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_172, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_173, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_174, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_175, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_176, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_177, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_178, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_179, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_18, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_180, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_181, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_182, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_183, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_184, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_185, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_186, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_187, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_188, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_189, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_19, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_190, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_191, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_192, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_193, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_194, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_195, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_196, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_197, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_198, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_199, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_2, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_20, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_200, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_201, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_202, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_203, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_204, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_205, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_206, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_207, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_21, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_22, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_23, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_24, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_25, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_26, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_27, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_28, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_29, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_3, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_30, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_31, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_32, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_33, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_34, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_35, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_36, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_37, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_38, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_39, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_4, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_40, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_41, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_42, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_43, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_44, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_45, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_46, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_47, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_48, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_49, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_5, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_50, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_51, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_52, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_53, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_54, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_55, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_56, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_57, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_58, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_59, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_6, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_60, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_61, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_62, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_63, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_64, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_65, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_66, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_67, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_68, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_69, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_7, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_70, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_71, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_72, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_73, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_74, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_75, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_76, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_77, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_78, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_79, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_8, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_80, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_81, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_82, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_83, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_84, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_85, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_86, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_87, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_88, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_89, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_9, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_90, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_91, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_92, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_93, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_94, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_95, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_96, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_97, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_98, _private.0.Erdos389.erdos_389.variants.mehta_four._native.native_decide.ax_99 what this means
Statement uses: IsLeast, Nat, Set.ofPred, And, LE.le, OfNat.ofNat, Dvd.dvd, Finset.prod, Finset.range, HAdd.hAdd
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, of_decide_eq_true, Decidable.byContradiction, Not, dite, False, LT.lt, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast and 3 more
238 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_389.variants.mehta_four :
    IsLeast
      { k | 1 ≤ k ∧ ∏ i ∈ Finset.range k, (4 + i) ∣ ∏ i ∈ Finset.range k, (4 + k + i) }
      207 := by
…
```