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