## Stream: new members

### Topic: Prime Theorem Help

#### Debendro Mookerjee (Mar 12 2020 at 23:27):

Here is the theorem I am trying to prove:
Let n > 1. If n has no positive prime factor less than or equal to sqrt(n), then n is prime.

Here is a proof from Hungerford's Abstract Algebra:
Suppose n has the given property but assume that n is not prime. Then n has at least two positive prime factors, say p1 and p2, so that n = p1p2k for some positive integer k. By hypothesis, n has no positive prime divisors less than or equal to sqrt(n). Hence p1 > sqrt(n) and p2 > sqrt(n). Hence n = p1p2k >= p1*p2 >n. Contradiction.

I am new to lean, so I am trying to translate proofs in textbooks for practice. Can anyone please tell me how to translate this proof into Lean code?

#### Kevin Buzzard (Mar 12 2020 at 23:54):

Here's the statement:

import data.nat.prime

open nat

example (n : ℕ) (hn : n > 1) (hp : ∀ p : ℕ, prime p ∧ p ∣ n → p > sqrt n) : prime n :=
begin
sorry
end


It's time for bed in London though, so you'll have to look through data.nat.prime for hints.

#### Debendro Mookerjee (Mar 13 2020 at 00:20):

Should I use an absurd statement for contradiction? If not then what?

#### Andrew Ashworth (Mar 13 2020 at 00:23):

Sure, why not? You'd prove X and not X and then use absurd. It's defined in core lean as def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b

#### Andrew Ashworth (Mar 13 2020 at 00:24):

The end result is: from contradictory hypotheses you can summon a proof of anything you want

#### Debendro Mookerjee (Mar 13 2020 at 00:28):

Can you give an example of how an absurd statement works in lean (I see how it works logically)

#### Reid Barton (Mar 13 2020 at 00:31):

In tactic mode, exact absurd h1 h2 where h1 is a proof of some proposition a and h2 is a proof of not a

#### Andrew Ashworth (Mar 13 2020 at 00:34):

axiom up_is_down : Prop

example : 1 = 2 → up_is_down :=
λ h,
have h_not : 1 ≠ 2 := dec_trivial,
absurd h h_not


#### Debendro Mookerjee (Mar 13 2020 at 00:35):

So based on the theorem statement of Kevin Buzzard and Hungerford's proof, should I be writing:
exact absurd (not prime) hp ? for my first line of code

no

So then what?

#### Kevin Buzzard (Mar 13 2020 at 00:37):

If you cannot do basic logic then trying to prove this theorem is biting off far more than you can chew.

#### Andrew Ashworth (Mar 13 2020 at 00:38):

You should start with some Lean tutorial, like the natural number game, or reading Theorem Proving in Lean

#### Kevin Buzzard (Mar 13 2020 at 00:38):

Why not try and prove stuff like p ∧ q → q ∧ p or p → ¬ ¬ p first?

#### Kevin Buzzard (Mar 13 2020 at 00:38):

You need to be able to steer basic logic before you can start doing arithmetic

#### Kevin Buzzard (Mar 13 2020 at 00:44):

sample exercises

Last updated: May 12 2021 at 04:19 UTC