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

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.

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

You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.

i think they were joking, but i can't prove it

Unfortunately the margin is too small to contain it.

Maybe -i can.

It's also independently pretty tedious to explain that 7 is prime to a proof checker.

The proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one might have. In any case, it is an exercise in Heather MacBeth's free book: The Mechanics of Proof,

https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur...

btw, that book is a lot of fun to work through.

The obvious proof term for isprime p is exponential compared to the size of p. The AKS proof term is polynomial, but still very bad.

Is it? You can tell the checker about the remainder of division by 2 to 6.

Maybe also need to show that there are no other naturals between 1 and 7? And also that numbers greater than 7 can't be a divisor of 7?

The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.

It's a joke about `i` being imaginary.

yes the joke is on i

Taking the square root of -1 is not only an irrational thing to do but bloody daft. QED 8)

i tends to pop out as a construction so I suspect you can probably prove it is both rational and irrational or neither, depending on the fine print.

Here's a discussion: https://math.stackexchange.com/questions/823970/is-i-irratio...

I doubt you'd be able to prove that it's rational, regardless of how it's constructed, since wouldn't that imply that it's also (for example) a real number?

That's the point. When you use ambiguous definitions, you get stuck in a morass.

Still, I don't see how any such definition could even be called a "definition of √-1" in the first place, since the resulting object wouldn't actually have the properties of √-1.