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

71–80 of 94 posts

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

#71

Post by SideQuark »

I always liked the simple to follow proof:

Assume √2=m/n, and take m,n reduced so that 2 does not divide both (i.e., cancel 2's out of the fraction).

. Then 2nn = mm. Then 2 divides the left hand side, so 2 must divide the right hand side, so 2 must divide m. Then 22 = 4 divides the right hand side, so divides the left hand side, so 2 must divide the (n*n) part. But then 2 divides n, contradicting that 2 does not divide both m and n.

This works without much changes for sqrt of any non-square.

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

#72

Post by BeetleB »

zeroonetwothree wrote: post #54
estomagordo wrote: post #40

Earlier quoted context omitted.

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.

Most people are taught that there are two values for the square root. It was only in later math courses (e.g. precalculus) that they reserved the square root symbol exclusively for the positive square root.

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

#73

Post by syzarian »

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 equation :

x^2 = a

where a is a positive real number has two solutions. An equation can have multiple solutions (even infinitely many solutions). Sqrt(x) is a function and as such it can have only one output for a given input. Functions don’t have solutions. By definition, sqrt(a) is the nonnegative solution of the equation x^2=a. Here, a can be zero.

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

#74

Post by raldi »

graycat wrote: post #18

Let's have a simple proof so that we don't have to argue about more complicate issues: For integers p, q with q not 0, suppose 2 = (p/q)^2 Then 2 q^2 = p^2 and the left size has an odd number of factors of 2 and the right side has an even number of factors of 2, a contradiction. Therefore such p, q do not exist, and 2 does not have a rational square root. Done.

> and the left size has an odd number of factors of 2 and the right side has an even number of factors of 2, a contradiction.

Can you explain this step further?

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

#78

Post by ColinWright »

hgsgm wrote: post #35
tromp wrote: post #20

Earlier quoted context omitted.

It is simple if you can assume unique factorization of positive integers [1]. [1] https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithme...

Which is proven in a similar way as OP's proof.

... but genuinely requires a lot more work to do carefully and properly.

People underestimate how much work it is to create a non-handwavey proof of the FTA. Tim Gowers has written about this (although I don't have the reference to hand, and I'm on a train with a dodgy connection).

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

#79

Post by thehappypm »

mannerheim wrote: post #61
thehappypm wrote: post #56

Earlier quoted context omitted.

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 vecto…

The radical symbol always refers to a single-valued function by convention. x^(1/n) is used for multi-valued functions in complex analysis, not the 'n-radical' symbol, which would usually refer to the principal root.

Sure, but doesn’t that weaken the proof? It is an arbitrary restriction on the function that is required

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

#80

Post by mannerheim »

thehappypm wrote: post #79
mannerheim wrote: post #61

Earlier quoted context omitted.

The radical symbol always refers to a single-valued function by convention. x^(1/n) is used for multi-valued functions in complex analysis, not the 'n-radical' symbol, which would usually refer to the principal root.

Sure, but doesn’t that weaken the proof? It is an arbitrary restriction on the function that is required

Barely? It proves it for the principal root, and you can trivially prove it for the negative root using the principal root's irrationality.
Post reply on HN