An error free lean code

Stream: new members

[Matherian]

Can anyone please provide Lean 4 code for a proof that sqrt(10001) is irrational which will run with no error messages in the Lean online editor? Thanks a lot!

[Notification Bot]

This topic was moved here from #lean4 > An error free lean code by Kevin Buzzard.

[Kevin Buzzard]

You can use e.g. docs#irrational_sqrt_intCast_iff_of_nonneg to do this. And it's better to ask questions with Lean code rather than informally -- it's not clear what the type of your numeral is, for example.

[Michael Rothgang]

Also, please don't double post: there's no need to. I only need to read something once :-)

[Matherian]

Kevin Buzzard said:

You can use e.g. docs#irrational_sqrt_intCast_iff_of_nonneg to do this. And it's better to ask questions with Lean code rather than informally -- it's not clear what the type of your numeral is, for example.

How to correct:

'''
import Mathlib.Data.Real.Irrational
import Mathlib.Tactic

theorem sqrt_10001_irrational : Irrational (Real.sqrt 10001) := by
-- 1. Apply the theorem: sqrt(n) is irrational if n is not a perfect square
apply Nat.irrational_sqrt_of_not_isSquare

-- 2. The goal is now to prove ¬ IsSquare 10001
-- We switch the definition of a square to a computable check: (sqrt n)^2 = n
rw [Nat.isSquare_iff_sq_sqrt]

-- 3. Ask Lean to compute the check (100^2 = 10000 ≠ 10001) and close the goal
decide
'''

Thanks!

[Ilmārs Cīrulis]

#backticks?

[Matherian]

Ilmārs Cīrulis said:

#backticks?

Do you know to correct the lean code? Thanks.

[Ilmārs Cīrulis]

My try, though I was very lazy and didn't add comments with explanations.

import Mathlib.NumberTheory.Real.Irrational
import Mathlib.Tactic

theorem sqrt_10001_irrational : Irrational (Real.sqrt 10001) := by
  rw [show (10001 : ℝ) = ↑(10001 : ℤ) by norm_cast]
  rw [irrational_sqrt_intCast_iff_of_nonneg (by norm_num)]
  norm_cast
  intro h
  rw [isSquare_iff_exists_sq] at h
  have aux : ∃ r, r * r = 10001 := by grind [sq]
  rw [Nat.exists_mul_self] at aux
  norm_num at aux

[Ilmārs Cīrulis]

Yes, I know. :D
I would suggest not using AI, until your natural brain has learned necessary Lean and Mathlib skills.

[Edit:] Ask for pointers how to learn all necessary Lean/Mathlib stuff by yourself, and people will help.

[Ilmārs Cīrulis]

There is something like this, too: https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Real/Irrational.html#instDecidableIrrationalSqrtOfNatReal

With an example how to use it, but I couldn't get it to work. Maybe this is useful.

[Ilmārs Cīrulis]

Today I learned something more.

This, of course, can be compressed by putting all rewrites under one simp_rw.

import Mathlib.Data.Real.Irrational
import Mathlib.Tactic

theorem sqrt_10001_irrational : Irrational (Real.sqrt 10001) := by
  rw [irrational_sqrt_ofNat_iff]
  rw [isSquare_iff_exists_sq]
  simp_rw [sq, eq_comm]
  rw [Nat.exists_mul_self]
  norm_num