Newbie question: error: unknown package 'data'

Stream: lean4

[Kai Middleton]

I have infinitude_of_primes.lean which I got from https://gist.github.com/ujjwal-9/36967b848bd1fa8c21b6e20b35a680b9

Is my setup wrong? Is the code wrong?

When I try to run it I get errors:

$ lean infinititude_of_primes.lean
infinititude_of_primes.lean:4:0: error: unknown package 'data'
infinititude_of_primes.lean:10:5: error: unknown namespace 'nat'
infinititude_of_primes.lean:14:35: error: expected token
infinititude_of_primes.lean:38:2: error: invalid 'end', insufficient scopes
infinititude_of_primes.lean:38:5: error: unexpected token ','; expected command
infinititude_of_primes.lean:60:3: error: invalid 'end', insufficient scopes
infinititude_of_primes.lean:60:6: error: unexpected token ','; expected command
infinititude_of_primes.lean:69:0: error: invalid 'end', insufficient scopes

Here's how I installed lean:

brew install elan mathlibtools
elan toolchain install stable
elan default stable

the version:

lean --version
Lean (version 4.2.0, commit 0d7051497ea0, Release)

Here is the source code:

-- https://mathcs.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html

-- Definitions about natural numbers and primes
import data.nat.prime

-- Library on linear arithmatic
import tactic.linarith

-- Define namespace, which is natural numbers in this case
open nat


-- Define theorem or goal to prove
theorem infinitude_of_primes: ∀ N, ∃ p >= N, prime p :=
-- between begin-end block we write tactics
begin
  -- define N to be a natural number as a part of our local hypothesis
  intro N,

  -- Continue with proof as mentioned in link provided in header
  -- let M to be N! + 1
  let M := factorial N + 1,

  -- let p be smallest prime factor of M which is not 1
  let p := min_fac M,


  -- define supporting hypothesis pp, p is prime
  have pp : prime p :=
  -- begin proof for supporting p being prime
  begin
    -- minimum factor of a number is prime, but what about if M = 1
    refine min_fac_prime _,
    -- so here we prove M != 1 or M > 1
    have : factorial N > 0 := factorial_pos N,
    -- this just automatically takes care of linear arithmatic required for proof
    linarith,
  end,

  -- before this we had existenial statement but now we have condition in p
  use p,

  -- split our goal in  2 subgoals
  split,

  -- proof by contradiction so it should output False
  {by_contradiction,

   /- hypothesis h1, p divides N! + 1 proved by
   min_fac_dvd : ∀ (n : ℕ), n.min_fac ∣ n
   -/
   have h₁ : p ∣ factorial N + 1 := min_fac_dvd M,

   -- hypothesis h2, p divides N!
   have h₂ : p ∣  factorial N :=
   begin
     refine pp.dvd_factorial.mpr _,
     -- proved p <= N, using hypothsis h
     exact le_of_not_ge h,
   end,
   /-
   proved using dvd_add_right with support from local hypothesis h₂ and h₁
   -/
   have h : p ∣ 1 := (nat.dvd_add_right h₂).mp h₁,
   -- prime not dividing one using local hypothesis pp and h
   exact prime.not_dvd_one pp h, },
   -- second part of proof is just our hypothesis pp that we already proved
  {exact pp, },
end

[Mauricio Collares]

The example you found is Lean 3, which is incompatible with Lean 4. This proof of the infinitude of primes in Lean 4 is not as readable but it might help you adapt the above proof to the current version of Lean: https://github.com/leanprover-community/mathlib4/blob/632ea7781942607e95dabee9f4d1335392d0f01a/Mathlib/Data/Nat/Prime.lean#L472-L481

[Mauricio Collares]

Other people probably have readable Lean 4 versions of this proof, let's wait a bit to see if someone has a useful link

[Julian Berman]

Someone indeed may come along with such a link, but just in case, @Kai Middleton here's a completely mechanical "port" of that proof to lean 4:

-- https://mathcs.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html

-- Definitions about natural numbers and primes
import Mathlib.Data.Nat.Prime

-- Mathlib's tactics library
import Mathlib.Tactic

-- We want to refer to some theorems about Natural numbers
open Nat


-- Define theorem or goal to prove
theorem infinitude_of_primes: ∀ N : ℕ, ∃ p ≥ N, Nat.Prime p := by
  -- After `by` we write our "tactics" to prove the theorem...

  -- let N be a natural number
  intro N

  -- Continue with proof as mentioned in link provided in header
  -- let M be N! + 1
  let M := factorial N + 1

  -- let p be smallest prime factor of M which is not 1
  let p := M.minFac


  -- define supporting hypothesis pp, p is prime
  have pp : Nat.Prime p := by
  -- begin proof for supporting p being prime
    -- minimum factor of a number is prime, but what about if M = 1
    apply minFac_prime
    -- so here we prove M != 1 or M > 1
    have : factorial N > 0 := factorial_pos N
    -- this just automatically takes care of linear arithmatic required for proof
    linarith

  -- before this we had existenial statement but now we have condition in p
  use p

  -- split our goal in  2 subgoals
  constructor

  -- proof by contradiction so it should output False
  · by_contra h
    /- hypothesis h1, p divides N! + 1 proved by
    min_fac_dvd : ∀ (n : ℕ), n.min_fac ∣ n
    -/
    have h₁ : p ∣ factorial N + 1 := minFac_dvd M

    -- hypothesis h2, p divides N!
    have h₂ : p ∣  factorial N := by
      apply pp.dvd_factorial.mpr _
      -- proved p <= N, using hypothsis h
      exact le_of_not_ge h
    /-
    proved using dvd_add_right with support from local hypothesis h₂ and h₁
    -/
    have h : p ∣ 1 := (Nat.dvd_add_right h₂).mp h₁
   -- prime not dividing one using local hypothesis pp and h
    exact Nat.Prime.not_dvd_one pp h
   -- second part of proof is just our hypothesis pp that we already proved
  · exact pp

[Julian Berman]

(Minor mostly irrelevant note: There's some minor annoyance in that even though one has open Nat you still get Lean complaining that Nat.Prime conflicts with _root_.Prime I think there's some plan to unify those eventually? Maybe someone will teach both of us if there's some other way to not have to write Nat.Prime)

[Julian Berman]

I guess I could have put that in namespace Nat and probably that would work.

[Scott Morrison]

I think we should namespace _root_.Prime. That's pretty bold to assume that no one will ever want to have a declaration called Prime in any other package...

[Kai Middleton]

Julian Berman said:

Someone indeed may come along with such a link, but just in case, Kai Middleton here's a completely mechanical "port" of that proof to lean 4:

-- https://mathcs.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html

-- Definitions about natural numbers and primes
import Mathlib.Data.Nat.Prime

-- Mathlib's tactics library
import Mathlib.Tactic

-- We want to refer to some theorems about Natural numbers
open Nat


-- Define theorem or goal to prove
theorem infinitude_of_primes: ∀ N : ℕ, ∃ p ≥ N, Nat.Prime p := by
  -- After `by` we write our "tactics" to prove the theorem...

  -- let N be a natural number
  intro N

  -- Continue with proof as mentioned in link provided in header
  -- let M be N! + 1
  let M := factorial N + 1

  -- let p be smallest prime factor of M which is not 1
  let p := M.minFac


  -- define supporting hypothesis pp, p is prime
  have pp : Nat.Prime p := by
  -- begin proof for supporting p being prime
    -- minimum factor of a number is prime, but what about if M = 1
    apply minFac_prime
    -- so here we prove M != 1 or M > 1
    have : factorial N > 0 := factorial_pos N
    -- this just automatically takes care of linear arithmatic required for proof
    linarith

  -- before this we had existenial statement but now we have condition in p
  use p

  -- split our goal in  2 subgoals
  constructor

  -- proof by contradiction so it should output False
  · by_contra h
    /- hypothesis h1, p divides N! + 1 proved by
    min_fac_dvd : ∀ (n : ℕ), n.min_fac ∣ n
    -/
    have h₁ : p ∣ factorial N + 1 := minFac_dvd M

    -- hypothesis h2, p divides N!
    have h₂ : p ∣  factorial N := by
      apply pp.dvd_factorial.mpr _
      -- proved p <= N, using hypothsis h
      exact le_of_not_ge h
    /-
    proved using dvd_add_right with support from local hypothesis h₂ and h₁
    -/
    have h : p ∣ 1 := (Nat.dvd_add_right h₂).mp h₁
   -- prime not dividing one using local hypothesis pp and h
    exact Nat.Prime.not_dvd_one pp h
   -- second part of proof is just our hypothesis pp that we already proved
  · exact pp

Thanks! I tried this mechanical port but am getting some different errors:

$ lean infinititude_of_primes.lean
infinititude_of_primes.lean:4:0: error: unknown package 'Mathlib'
infinititude_of_primes.lean:10:5: error: unknown namespace 'Nat'
infinititude_of_primes.lean:14:39: error: expected token

I did some googling; one hint was to set up LEAN_PATH? But I'm not finding any real documentation to discuss that in greater depth.

I like this idea of a standalone proof of the infinitude of primes as it should be a nice self contained demo of Lean capabilities on an easy but not completely trivial proof.

[Mario Carneiro]

the normal way to invoke lean is via lake, in the context of a project

[Mario Carneiro]

See https://lean-lang.org/lean4/doc/setup.html#lake or https://leanprover-community.github.io/install/project.html#creating-a-lean-project

[Kai Middleton]

Mario Carneiro said:

See https://lean-lang.org/lean4/doc/setup.html#lake or https://leanprover-community.github.io/install/project.html#creating-a-lean-project

Ok thanks, I didn't know I couldn't just do a one-off, will give that a try.

[Mario Carneiro]

you can, but only for files that don't import anything

[Mario Carneiro]

if you want to import Mathlib you need to make a project depending on mathlib via lake new myproj math