It is well known that the greeks proved the irrationality of $\sqrt{2} $ but they do so in a informal manner, i.e. they lack of formal definition of irrational number. Today we have several axiomatic constructions of the reals, and formal definitions of real numbers and irrational numbers, take the Dedekind cuts for example, a irrational number is now defined to be a Dedekind cut that is not a rational cut.
My question is:
"Is the classical proof of the irrationality of $\sqrt{2}$ correct/valid by modern standards?"
If it is not, can we use it's method (with some minor alterations of course) to prove that $\{x \in \mathbb Q : x^2 < 2 \text { or } x < 0 \}$ is not a rational cut ?
Thanks in advance.