FormalConjectures/ErdosProblems/913.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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 913

Reference: erdosproblems.com/913

Reviewed by @b-mehta on 2025-05-27

Imports (1)
  1. theorem Erdos913.erdos_913 Are there infinitely many $n$ such that if $$ n(n + 1) = \prod_i p_i^{k_i} $$ is the factorisation into distinct primes then all exponents $k_i$ are distinct? sorry line 40 source

    Source documentation

    Are there infinitely many $n$ such that if $$ n(n + 1) = \prod_i p_i^{k_i} $$ is the factorisation into distinct primes then all exponents $k_i$ are distinct?

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, Set.InjOn, Finsupp, Nat.factorization, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Finset, Nat.primeFactors

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

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_913 : answer(sorry) ↔
    { n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite := by
…
  2. theorem Erdos913.erdos_913.variants.infinite_many_8p_sq_add_one_primes It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime sorry line 48 source

    Source documentation

    It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime.

    depends on sorry what this means

    Statement uses: Set.Infinite, Nat, Set.ofPred, And, Nat.Prime, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow

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

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_913.variants.infinite_many_8p_sq_add_one_primes :
    { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite := by
…
  3. theorem Erdos913.erdos_913.variants.conditional If there are infinitely many primes $p$ such that $8p^2 - 1$ is prime, then this is true line 54 source

    Source documentation

    If there are infinitely many primes $p$ such that $8p^2 - 1$ is prime, then this is true.

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

    Statement uses: Set.Infinite, Nat, Set.ofPred, And, Nat.Prime, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, Set.InjOn, Finsupp, Nat.factorization, HAdd.hAdd, Finset, Nat.primeFactors

    Proof uses: Set, LT.lt, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 145 more

    195 instances, coercions and auxiliary constants left out.

    Tactic trace: 47 steps

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

    theorem erdos_913.variants.conditional (h : { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite) :
    { n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite := by
…