Zulip Chat Archive

Stream: new members

Topic: Help me prove sqrt(6) is irrational?


Mr Proof (Jun 14 2024 at 02:47):

My proof so far:

import Mathlib

theorem irrationalSqrt6 : Irrational (6) := by
  have h:(6)^2 = 6 := by norm_num
  have q: 2 < 6 := by rw [Real.lt_sqrt];norm_num;simp
  have p: 6 < 3 :=by rw [Real.sqrt_lt];norm_num;simp;simp
  have g:Not (exists y:Int, 6 = y) :=by apply sorry
  simpa using irrational_nrt_of_notint_nrt 2 6 h g

I'm using irrational_nrt_of_notint_nrt but it needs to know that √6 is not an integer. So I've proved it lies between 2 and 3. But there I'm stuck.

I think I really need to find a better way of searching for tactics. What are the best strategies for looking for tactics? There's so many!

Kyle Miller (Jun 14 2024 at 02:58):

We're working on getting a list of tactics into the mathlib docs, but for now you can use the #help tactic command.

There's a 9-month-old copy of that output here: https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

Kyle Miller (Jun 14 2024 at 03:02):

Here are some tricks:

theorem irrationalSqrt6 : Irrational (6) := by
  have h:(6)^2 = 6 := by simp
  have q: 2 < 6 := by convert_to 4 < 6; simp; gcongr; norm_num
  have p: 6 < 3 :=by convert_to 6 < 9; simp; gcongr; norm_num
  have g:¬  y:Int, 6 = y := by
    push_neg
    intro y h
    rw [h] at p q
    norm_cast at p q
    omega
  simpa using irrational_nrt_of_notint_nrt 2 6 h g

Mr Proof (Jun 14 2024 at 03:13):

Thanks. The convert_to didn't seem to work on the web version (maybe it's not up to date yet) so I just used my original definitions of p and q and the rest seemed to work.

So omega I guess just basically solves integer equations, and in this case it found that there was no solution.

Kyle Miller (Jun 14 2024 at 03:32):

convert_to does exactly what it's supposed to do in the web version. Instead, it's that I forgot I had my simproc from the other thread still defined, so simp was able to prove the 2 = √4 goal.

Mr Proof (Jun 14 2024 at 03:33):

Ah :grinning_face_with_smiling_eyes:. Yeah that simproc is very useful. Hope you will add it to Lean even as just an extra tactic. Could call it sqrt_norm perhaps?

Asei Inoue (Jun 26 2024 at 08:24):

I’m maintaining the list of all tactics

https://github.com/Seasawher/mathlib4-tactics


Last updated: May 02 2025 at 03:31 UTC