FormalConjectures/ErdosProblems/379.lean

GitHub source file

2 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 379

Reference: erdosproblems.com/379

Imports (1)
  1. def Erdos379.S line 32 source

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

    Statement uses: Nat

    Proof uses: SupSet.sSup, Set.ofPred, Membership.mem, Finset, Finset.Ico, OfNat.ofNat, Exists, And, Nat.Prime, Dvd.dvd, HPow.hPow, Nat.choose

    11 instances, coercions and auxiliary constants left out.

  2. theorem Erdos379.erdos_379 sorry line 45 source

    depends on sorry what this means

    Statement uses: Eq, ENat, Filter.limsup, Nat, Erdos379.S, Filter.atTop, Top.top

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

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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