Zulip Chat Archive

Stream: new members

Topic: Prime Theorem Help


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 00:20):

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

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 00:24):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Mar 13 2020 at 00:37):

no

view this post on Zulip Debendro Mookerjee (Mar 13 2020 at 00:37):

So then what?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 00:38):

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

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 00:38):

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

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 00:44):

sample exercises


Last updated: May 12 2021 at 04:19 UTC