FormalConjectures/ErdosProblems/1056.lean

GitHub source file

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

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

5 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1056

Reference: erdosproblems.com/1056

Imports (1)
  1. def Erdos1056.AllModProdEqualsOne The proposition that the modular product of a collection of consecutive interval equals line 35 source

    Source documentation

    The proposition that the modular product of a collection of consecutive interval equals $1$ modulo $p$, where intervals are defined by a function specifying the consecutive boundaries.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat

    Proof uses: Nat.ModEq, Finset.prod, Finset.Ico, Fin.castSucc

    12 instances, coercions and auxiliary constants left out.

    def AllModProdEqualsOne (p : ℕ) {k : ℕ} (boundaries : Fin (k + 1) → ℕ) : Prop :=
…
  2. theorem Erdos1056.erdos_1056 Let $k ≥ 2$ sorry line 44 source

    Source documentation

    Let $k ≥ 2$. Does there exist a prime $p$ and consecutive intervals $I_0,\dots,I_k$ such that $\prod\limits_{n{\in}I_i}n \equiv 1 \mod n$ for all $1 \le i \le k$?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, Nat.Prime, Fin, HAdd.hAdd, StrictMono, Erdos1056.AllModProdEqualsOne

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_1056 : answer(sorry) ↔
    ∀ k ≥ 2, ∃ (p : ℕ) (_ : p.Prime) (boundaries : Fin (k + 1) → ℕ) (_ : StrictMono boundaries),
    AllModProdEqualsOne p boundaries := by
…

    Mentions: Erdos1056.AllModProdEqualsOne

  3. theorem Erdos1056.erdos_1056.variants.k2 This is problem A15 in Guy's collection [Gu04], where he reports that in a letter in 1979 Erdős observed that $3 * 4 \equiv 5 * 6 * 7 \equiv 1 \mod 11$ line 54 source

    Source documentation

    This is problem A15 in Guy's collection [Gu04], where he reports that in a letter in 1979 Erdős observed that $3 * 4 \equiv 5 * 6 * 7 \equiv 1 \mod 11$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Erdos1056.AllModProdEqualsOne, OfNat.ofNat, Nat, Nat.succ, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: id, of_decide_eq_true, Fin, Nat.ModEq, Finset.prod, Finset.Ico, Fin.castSucc, HAdd.hAdd, Eq, Bool, Decidable.decide, Bool.true, Eq.refl

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_1056.variants.k2 :
    AllModProdEqualsOne 11 ![3, 5, 8] := by
…

    Mentions: Erdos1056.AllModProdEqualsOne

  4. theorem Erdos1056.erdos_1056.variants.k3 Makowski [Ma83] found, for $k=3$: $2 * 3 * 4 * 5 \equiv 6 * 7 * 8 * 9 * 10 * 11 \equiv 12 * 13 * 14 * 15 \equiv 1 \mod 17$ line 64 source

    Source documentation

    Makowski [Ma83] found, for $k=3$: $2 * 3 * 4 * 5 \equiv 6 * 7 * 8 * 9 * 10 * 11 \equiv 12 * 13 * 14 * 15 \equiv 1 \mod 17$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Erdos1056.AllModProdEqualsOne, OfNat.ofNat, Nat, Nat.succ, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: id, of_decide_eq_true, Fin, Nat.ModEq, Finset.prod, Finset.Ico, Fin.castSucc, HAdd.hAdd, Eq, Bool, Decidable.decide, Bool.true, Eq.refl

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_1056.variants.k3 :
    AllModProdEqualsOne 17 ![2, 6, 12, 16] := by
…

    Mentions: Erdos1056.AllModProdEqualsOne

  5. theorem Erdos1056.erdos_1056.variants.noll_simmons Noll and Simmons asked, more generally, whether there are solutions to $q_1! \equiv \dots \equiv q_k! \mod p$ for arbitrarily large $k$ (with $q_1 < \dots < q_k$) sorry line 74 source

    Source documentation

    Noll and Simmons asked, more generally, whether there are solutions to $q_1! \equiv \dots \equiv q_k! \mod p$ for arbitrarily large $k$ (with $q_1 < \dots < q_k$).

    depends on sorry what this means

    Statement uses: Iff, True, Filter.Eventually, Nat, Exists, Nat.Prime, Fin, StrictMono, LT.lt, Nat.ModEq, Nat.factorial, Filter.atTop

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_1056.variants.noll_simmons :
    answer(sorry) ↔ ∀ᶠ k in Filter.atTop,
    ∃ (p : ℕ) (_ : p.Prime) (Q : Fin k → ℕ) (_ : StrictMono Q) (_ : ∀ i, Q i < p),
    ∀ i j : Fin k, (Q i)! ≡ (Q j)! [MOD p] := by
…