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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 979

Reference: erdosproblems.com/979

Imports (1)
  1. def Erdos979.solutionSet line 30 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Set, Multiset

    Proof uses: Set.ofPred, And, Eq, Multiset.card, Membership.mem, Nat.Prime, Multiset.sum, Multiset.map, HPow.hPow

    6 instances, coercions and auxiliary constants left out.

  2. theorem Erdos979.erdos_979 Let $k ≥ 2$, and let $f_k(n)$ count the number of solutions to $n = p_1^k + \dots + p_k^k$, where the $p_i$ are prime numbers sorry line 38 source

    Source documentation

    Let $k ≥ 2$, and let $f_k(n)$ count the number of solutions to $n = p_1^k + \dots + p_k^k$, where the $p_i$ are prime numbers. Is it true that $\limsup f_k(n) = \infty$?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Eq, ENat, Filter.limsup, Set.encard, Multiset, Erdos979.solutionSet, Filter.atTop, Top.top

    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_979 : answer(sorry) ↔
    ∀ k ≥ 2, Filter.limsup (fun n => (solutionSet n k).encard) Filter.atTop = ⊤ := by
…

    Mentions: Erdos979.solutionSet

  3. theorem Erdos979.erdos_979.variants.k2 Erdős [Er37b] proved that if $f_2(n)$ counts the number of solutions to $n = p_1^2 + p_2^2$, where $p_1$ and $p_2$ are prime numbers, then $\limsup f_2(n) = \infty$ sorry line 48 source

    Source documentation

    Erdős [Er37b] proved that if $f_2(n)$ counts the number of solutions to $n = p_1^2 + p_2^2$, where $p_1$ and $p_2$ are prime numbers, then $\limsup f_2(n) = \infty$.

    [Er37b] Erdős, Paul, On the Sum and Difference of Squares of Primes. J. London Math. Soc. (1937), 133--136.

    depends on sorry what this means

    Statement uses: Eq, ENat, Filter.limsup, Nat, Set.encard, Multiset, Erdos979.solutionSet, OfNat.ofNat, Filter.atTop, Top.top

    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_979.variants.k2 :
    Filter.limsup (fun n => (solutionSet n 2).encard) Filter.atTop = ⊤ := by
…

    Mentions: Erdos979.solutionSet

  4. theorem Erdos979.erdos_979.variants.k3 sorry line 58 source

    depends on sorry what this means

    Statement uses: Eq, ENat, Filter.limsup, Nat, Set.encard, Multiset, Erdos979.solutionSet, OfNat.ofNat, Filter.atTop, Top.top

    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.