--- Título: La raíz cuadrada de 2 es irracional Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que la raíz cuadrada de 2 es irracional; es decir, que no existen \\(m, n ∈ ℕ\\) tales que \\(m\\) y \\(n\\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \\(m² = 2n²\\). Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
import Std.Data.Nat.Gcd
open Nat
variable {m n : ℕ}

example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 :=
by sorry

1. Demostración en lenguaje natural

Usaremos el lema del ejercicio anterior: \\[ (∀ n ∈ ℕ)[2 ∣ n² → 2 | n] \\] Supongamos que existen existen \\(m, n ∈ ℕ\\) tales que \\(m\\) y \\(n\\) son coprimos y \\(m² = 2n²\\) y tenemos que demostrar una contradicción. Puesto que 2 divide a 1, para tener la contradicción basta demostrar que 2 divide a 1 y (ya que \\(m\\) y \\(n\\) son coprimos); para ello es suficiente demostrar que 2 divide al máximo común divisor de \\(m\\) y \\(n\\). En definitiva, basta demostrar que 2 divide a \\(m\\) y a \\(n\\). La demostración de que 2 divide a \\(m\\) es \\begin{align} m² = 2n² &⟹ 2 | m² \\\\ &⟹ 2 | m &&\\text{[por el lema]} \\end{align} Para demostrar que 2 divide a \\(n\\), observamos que, puesto que 2 divide a \\(m\\), existe un \\(k ∈ ℕ\\) tal que \\(m = 2k\\). Sustituyendo en \\[ m² = 2n² \\] se tiene \\[ (2k)² = 2n² \\] Simplificando, queda \\[ 2k = n² \\] Por tanto, 2 divide a \\(n²\\) y, por el lema, 2 divide a \\(n\\).

2. Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime
import Std.Data.Nat.Gcd
open Nat
variable {m n : ℕ}

lemma par_si_cuadrado_par
  (h : 2 ∣ n ^ 2)
  : 2 ∣ n :=
by
  rw [pow_two] at h
  -- h : 2 ∣ n * n
  have h2 : 2 ∣ n ∨ 2 ∣ n := (Prime.dvd_mul prime_two).mp h
  tauto

example : ¬∃ m n, coprime m n ∧ m ^ 2 = 2 * n ^ 2 :=
by
  rintro ⟨m, n, ⟨h1, h2⟩⟩
  -- m n : ℕ
  -- h1 : coprime m n
  -- h2 : m ^ 2 = 2 * n ^ 2
  -- ⊢ False
  have h3 : ¬(2 ∣ 1) := by norm_num
  have h4 : 2 ∣ 1 := by
    have h5 : Nat.gcd m n = 1 := h1
    rw [← h5]
    -- ⊢ 2 ∣ Nat.gcd m n
    have h6 : 2 ∣ m := by
      apply par_si_cuadrado_par
      -- ⊢ 2 ∣ m ^ 2
      rw [h2]
      -- ⊢ 2 ∣ 2 * n ^ 2
      exact Nat.dvd_mul_right 2 (n ^ 2)
    have h7 : 2 ∣ n := by
      have h8 : ∃ k, m = 2 * k := h6
      rcases h8 with ⟨k, h9⟩
      -- k : ℕ
      -- h9 : m = 2 * k
      have h10 : 2 * k ^ 2 = n ^ 2 := by
        have h10a : 2 * (2 * k ^ 2) = 2 * n ^ 2 := calc
          2 * (2 * k ^ 2) = (2 * k) ^ 2 := by nlinarith
                        _ = m ^ 2       := by rw [← h9]
                        _ = 2 * n ^ 2   := h2
        show 2 * k ^ 2 = n ^ 2
        exact (mul_right_inj' (by norm_num : 2 ≠ 0)).mp h10a
      have h11 : 2 ∣ n ^ 2 := by
        rw [← h10]
        -- ⊢ 2 ∣ 2 * k ^ 2
        exact Nat.dvd_mul_right 2 (k ^ 2)
      show 2 ∣ n
      exact par_si_cuadrado_par h11
    show 2 ∣ Nat.gcd m n
    exact Nat.dvd_gcd h6 h7
  show False
  exact h3 h4

-- Lemas usados
-- ============

-- variable (p k : ℕ)
-- #check (pow_two n : n ^ 2 = n * n)
-- #check (Prime.dvd_mul : Nat.Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n))
-- #check (prime_two : Nat.Prime 2)
-- #check (Nat.dvd_gcd : k ∣ m → k ∣ n → k ∣ Nat.gcd m n)
-- #check (Nat.dvd_mul_right m n :  m ∣ m * n)
-- #check (mul_right_inj' : k ≠ 0 → (k * m = k * n ↔ m = n))

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.