Learning the basics of Lean

Stream: new members

[Riley Riles]

Hi! I'm new to Lean and am trying to learn the basics. I'm currently trying to prove that 2*n^2 = m^2 where n, m are integers is a contradiction. As an informal proof I would use induction, but I don't see a way to use the induction tactic here. Any suggestions for how to approach this?

[Yakov Pechersky]

First thing would be to try to even write the statement of the problem. Do you have an example of how you'd formalize the statement?

[Aaron Liu]

First you have to get an idea of what you mean by induction. There are two indices, so there are lots of ways to do induction. You can do strong, two-step, or cauchy induction on the first, second, or both indices at once. What kind of induction do you want?

[Julian Berman]

First you have to choose which of the two first things you want to do first!

[Riley Riles]

\forall n m : Int, \not (2*n^2 = m^2)

``` is how I formalized it. The issue is that just doing induction on n or m would induct on the successor function, which is not particularly helpful here. What I want to do is induct on the degree of powers of two that divide n or m, but I can't figure out a way to do this without having an inductive constructor that depends on prime factorization, which would be a nightmare to implement.

[Notification Bot]

This topic was moved here from #maths > Learning the basics of Lean by Frédéric Dupuis.

[Chris Wong]

docs#Nat.binaryRec might be helpful.

[Chris Wong]

That induction principle works by repeatedly halving the argument.

[Bolton Bailey]

\forall n m : Int, \not (2*n^2 = m^2)

You might have some trouble trying to formalize this version: What happens if both m and n are zero?

[Yakov Pechersky]

Okay but it's not true as stated. n = 0, m = 0 is a solution. So you could reduce your (corrected) statement to one over the positive naturals. Then using your assumption, you could show that m > n, then express m as n + k + 1, removing one free variable.

That being said, we also have docs#Nat.recOnPrimePow or you can use the binaryRec, or argue from a parity point of view

[suhr]

Here's a generalized statement of your exercise with some lemmas that could be used to prove it:

import Mathlib

#check padicValNat
#check padicValNat.mul
#check padicValNat.prime_pow

#check Nat.prime_def

theorem sq_ne_prime_sq {n k p: Nat}[pp: Fact p.Prime](pn: 0 < n)(pk: 0 < k)
    (h: n*n = p*(k*k)): False :=
  sorry

You don't need induction to prove this.

[Kevin Buzzard]

You don't need induction if you use p-adic valuations but in some sense they're defined using induction. In some sense you can't prove anything about the naturals beyond statements like 2+2=4 without induction

[suhr]

True, but that particular proof does not require explicit induction. It is also a rather nice proof, p-adic valuation makes things more elegant.

[Kevin Buzzard]

I agree that p-adic valuations make the proof look very elegant. All I'm saying is that they are hiding a huge amount of stuff behind the API. For example $v_p(ab)=v_p(a)+v_p(b)$ (necessary for the even/odd part of the argument in the contradiction) is assuming uniqueness of prime factorization which is far deeper than irrationality of sqrt(2).

[suhr]

I think one could prove this using just the Euclid's lemma, which in turn only requires the Bezout's identity. So it does not have to be this big under the API. I agree that it's a boring corollary of much cooler results though.

[Kevin Buzzard]

Yes, it only requires all the key ingredients for uniqueness of prime factorization.

[Riley Riles]

Wow, I didn't know p-adic valuations were in Lean! Thanks so much, I'll use this :)