4 ms·

I think that the reasoning is the same: * sqrt(-1) = a/b * a^2 = -1 * b^2 Then either a^2 or b^2 are negative but a square can't be negative, so contradictio

I think that the reasoning is the same: * sqrt(-1) = a/b * a^2 = -1 * b^2 Then either a^2 or b^2 are negative but a square can't be negative, so contradiction and sqrt(-1) is not rational. The main "problem" with this proof (and the original with sqrt(2)) is "how to prove that a^2 >= 0" (or that "if a^2 is even, then a is even") The first one is easy to prove: * a^2 = sign(a)^2 * abs(a)^2 * abs(a) >= 0 for any a * sign(a) = 1 or -1 for any a so sign(a)^2 = 1 (either 1*1 or -1*-1) * so a^2 >= 0 The second one may be proved: * Assume a is even, then a=2n, then a^2=4n^2=2*(2n^2) so a is even => a^2 is even * Assume a is odd, then a=2n+1, then a^2=4n^2+4n+1=2*(2n^2+2n)+1, then a^2 is odd * a is either even or odd * So the only possibility for a^2 to be even is for a to be even

ted_dunning 2y ago
There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why? And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)? Are you assuming a construction of integers from the natural numbers such that for any n < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)? Later you assume that all integers are even or odd. Why? These are niggling details that don't matter when you have chalk in hand, but do matter when speaking to a system like lean4.
- olivierduval 2y ago
  You're right that a lot that is "usually defined" in math has to be explicitly defined in theorem prover/proof assistant * abs(x) is usually defined as "x if x >=0 and -x if x < 0" * sign(x) is usually defined as "1 if x >=0 and -1 if x < 0" * with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0) Showing that any integer is either even or odd seem less obvious

ted_dunning 2y ago

There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why? And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)? Are you assuming a construction of integers from the natural numbers such that for any n < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)? Later you assume that all integers are even or odd. Why? These are niggling details that don't matter when you have chalk in hand, but do matter when speaking to a system like lean4.

olivierduval 2y ago
You're right that a lot that is "usually defined" in math has to be explicitly defined in theorem prover/proof assistant * abs(x) is usually defined as "x if x >=0 and -x if x < 0" * sign(x) is usually defined as "1 if x >=0 and -1 if x < 0" * with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0) Showing that any integer is either even or odd seem less obvious