Why is proof the root 2 is irrational so long?

Stream: mathlib4

[Mr Proof]

The proof that root 2 is irrational is an elementary proof.

Summarised as:
sqrt(2) = a/b , gcd(a,b)=1
=>a^2/b^2=2
=>a^2=2b^2
=>a=2k
=>2k^2=b^2
=>b=2l
contradicts gcd(2k,2l)=1
QED

That is at most 7 lines. I think any math student would be able to follow this proof.

Yet the Lean proofs I have seen for this are very long. To me this is telling us that we are lacking the syntax to express this in a simpler way even including Mathlib. (Unless I'm mistaken and there is a simpler proof). Of course one could simply add the proof to Mathlib as a single statement but that would be cheating!

(1). So my questions are, what could be missing in Lean to make it be able to write a proof as short as this?
(2). Do you think an exercise like Code Golf in which people compete to find the shortest proofs would be a useful or fun thing?

[Eric Wieser]

Yet the Lean proofs I have seen for this are very long.

docs#irrational_sqrt_two is very short:

theorem irrational_sqrt_two : Irrational (√2) := by
  simpa using Nat.prime_two.irrational_sqrt

[Mr Proof]

Hmm... That's fair enough. But what about doing the same for sqrt(17) ?

Also, an aside the √ sign doesn't seem to work in the lean 4 web.

[Henrik Böving]

You need to import mathlib. And doing it for sqrt(17) would be as difficult as showing that 17 is prime which I imagine is possible easily.

[Mr Proof]

What about for.... sqrt(24)?

But really, my point was if the proof as I outlined above could be easily written, rather than we hide the proof inside a library.

But anyway I can prove sqrt(17) is irrational, the sqrt(24) would be harder:

import Mathlib

theorem irrationalSqrtSeventeen : Irrational (√17) := by
  have seventeenIsPrime:Nat.Prime 17 := by norm_num
  simpa using Nat.Prime.irrational_sqrt seventeenIsPrime

Not sure if there is away to inline the two seventeenIsPrime so it's only one line?

[Eric Wieser]

I think there is a missing result here:

theorem irrational_sqrt_natCast_of_not_isSquare (n : ℕ)
    (h : ¬ IsSquare n) : Irrational √n := by
  sorry

[Mr Proof]

(Oops square free doesn't mean it's a square - sorry for my silly post!)

[Michael Stoll]

docs#irrational_nrt_of_notint_nrt and nearby statements?

[Eric Wieser]

Unfortunately docs#Nat.sqrt is irreducible, so

theorem irrationalSqrtSeventeen : Irrational (√17) := by
  suffices Irrational (√(17 : ℚ)) by simpa
  decide

no longer works

[Eric Wieser]

@Joachim Breitner, we can fix that by adding @[semireducible], right?

[Matthew Ballard]

unseal Nat.sqrt.iter in?

[Mr Proof]

Here's my attempt at doing sqrt(6):

theorem irrationalSqrt6 : Irrational (√6) := by
  have h:(√6)^2 = 6 := by norm_num
  have g:Not (exists y:Int, √6 = y) :=by sorry
  simpa using irrational_nrt_of_notint_nrt 2 6 h g

Seems like I've got myself in a circular logic... actually I think I just need to show 2<sqrt(6)<3.

[Eric Wieser]

Matthew Ballard said:

unseal Nat.sqrt.iter in?

Doesn't seem to work:

import Mathlib

unseal Nat.sqrt.iter in
theorem irrationalSqrtSeventeen : Irrational (√17) := by
  suffices Irrational (√(17 : ℚ)) by simpa
  decide

[Mr Proof]

Ah I see I can do this which is quite short (though less readable):

import Mathlib
theorem irrationalSqrt17:Irrational √17:=by apply Nat.Prime.irrational_sqrt (by norm_num)

[Kyle Miller]

No need for by apply here:

theorem irrationalSqrt17 : Irrational √17 :=
  Nat.Prime.irrational_sqrt (by norm_num)

[Kyle Miller]

Eric Wieser said:

we can fix that by adding @[semireducible], right?

Wouldn't it be better to change the definition to not use well-founded recursion since it reduces unreliably? That's assuming you want decide to work here. Maybe a simproc or a norm_num extension is a better choice?

[Eric Wieser]

Yes, I was in the process of describing the norm_num extension when I spotted the decidable instance, and was hopeful it would still work

[Eric Wieser]

I made #13788 with some results related to IsSquare that might make the API more pleasant around here

[Eric Wieser]

Eric Wieser said:

I think there is a missing result here:

theorem irrational_sqrt_natCast_of_not_isSquare (n : ℕ)
    (h : ¬ IsSquare n) : Irrational √n := by
  sorry

#13867

[Eric Wieser]

Should these be simp, or is that unhelpful?

[Eric Wieser]

With that you can write

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

[Notification Bot]

This topic was moved here from #lean4 > Why is proof the root 2 is irrational so long? by Eric Wieser.

[Michael Stoll]

Heer is an alternative proof of the irrationality of √6 using docs#irrational_sqrt_of_multiplicity_odd:

import Mathlib

example : Irrational √6 := by
  apply irrational_sqrt_of_multiplicity_odd (2 * 3 :) (by omega) 2
  simp only [multiplicity.Int.natCast_multiplicity] -- convert to multiplicities over Nat
  have : multiplicity 2 (2 * 3) = 1 := by
    rw [multiplicity.mul <| Nat.prime_iff.mp Nat.prime_two, Nat.Prime.multiplicity_self Nat.prime_two,
      show multiplicity 2 3 = 0 by refine multiplicity.multiplicity_eq_zero.mpr (by omega), add_zero]
  simp only [this, PartENat.get_one, Nat.mod_succ]

Working with docs#multiplicity (which produces a docs#PartENat) feels more cumbersome than it should be, however.
Is there a simpler way of doing this?

[Yaël Dillies]

Michael Stoll said:

Working with docs#multiplicity (which produces a docs#PartENat) feels more cumbersome than it should be

I agree. I think we should make multiplicity be Nat-valued, in the spirit of docs#Nat.factorization

[Michael Stoll]

Why do we have docs#PartENat and docs#ENat ?

[Yaël Dillies]

PartENat was the former ENat and the current ENat was just WithTop Nat

[Michael Stoll]

Is there an intrinsic reason for having both? What is the difference and where is it relevant?

[Yaël Dillies]

PartENat is useful for computability, but that's about it. I am pretty sure the only reason we have both is an artifact of the refactor I mentioned (changing ENat from Part Nat to WithTop Nat) was never completed.

[Ruben Van de Velde]

In other words "historical reasons"

[Eric Wieser]

Eric Wieser said:

With that you can write

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

The change that permits this is now on master