Example Proof

Stream: new members

[Don Burgess]

Could someone write an example proof by contradiction in Lean for the statement:
Given that p is a natural number, then p^2 = 3 q^2 implies that p is a multiple of 3.

Response from Chat GPT:

https://chat.openai.com/share/d22b0f24-56d8-4c35-8e93-a125d8592ea8

[Eric Wieser]

Have you managed to state the problem in lean? That's always a good place to start.

[Bhakti Shah]

just curious, why are you trying to do it by contradiction? it seems quite simple directly (but i haven't tried it so don't quote me).
here's the problem statement if it helps, i can take a shot at it in a bit.

theorem ex₁ (p : Nat) :
(∃ q, p^2 = 3 * q^2) -> ∃ r, p = 3 * r := sorry

[Peter Hansen]

You could ask ChatGPT to prove it Lean. It will do it Lean 3, but I will get you started.

[Kevin Buzzard]

Proof by contradiction is a natural way to prove this. If p isn't a multiple of 3 then it has remainder 1 or 2 mod 3, so its square has remainder 1 mod 3 by a simple algebraic calculation and you're done. You need the theory of division with remainder but nothing else. In contrast the proof using that 3 is prime (which of course generalises to all prime numbers) is deeper because you need that if p divides ab then it divides a or b. To prove this (irreducibles are prime) has a little content (but of course we have it in mathlib). Also it's slightly harder to prove this claim constructively because it's a theorem of the form X implies Y or Z and the constructivists get a bit edgy with statements of this form.

[Don Burgess]

Thank you very much for your suggestions.

One of my frustrations as a newbie is that when I apply a solution from lean3 I seem to get lost in the syntax of lean 4

[Bhakti Shah]

@Kevin Buzzard wake up call that my math is super rusty and I should have probably tried the proof :)

[Bhakti Shah]

Don Burgess said:

Thank you very much for your suggestions.

One of my frustrations as a newbie is that when I apply a solution from lean3 I seem to get lost in the syntax of lean 4

specifically which syntactic elements? Also new but I had the same issue because a lot of resources are for lean3; I think i've overcome most of the lean3 -> lean4 confusion so maybe i can help :D

[Peter Hansen]

Finally a question on Zulip that is just basic enough that I can actually be useful!

import Mathlib.Tactic

-- The theorem
theorem p_squared_multiple_of_3_implies_p_multiple_of_3 (p : ℕ) (h_divides_p_squared : 3 ∣ p^2) : 3 ∣ p := by

  -- We introduce the following notation
  let k := p / 3
  let r := p % 3

  -- We can write p = 3k + r for some k and r
  have p_eq_3k_plus_r : p = 3 * k + r := symm (Nat.div_add_mod p 3)

  -- We use this to rewrite our goal
  rw [p_eq_3k_plus_r]

  -- Calculate p^2 = 9k^2 + 6kr + r^2 = 3 (3k^2 + 2kr) + r^2
  have p_squared_eq : p^2 = 3 * (3 * k^2 + 2 * k * r) + r^2 := by
    rw [p_eq_3k_plus_r]
    · ring

  -- Our assumption of 3 ∣ p^2 implies 3 ∣ r^2
  have remainder : 3 ∣ r^2 := by
    rw [← Nat.dvd_add_right (dvd_mul_right 3 _), ← p_squared_eq]
    · exact h_divides_p_squared

  -- We know that r is at most 2
  have : r < 3 := Nat.mod_lt p (Nat.succ_pos 2)

  -- so r must be either 0, 1 or 2.
  interval_cases r

  -- if r = 0, then 3 ∣ p and we are done
  · exact dvd_mul_right 3 k

  -- if r = 1, then 3 ∣ 1^2 which is false (contradiction)
  · contradiction

  -- if r = 2, then 3 ∣ 2^2 which is false (contradiction)
  · contradiction

  done

[Kevin Buzzard]

Instead of writing one long proof you might want to consider writing several little lemmas each with short proofs which just all slot together.

[Peter Hansen]

Kevin Buzzard said:

Instead of writing one long proof you might want to consider writing several little lemmas each with short proofs which just all slot together.

I have tried to simplify to proof, so it is easier follow. Would you still recommend splitting the theorem up into to shorter lemmas?

I guess the have : remainder could have been a lemma on its own as

lemma square_of_remainder_is_multiple (p : ℕ) (n : ℕ) (h_divides_p_squared : n ∣ p^2) : n ∣ (p % n)^2 := sorry

[Don Burgess]

I am very impressed with the responsiveness and helpfulness of this community.
Thank you Peter Hansen for the example proof -- very well done.
Chat GPT's proof started out well but seemed to end wrong.
Chat GPT's lean3 proof appeared nonsensical to me.
@Peter Hansen

[Kevin Buzzard]

@Peter Hansen looking again at your proof I think it's fine. I was misled by the length, which is to a large extent caused by the helpful comments :-) Often proofs with many haves in benefit from being split up.