Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalising a new proof that the square root of two is irrational

lawrencecpaulson.github.io

Post reply on HN
Print view View original

51–60 of 94 posts

Re: Formalising a new proof that the square root of two is irrational

#51

Post by zeroonetwothree »

gunnihinn wrote: post #13
tromp wrote: post #9

The new proof rephrased: Let K be the set of positive integers k such that k √2 is an integer. Suppose K is non-empty, denote its minimum as k. Consider the positive integer k' = k √2 - k = k (√2 - 1). Then k' < k and k' is also in K since k' √2 = 2 k - k √2, contradicting non-emptyness of K.

As the post points out this involves some claims about infinite sets that are maybe not super obvious to laypeople (every infinite set of natural numbers has a least element). But we can rephrase this to avoid mentioning sets: For any rational number p/q (with q > 0) there exists a smallest positive natural number k such that k * p/q is natural: Clearly q works, so we check the finitely many numbers 1, ..., q and pic…

You don’t have to pick the smallest, just start with q and then find you can keep decreasing it forever.

Re: Formalising a new proof that the square root of two is irrational

#52

Post by janm31415 »

I might be missing something, but as I see it here: by assumption, √2 is rational. Then k(√2-1) √2 is a positive integer.

This does not mean that k(√2 - 1) belongs to K, with K the set of positive integers {n: n√2 ∈ ℤ}, as k(√2 - 1) is not necessarily an integer.

The proof can be fixed I think with K the set of rational numbers {q: q√2 ∈ ℤ}

Re: Formalising a new proof that the square root of two is irrational

#53

Post by zeroonetwothree »

DNied wrote: post #43
scotty79 wrote: post #42

Earlier quoted context omitted.

I think we are basing it on what we know about root 2. That it's larger than one and less than 2.

You forget that √x always has 2 solutions: 1 positive and 1 negative.

The sqrt symbol is defined as the positive root

Re: Formalising a new proof that the square root of two is irrational

#54

Post by zeroonetwothree »

estomagordo wrote: post #40
phkahler wrote: post #39

Earlier quoted context omitted.

>> The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1. Doesn't it also rely on √2 being positive?

Which it is, by definition?

I can’t believe you are downvoted. In math sqrt is defined as the positive one. It seems HN readers need a refresher.

Re: Formalising a new proof that the square root of two is irrational

#56

Post by thehappypm »

johnnny wrote: post #48
thehappypm wrote: post #45

Earlier quoted context omitted.

-1.4ish is another square root of 2

I'll repeat myself: it's very obvious in context that they meant the positive solution of xˆ2 = 2. My definition of the square root is as follows: the square root of a positive real number x is the positive number, noted √x, such that (√x) ^ 2 = x. To make this a useable definition, we need to prove that equation has a solution (using the fact the function t -> t^2 is zero for t=0, diverges to +inf when t -> +inf, an…

The most satisfying answer I have for the nature of the square root is to consider complex numbers.

For an arbitrary complex number, a + bi, we can plot this as a vector on a two axis scale (x axis real and y axis imaginary). We can also convert any complex number to the form z = r e^(i θ). In other words, draw the complex number vector as an angle and a magnitude, in polar form.

So any number can be drawn as a vector onto the complex plane. Multiplying two vectors together causes the angles to add and the magnitude to multiply — creating a rotated and extended (or shrunken) new vector as the product.

So what’s the square root of a complex number z? It’s the vector a that, when multiplied by itself, winds up with z.

When z has no imaginary component, it lies flat on the x axis; its magnitude is z and the angle is 0. What’s its square root?

There are two. |a|e^(i 0) and |a|e^(i 180). 180 degrees multiplied together rotates the vector back to 0. And the e^(i 180), in radians, is e^(i pi), or negative one.

So putting it together: there are only two solutions, with the same magnitude, and different signs.

Re: Formalising a new proof that the square root of two is irrational

#57

Post by johnnny »

janm31415 wrote: post #52

I might be missing something, but as I see it here: by assumption, √2 is rational. Then k(√2-1) √2 is a positive integer. This does not mean that k(√2 - 1) belongs to K, with K the set of positive integers {n: n√2 ∈ ℤ}, as k(√2 - 1) is not necessarily an integer. The proof can be fixed I think with K the set of rational numbers {q: q√2 ∈ ℤ}

k * √2 is an integer, and k is an integer, by construction of K and the initial assumption that K is not empty.

Therefore their difference k * √2 - k = k * (√2 - 1) is an integer.

Re: Formalising a new proof that the square root of two is irrational

#58

Post by janm31415 »

johnnny wrote: post #57
janm31415 wrote: post #52

I might be missing something, but as I see it here: by assumption, √2 is rational. Then k(√2-1) √2 is a positive integer. This does not mean that k(√2 - 1) belongs to K, with K the set of positive integers {n: n√2 ∈ ℤ}, as k(√2 - 1) is not necessarily an integer. The proof can be fixed I think with K the set of rational numbers {q: q√2 ∈ ℤ}

k * √2 is an integer, and k is an integer, by construction of K and the initial assumption that K is not empty. Therefore their difference k * √2 - k = k * (√2 - 1) is an integer.

correct, I missed that.

Re: Formalising a new proof that the square root of two is irrational

#59

Post by perihelions »

jacobn wrote: post #50
martopix wrote: post #10

Earlier quoted context omitted.

... which contradicts the hypothesis that k is the minimum. Therefore, K is empty.

For clarity: the proof hinges on (√2 - 1) This is why it also works for √3, but doesn’t work for √5 or 1.5

Right. It can also generalize for any non-integral square root of an integer √n. Let a be the integer ⌊√n⌋, such that a 
    k' = √n k - a k         (instead of √2 k - 1 k)
       = k(√n - a)          (so 0

Re: Formalising a new proof that the square root of two is irrational

#60

Post by johnnny »

janm31415 wrote: post #58
johnnny wrote: post #57

Earlier quoted context omitted.

k * √2 is an integer, and k is an integer, by construction of K and the initial assumption that K is not empty. Therefore their difference k * √2 - k = k * (√2 - 1) is an integer.

correct, I missed that.

As fro your further edit: assuming √2 is rational, then the set of ~~rational~~ integers {q: q√2 ∈ ℤ} does not admit a minimum, indeed it contains arbitrarily small numbers, so we can't pick k the smallest member of that set.
Post reply on HN