Proof for Infinite Primes

Stream: general

[Daniel Park]

Hello, I need a help for proving my first proposition in Lean 4. I looked over some documentation, but I did not quite fully graspe the entire idea just yet. I am trying to prove that there are infinitely many prime numbers, and my plan to prove this statement is the following:

1. Assume the set of primes $\mathbb{P}$ is finite.
2. Compose a new number by $P = \prod_{p \in \mathbb{P}} p + 1$.
3. If $P$ is a prime, it is a contradiction since $P \notin \mathbb{P}$.
4. If $P$ is a composite, it must be divisible by some prime numbers, but any prime number $p \in \mathbb{P}$ cannot divide $P$.
5. Therefore, there are infinitely many primes.

My first blocker was, I tried to import prime numbers by import data.nat.prime, but it did not work. I couldn't find a way to properly import this, so I decided to define it by myself. This is what I got so far:

def is_prime (n : ℕ) : Prop :=
  n > 1 ∧ ∀ d ∈ ℕ, d | n → d = 1 ∧ d = n

I am having a lot of errors with this such as:

failed to synthesize
  LT ℕ
Additional diagnostic information may be available using the `set_option diagnostics true` comm

failed to synthesize
  OfNat ℕ 1
numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
  ℕ
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

failed to synthesize
  Membership ?m.28 (Type ?u.14)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

unexpected token '|'; expected command

Hopefully, at least I can see that the divisible sign '$|$' did not work in Lean 4 as my expectation. Other than this, I cannot understand what went wrong. Can someone please help me to fix it or let me know how to import prime numbers? Also, where can I find example codes to familiarize myself with the Lean 4 syntax?

Thank you!

[Edward van de Meent]

if you created a project with mathlib, import Mathlib should fix most of these issues.

[Daniel Park]

Edward van de Meent said:

if you created a project with mathlib, import Mathlib should fix most of these issues.

Thank you. It seems my issue is resolved for now. So, even though I created a project with mathlib, do I still have to write import Mathlib on the top?

[Edward van de Meent]

yes. do note that import Mathlib is a very general import, you might want/need to refine to something like import Mathlib.Data.Nat.Basic or something like that in order to reduce compile time.

[Daniel Park]

I see, thank you!

[Ruben Van de Velde]

By the way, your first error was that lean didn't realize that you meant the natural numbers when you wrote ℕ. If you added

set_option autoImplicit false

at the start, you'd get unknown identifier 'ℕ' as the error

[Daniel Park]

Hello, thank you for answering. So, does that mean I have to import natural numbers from Mathlib to use $\mathbb{N}$?

[Edward van de Meent]

you have to import the notation from mathlib. Nat should always be available.

[Daniel Park]

So, can I import notation by import Mathlib.notation? Where can I look up import related documentations?

[Edward van de Meent]

the documentation for this specific notation can be found here, and imported from Mathlib.Data.Nat.Notation

[Edward van de Meent]

it gets imported transitively with import Mathlib, so you don't need to worry about this specific file if you just want it available.

[Daniel Park]

Thanks a lot! Now, I see the meaning behind this.

[Dan Velleman]

Other errors you have:

1. Instead of ∀ d ∈ ℕ, you should have ∀ d : ℕ.
2. I think you used the wrong vertical line character for "divides". There are two vertical line characters that look slightly different: | and ∣. The first is what you typed, but for "divides" you need to use the second one. To type it, type \|.
3. I think you meant d = 1 ∨ d = n, not d = 1 ∧ d = n.

[Daniel Park]

Thank you so much!

[Daniel Park]

Thanks to everyone's help in here, I could define a new proposition about composite numbers, as following:

def composite (n: ℕ) : Prop :=
  n > 1 ∧ ∃ d: ℕ, d ∣ n → d != 1 ∧ d != n

[Kim Morrison]

@Daniel Park, not quite:

import Mathlib

def composite (n: ℕ) : Prop :=
  n > 1 ∧ ∃ d: ℕ, d ∣ n → d != 1 ∧ d != n

theorem composite_seven : composite 7 :=
  ⟨by norm_num, 3, by decide⟩

[Daniel Park]

Hello, @Kim Morrison. Thank you for pointing out. If you don't mind, can you please explain what the theorem composite_seven does from your code?

[Kim Morrison]

My theorem proves that, according to your definition of composite, that 7 is composite.

[Kim Morrison]

It does this by discharging the n > 1 goal via the tactic norm_num, picking 3 as the existential witness d in your statement, and then using decidability to check that 3 ∣ 7 → 3 != 1 ∧ 3 != 7.

[Daniel Park]

Ah, I see. Essentially, is this because the statement by itself true even though it does not satisfy $d | n$?

[Kim Morrison]

It's that a false statement implies anything. You just have your logical connectives wrong here.

[Daniel Park]

Yes. I might have to rethink about how to correctly negate my prime proposition. Thank you.

[Kim Morrison]

Apologies, @Daniel Park, I'm now going to hijack your thread to discuss tooling to help people with problems like this. :-)

[Kim Morrison]

@Henrik Böving, @Eric Wieser, how about this:

import Mathlib
import Plausible

-- This part maybe should be added to the `Plausible` library.
namespace Plausible

def testable_of_iff (a : Prop) (h : a ↔ b) [T : Testable a] : Testable b where
  run cfg m := (TestResult.iff h.symm) <$> T.run cfg m

instance {p q : Prop} [Testable (¬ p)] [Testable ¬ q] : Testable (¬ (p ∧ q)) :=
  testable_of_iff (¬ p ∨ ¬ q) (Classical.not_and_iff_or_not_not.symm)

instance [SampleableExt α] {p : α → Prop} [∀ a, Testable (¬ p a)] : Testable (¬ ∃ a, p a) :=
  testable_of_iff (NamedBinder "existential witness" <| ∀ a, ¬ p a) not_exists.symm

end Plausible

-- Now the example:

def composite (n: ℕ) : Prop :=
  n > 1 ∧ ∃ d: ℕ, d ∣ n → d != 1 ∧ d != n

theorem not_composite_seven : ¬ composite 7 := by
  unfold composite
  plausible -- Prints an error message about finding a counterexample.

[Kim Morrison]

Ideally every time someone comes up with a broken definition like in this thread, we should try to make sure plausible would have helped them.

[Kim Morrison]

The code above doesn't quite get there.

1. I had to add a fake name for the existential binder, but I think we could change docs#Plausible.Decorations.addDecorations to also annotate the binders under \exists.
2. It's a bit sad that we need to unfold composite before plausible can do its magic. Would it be reasonable for plausible to do some unfolding automatically? I'm not seeing a good strategy yet.

[Daniel Park]

Kim Morrison said:

Apologies, Daniel Park, I'm now going to hijack your thread to discuss tooling to help people with problems like this. :-)

Sounds fair. I don't really understand the code written by you after that anyway... :joy:

[Eric Wieser]

For 2, perhaps the answer is "unfold things from the current file"?

[Henrik Böving]

I don't think there really is a need to unfold here? If we had a sufficiently good derivable logic for Testable this should be doable with just deriving Testable for Composite

[Kim Morrison]

I guess dynamic generation of Testable is possible!

[Eric Wieser]

Is deriving Decidable enough here?

[Henrik Böving]

Yes

[Jon Eugster]

on a side note @Daniel Park, last time I wrote down this proof, I found it easier to use "pick the largest prime and then look at p+1 factorial" instead of the product over all primes. Somehow I found the available results in mathlib about factorial more useful.

[Luigi Massacci]

Jon Eugster said:

on a side note Daniel Park, last time I wrote down this proof, I found it easier to use "pick the largest prime and then look at p+1 factorial" instead of the product over all primes. Somehow I found the available results in mathlib about factorial more useful.

I might misremember, but that's the proof that mathlib has, so it wouldn't be surprising that there's a bunch of useful helper lemmas lying around mathlib

[Dan Velleman]

Daniel Park said:

Yes. I might have to rethink about how to correctly negate my prime proposition. Thank you.

¬ (p → q) is equivalent to p ∧ ¬ q (as you can check with a truth table). That may be where you went wrong in negating your definition of prime.

[Dan Velleman]

Jon Eugster said:

on a side note Daniel Park, last time I wrote down this proof, I found it easier to use "pick the largest prime and then look at p+1 factorial" instead of the product over all primes. Somehow I found the available results in mathlib about factorial more useful.

I agree, this would be easier. But did you mean p! + 1?

[Daniel Park]

Dan Velleman said:

Daniel Park said:

Yes. I might have to rethink about how to correctly negate my prime proposition. Thank you.

¬ (p → q) is equivalent to p ∧ ¬ q (as you can check with a truth table). That may be where you went wrong in negating your definition of prime.

Thank you for the reminder. Now, I have this:

def composite (n: ℕ) : Prop :=
  n > 1 ∧ ∃d: ℕ, d ∣ n ∧ (d ≠ 1 ∧ d ≠ n)

[Ruben Van de Velde]

Is 1 composite? :innocent:

[Daniel Park]

Jon Eugster said:

on a side note Daniel Park, last time I wrote down this proof, I found it easier to use "pick the largest prime and then look at p+1 factorial" instead of the product over all primes. Somehow I found the available results in mathlib about factorial more useful.

Hello, thank you for the comment. So, did you do something like:

1. Assume the set of primes $\mathbb{P}$ is finite, and let $P$ be the largest prime number.
2. Pick $P' = P! + 1$.
3. Since we know that $P' > 1$, $P$ must be either prime or composite.
4. If $P'$ is prime, then it contradicts because $P' \notin \mathbb{P}$.
5. If $P'$ is composite, then some prime numbers should be able to divide $P'$, but it is impossible.
6. Therefore, we conclude that there are infinitely many primes.

[Daniel Park]

Ruben Van de Velde said:

Is 1 composite? :innocent:

I put n > 1 in my proposition.