# Zulip Chat Archive

## 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

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

no

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

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):

Last updated: May 12 2021 at 04:19 UTC