## Stream: new members

### Topic: Proving n^2 not equal 2

#### Yuhan Du (Aug 31 2018 at 16:01):

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

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


Could someone possibly help me?

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

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

#### Patrick Massot (Aug 31 2018 at 16:09):

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

#### Mario Carneiro (Aug 31 2018 at 16:36):

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

#### Mario Carneiro (Aug 31 2018 at 16:36):

You can do it by cases on n.nat_abs

#### Mario Carneiro (Aug 31 2018 at 16:37):

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

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


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

#### Chris Hughes (Aug 31 2018 at 16:38):

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

#### Mario Carneiro (Aug 31 2018 at 16:38):

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

#### Mario Carneiro (Aug 31 2018 at 16:39):

that should make it an easy dec_trivial proof

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

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


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

#### Mario Carneiro (Aug 31 2018 at 16:55):

I assume the #eval worked

#### Chris Hughes (Aug 31 2018 at 16:55):

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

#### Mario Carneiro (Aug 31 2018 at 16:56):

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

#### Mario Carneiro (Aug 31 2018 at 16:56):

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

#### Mario Carneiro (Aug 31 2018 at 16:57):

We need another norm_num extension for this

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

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

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

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

#### Ali Sever (Sep 01 2018 at 12:09):

I aspire to be a Chris one day

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

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


#### Kenny Lau (Sep 01 2018 at 13:18):

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

#### Kenny Lau (Sep 01 2018 at 13:19):

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

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

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

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

#### 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 suffices to show it for all $n\in\mathbb{Z}$.

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

#### Patrick Massot (Sep 01 2018 at 14:09):

yes, this is what I had in mind

#### Patrick Massot (Sep 01 2018 at 14:10):

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

#### Mario Carneiro (Sep 01 2018 at 14:10):

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

#### Mario Carneiro (Sep 01 2018 at 14:10):

there is not_prime_mul which takes care of the large n case

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

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

#### Mario Carneiro (Sep 01 2018 at 14:22):

you have to use rw ← nat.pow_two

#### Patrick Massot (Sep 01 2018 at 14:30):

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

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

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

#### Mario Carneiro (Sep 01 2018 at 14:34):

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

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


#### Patrick Massot (Sep 01 2018 at 14:41):

This is still cheating because there is nothing about negative integers

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

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