Is exercise 1.3.16 actually possible?

[zli117]

First off, thanks to the team for putting this amazing course together!

Problem 1.3.16 asks to prove $p^2 + q^2 + r^2 = -4$ with $p, q, r$ being rational numbers. The problem is that, iirc, rational numbers don't include imaginary numbers, hence the square of such should be non-negative. Therefore their sum should also be non-negative.

More interestingly, I can actually write up the proof as this and Lean happily accepts it?

example {p q r : ℚ} (h1 : p + q + r = 0) (h2 : p * q + p * r + q * r = 2) :
    p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
  calc p ^ 2 + q ^ 2 + r ^ 2 = p * p + q * q + r * r := by ring
  _ = (p + q + r) ^ 2 - 2 * (p * q + p * r + q * r) := by ring
  _ = 0 ^ 2 - 2 * 2 := by rw [h1, h2]
  _ = -4 := by ring

[rzeta0]

This is interesting, I'd like to know too.

You might get an answer here: https://leanprover.zulipchat.com

(my best guess is that the hypothesis are contradictory and that is why we can get a false conclusion).

[zli117]

I think the hypothesis are indeed not consistent, and I guess Lean doesn't care about hypothesis, just whether the derivation is consistent.