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

Reference: erdosproblems.com/200

Imports (1)
Imported by 1 file
  1. def Erdos200.longestPrimeArithmeticProgressions The length of the longest arithmetic progression of primes in $\{1,\ldots,n\}$ line 35 source

    Source documentation

    The length of the longest arithmetic progression of primes in $\{1,\ldots,n\}$.

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

    Statement uses: Nat

    Proof uses: SupSet.sSup, Set.ofPred, Erdos200.longestPrimeArithmeticProgressions.match_1, Exists, Set, And, LE.le, Set.Icc, OfNat.ofNat, Set.IsAPOfLength, ENat, Membership.mem, Nat.Prime

    8 instances, coercions and auxiliary constants left out.

    noncomputable def longestPrimeArithmeticProgressions (n : ℕ) : ℕ :=
…
  2. theorem Erdos200.erdos_200 Does the longest arithmetic progression of primes in $\{1,\ldots,N\}$ have length $o(\log N)$? sorry line 42 source

    Source documentation

    Does the longest arithmetic progression of primes in $\{1,\ldots,N\}$ have length $o(\log N)$?

    depends on sorry what this means

    Statement uses: Iff, True, Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Erdos200.longestPrimeArithmeticProgressions, Real.log

    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_200 : answer(sorry) ↔
    (fun n => (longestPrimeArithmeticProgressions n : ℝ)) =o[atTop] (fun n => log n) := by
…

    Mentions: Erdos200.longestPrimeArithmeticProgressions

  3. theorem Erdos200.erdos_200.variants.upper It follows from the prime number theorem that such a progression has length $\leq(1+o(1))\log N$ sorry line 50 source

    Source documentation

    It follows from the prime number theorem that such a progression has length $\leq(1+o(1))\log N$.

    depends on sorry what this means

    Statement uses: Exists, Nat, Real, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, LE.le, Erdos200.longestPrimeArithmeticProgressions, HMul.hMul, HAdd.hAdd, Real.log

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

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_200.variants.upper : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
    ∀ n, longestPrimeArithmeticProgressions n ≤ (1 + o n) * log n := by
…

    Mentions: Erdos200.longestPrimeArithmeticProgressions