Prime Theorem Help

Stream: new members

[Debendro Mookerjee]

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]

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]

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

[Andrew Ashworth]

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]

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

[Debendro Mookerjee]

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

[Reid Barton]

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]

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]

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

[Andrew Ashworth]

no

[Debendro Mookerjee]

So then what?

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

sample exercises