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

41–50 of 94 posts

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

#41

Post by vlovich123 »

phkahler wrote: post #39
thaumasiotes wrote: post #17

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. (This is necessary when we conclude that k(√2 - 1) is less than k.) The same is not true of √4 - 1. If you look at my more explicit proof sidethread, the problem occurs in line L1, where instead of going from "√2 < 2" to "√2 - 1 < 1", you'd go from "√4 < 4" to "√4 - 1 < 3" and then you'd be stuck. (My proof won't even…

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

I’m very rusty but I think this proves the positive roots are irrational. If the positive roots are irrational then the negative ones would be too.

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

#42

Post by scotty79 »

phkahler wrote: post #37
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.

Love a proof by infinite descent! But you do make the assumption that (√2 - 1) is positive and less than 1. Root 2 can be negative.

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

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

#43

Post by DNied »

scotty79 wrote: post #42
phkahler wrote: post #37

Earlier quoted context omitted.

Love a proof by infinite descent! But you do make the assumption that (√2 - 1) is positive and less than 1. Root 2 can be negative.

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.

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

#44

Post by mannykannot »

thaumasiotes wrote: post #17
technion wrote: post #14

Earlier quoted context omitted.

What am I missing about why this couldn't also argue sqrt(4) is irrational?

The parent comment didn't call it out, but this proof relies on the fact that √2 - 1 is less than 1. (This is necessary when we conclude that k(√2 - 1) is less than k.) The same is not true of √4 - 1. If you look at my more explicit proof sidethread, the problem occurs in line L1, where instead of going from "√2 < 2" to "√2 - 1 < 1", you'd go from "√4 < 4" to "√4 - 1 < 3" and then you'd be stuck. (My proof won't even…

If I am not mistaken, the proof in the article works for √3, and your lemma 1 can be modified by noting that when x > 1, √x > 1 and also 1 < 3 < 4 so 1 < √3 < 2, 0 < √3 - 1 < 1, and k' = k(√3 - 1) < k.

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

#45

Post by thehappypm »

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?

-1.4ish is another square root of 2

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

#47

Post by johnnny »

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.

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, and is continuous between the two) and that solution is unique (using the fact the same function is strictly increasing).

Do you have any other definition of √x?

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

#48

Post by johnnny »

thehappypm wrote: post #45
estomagordo wrote: post #40

Earlier quoted context omitted.

Which it is, by definition?

-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, and is continuous between the two) and that solution is unique (using the fact the same function is strictly increasing).

Do you have any other definition of √x?

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

#49

Post by Omin »

phkahler wrote: post #37
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.

Love a proof by infinite descent! But you do make the assumption that (√2 - 1) is positive and less than 1. Root 2 can be negative.

It's not an assumption, √x is defined to be the positive square root (the principal square root). The negative one is -√x.

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

#50

Post by jacobn »

martopix wrote: post #10
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.

... 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
Post reply on HN