Mechanics of Proof 1.3.11 ex 16

Stream: lean4

[George Menhorn]

Problem 1.3.11 ex 16 in Mechanics of Proofs asks to show:

example {p q r : ℚ} (h1 : p + q + r = 0) (h2 : p * q + p * r + q * r = 2) :
    p ^ 2 + q ^ 2 + r ^ 2 = -4.

This is fairly straight forward to show in Lean but it begs the question. I understand that given the two hypotheses, it is algebraically valid to show the result. However, the result, the sum of squares of three rational numbers, can never be negative. How, then, can this be shown to be valid in Lean? I assumed that Lean's type checking machinery would catch this sort of inconsistency, but it does not. Could something like this come up in the context of a larger proof where a theorem can be proved but isn't actually consistent?

Thanks for any clarification on this behavior in Lean.

[Riccardo Brasca]

There are two things here:

• first of all Lean has no way of guessing that something is false in general (otherwise it would be able to say when something is true, so it would be able to solve all mathematics, and this is not the case).
• secondly, the fact that something false implies something is true mathematically, so there is no problem here. What you have proved is something like 1 + 1 = 3 → 6 > 5, that is simply true.

[Riccardo Brasca]

https://en.wikipedia.org/wiki/Principle_of_explosion

[Chris Wong]

As a bonus exercise, you can try replacing the goal with False :wink: