Zulip Chat Archive

Stream: new members

Topic: Proving n^2 not equal 2


view this post on Zulip Yuhan Du (Aug 31 2018 at 16:01):

I am trying to prove the statement that n22n^2 \neq 2

import algebra.group_power
theorem what_i_need: ¬ ( n :  , n ^ 2 = 2 ) := sorry

Could someone possibly help me?

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 16:08):

Yesterday there was some chat about proving integer squares were 0 or 1 or 4 mod 8. It just occurs to me that an analogous approach mod 4 would do this (or mod 3)

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 16:08):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/0.3C.3Dd.3C3.20implies.20d.3D0.2C1.2C2

view this post on Zulip Patrick Massot (Aug 31 2018 at 16:09):

have you looked at https://github.com/leanprover/mathlib/blob/master/data/nat/prime.lean?

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:36):

Well, this is quite a bit easier than proving that sqrt 2 is irrational

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:36):

You can do it by cases on n.nat_abs

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:37):

too small when it is 0 or 1, too big when it is >= 2

view this post on Zulip Chris Hughes (Aug 31 2018 at 16:37):

This is one method.

import data.zmod

example : ¬  n : , n ^ 2 = 2 :=
λ n, hn, have h :  n : zmod 3, n ^ 2  (2 : ), from dec_trivial,
by have := h n; rw  hn at this; simpa

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 16:38):

The congruence trick is somehow better -- if a positive integer is not a square then it's not a square mod p for infinitely many p, and so you can just work in zmod p for the smallest such p :-)

view this post on Zulip Chris Hughes (Aug 31 2018 at 16:38):

It's also not very easy to come up with.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:38):

Even easier, you can square the square root and see if it matches

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:39):

that should make it an easy dec_trivial proof

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 16:40):

Oh that's a good idea -- prove that n is a square iff (sqrt n)^2=n

view this post on Zulip Chris Hughes (Aug 31 2018 at 16:53):

Not quite sure why this doesn't work

instance h (m : ) : decidable ( n : , n ^ 2 = m) :=
decidable_of_iff (0  m  m.nat_abs.sqrt ^ 2 = m.nat_abs)
⟨λ h, nat.sqrt m.nat_abs, by rw [ int.coe_nat_pow, h.2, int.nat_abs_of_nonneg h.1],
 λ s, hs, hs  (pow_two_nonneg _), by rw [ hs, pow_two, int.nat_abs_mul, nat.sqrt_eq, nat.pow_two]⟩⟩

#eval (¬  n : , n ^ 2 = 2 : bool)

lemma two_not_square : ¬  n : , n ^ 2 = 2 := dec_trivial

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:54):

nat.sqrt is defined through well founded recursion, which may cause a problem on all but the simplest problems. A similar issue came up with nat.prime

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:55):

I assume the #eval worked

view this post on Zulip Chris Hughes (Aug 31 2018 at 16:55):

The eval did work. So the issue is that it's just too slow?

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:56):

I think it won't reduce well founded proofs because it requires evaluating theorems

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:56):

you can probably get #reduce to do it but that's not so helpful

view this post on Zulip Mario Carneiro (Aug 31 2018 at 16:57):

We need another norm_num extension for this

view this post on Zulip Chris Hughes (Aug 31 2018 at 17:00):

Why can I prove example : nat.gcd 4 5 = 1 := rfl? That uses well founded recursion I take it.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 17:05):

I think it is just a complexity problem. The #reduce times out for the sqrt example but not gcd

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:43):

This thread is really depressing. Sometimes I feel like we are going somewhere (like when we make progress on topological groups or noetherian modules) but then some super elementary problem is raised and we abruptly come back to reality: trivial things are not trivial at all in Lean.

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 09:56):

The proof that there's no integer whose square is 2 is "it doesn't work for small n, and big n are too big". Formalising this is a bore. Automating it is possible, but it hasn't been done yet. That's not depressing, it just means things need to be done. Chris made an attempt. In 1 year's time there might be 10 Chris's at Imperial (here's hoping).

view this post on Zulip Ali Sever (Sep 01 2018 at 12:09):

I aspire to be a Chris one day

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 12:17):

That would be great Ali :-) come along on Thursday evenings in Oct and help me deal with the inevitable pile of freshers!

view this post on Zulip Kenny Lau (Sep 01 2018 at 13:18):

import data.nat.basic algebra.group_power

instance nat.decidable_bex_lt (n : nat) (P : Π k < n, Prop) :
   [H :  n h, decidable (P n h)], decidable ( k h, P k h) :=
begin
  induction n with n IH; intro; resetI,
  { exact is_false (λ ⟨_, h, _⟩, nat.not_lt_zero _ h) },
  cases IH (λ k h, P k (nat.lt_succ_of_lt h)) with h,
  { by_cases p : P n (nat.lt_succ_self n),
    { exact is_true n, nat.lt_succ_self n, p },
    { apply is_false,
      intro hk,
      rcases hk with k, hk1, hk2,
      cases nat.lt_succ_iff_lt_or_eq.1 hk1 with hk hk,
      { exact h k, hk, hk2 },
      { subst hk, exact p hk2 } } },
  apply is_true,
  rcases h with k, hk1, hk2,
  exact k, nat.lt_succ_of_lt hk1, hk2
end

instance nat.decidable_bex_le (n : nat) (P : Π k  n, Prop)
  [Π n h, decidable (P n h)] : decidable ( k h, P k h) :=
decidable_of_iff ( k < n + 1, P k (nat.le_of_lt_succ H))
⟨λ k, h1, h2, k, nat.le_of_lt_succ h1, h2,
λ k, h1, h2, k, nat.lt_succ_of_le h1, h2⟩⟩

instance decidable_mul_self_nat (n : ) : decidable ( k, k * k = n) :=
decidable_of_iff ( k  n, k * k = n)
⟨λ k, h1, h2, k, h2, λ k, h1, k, h1  nat.le_mul_self k, h1⟩⟩

instance decidable_sqr_nat (n : ) : decidable ( k, k^2 = n) :=
decidable_of_iff ( k, k * k = n)
⟨λ k, h, k, by rwa [nat.pow_two], λ k, h, k, by rwa [nat.pow_two] at h⟩⟩

instance decidable_mul_self_int : Π (n : ), decidable ( k, k * k = n)
| (int.of_nat n) := decidable_of_iff ( k, k * k = n)
    ⟨λ k, hk, k, by rw [ int.coe_nat_mul, hk]; refl,
    λ k, hk, int.nat_abs k, by rw [ int.nat_abs_mul, hk]; refl⟩⟩
| -[1+ n] := is_false $ λ k, h1, not_lt_of_ge (mul_self_nonneg k) $
    h1.symm  int.neg_succ_of_nat_lt_zero n

instance decidable_sqr_int (n : ) : decidable ( k, k^2 = n) :=
decidable_of_iff ( k, k * k = n)
⟨λ k, h, k, by rwa [pow_two], λ k, h, k, by rwa [pow_two] at h⟩⟩

theorem what_i_need: ¬ ( n :  , n ^ 2 = 2 ) := dec_trivial

view this post on Zulip Kenny Lau (Sep 01 2018 at 13:18):

btw the first part of my code is from this discussion four months ago

view this post on Zulip Kenny Lau (Sep 01 2018 at 13:19):

(and mathlib still doesn't know it's true :P)

view this post on Zulip Kenny Lau (Sep 01 2018 at 13:20):

This thread is really depressing. Sometimes I feel like we are going somewhere (like when we make progress on topological groups or noetherian modules) but then some super elementary problem is raised and we abruptly come back to reality: trivial things are not trivial at all in Lean.

@Patrick Massot Well this is just a puzzle that cannot be generalized to more useful maths...

view this post on Zulip Mario Carneiro (Sep 01 2018 at 13:35):

Yes, of course this is the other option - to check n is a square, just look at all the squares and see if n is in the list. It is much slower than squaring the square root, but it works better in small cases in the kernel since there are no wf definitions involved

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:05):

Kenny, why don't you PR the general stuff above? That could be useful in lots of small annoying situations

view this post on Zulip Bryan Gin-ge Chen (Sep 01 2018 at 14:06):

Following Patrick Massot's suggestion to look at data.nat.prime, I started trying to prove it using nat.not_prime_mulbut I got stuck.

import algebra.group_power data.nat.prime

theorem what_i_need: ¬ ( n :  , n ^ 2 = 2 ) :=
have p2: nat.prime 2, from nat.prime_two,
begin
unfold pow, unfold monoid.pow,
intro h,
exact exists.elim h (assume n,
begin
clear h,
rw [mul_one],
assume h1,
_
--have pnn : nat.prime (n*n), by sorry,
--exact false.elim ((nat.not_prime_mul (sorry) (sorry)) h1)
end
)
end

I think the main thing I'm missing how to do is showing that proving it for 1<nN1<n \in \mathbb{N} suffices to show it for all nZn\in\mathbb{Z}.

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:09):

In this direction, I suggest proving ¬ nat.prime (n*n). It has no assumptions, but you have to special case 0 and 1

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:09):

yes, this is what I had in mind

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:10):

I hoped that proving that from prime.lean wouldn't be too hard

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:10):

I thought it was a theorem already but I could be mistaken

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:10):

there is not_prime_mul which takes care of the large n case

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:17):

Even without trying to go to the heart of the matter, natural number hell strikes:

import algebra.group_power data.nat.prime

lemma aux (n : ) : ¬ nat.prime (n*n) :=
sorry

theorem what_i_need: ¬ ( n :  , n ^ 2 = 2 ) :=
begin
  rintro n, h,
  apply aux n,
  rw pow_two,
  rw h,
  exact nat.prime_two,
end

The rw h doesn't work. simp [h] does work, but these kind of things is really the worse of Lean

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:17):

And I'm not even talking about trying to deduce the result with integers instead of natural numbers

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:22):

you have to use rw ← nat.pow_two

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:30):

I'm sure there is a solution, but having to know all that is really painful

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:33):

most of this "ambient knowledge" is encoded in the simp lemmas, which is why simp [h] worked. If you look at the rewrites used you will see normalization of the group_power instance on nat to nat.pow

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:34):

the problem is that nat has two power notations, one elementary from nat.pow and another from the group power instance

view this post on Zulip Mario Carneiro (Sep 01 2018 at 14:34):

nat.pow is the canonical one, at least until it is removed (it's in core)

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:40):

@Bryan Gin-ge Chen

import algebra.group_power data.nat.prime

open nat

lemma aux (n : ) : ¬ nat.prime (n*n) :=
begin
  intro h,
  cases n,
  { simpa [not_prime_zero] using h },
  { cases n,
    { simpa [not_prime_one] using h },
    { have : succ (succ n) > 1 := dec_trivial,
      exact not_prime_mul this this h } }
end

theorem what_i_need: ¬ ( n :  , n ^ 2 = 2 ) :=
begin
  rintro n, h,
  apply aux n,
  rw [nat.pow_two, h],
  exact nat.prime_two,
end

view this post on Zulip Patrick Massot (Sep 01 2018 at 14:41):

This is still cheating because there is nothing about negative integers

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2018 at 03:07):

A few days late and not very pretty, but I managed to complete your proof @Patrick Massot

import algebra.group_power data.nat.prime

open nat

lemma aux (n : ) : ¬ prime (n*n) :=
begin
  intro h,
  cases n,
  { simpa [not_prime_zero] using h },
  { cases n,
    { simpa [not_prime_one] using h },
    { have : succ (succ n) > 1 := dec_trivial,
      exact not_prime_mul this this h } }
end

theorem what_i_need_N: ¬ ( n :  , n ^ 2 = 2 ) :=
begin
  rintro n, h,
  apply aux n,
  rw [nat.pow_two, h],
  exact prime_two,
end

open int

lemma sq_eq_nat_abs_sq {n : } {m : } : n^2 = (nat_abs n^2) :=
by rw [_root_.pow_two, _root_.pow_two,
 int.coe_nat_mul, nat_abs_mul_self]

lemma nat_sq_of_int_sq {n : } {m : } : n^2 = m  ( nn : , nn ^ 2 = m) :=
begin
  intro h,
  existsi (nat_abs n),
    apply int.coe_nat_inj,
    rw [nat.pow_two, int.coe_nat_mul,  _root_.pow_two,
     sq_eq_nat_abs_sq],
  exact h,
  exact m
end

theorem what_i_need : ¬ ( n : , n^2 = 2) :=
begin
  rintro n,h,
  exact false.elim (what_i_need_N (nat_sq_of_int_sq h))
end

I think I learned a few things along the way, though it still feels like I've got a long way to go before I can do anything useful...

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 06:50):

of course anyone reading this thread and seeing several very long proofs that 2 isn't a square might argue that we all have a long way to go before we can do anything useful...


Last updated: May 13 2021 at 22:15 UTC