29 enero 2024 – Calculemus

La raíz cuadrada de 2 es irracional

PorJosé A. Alonso 29 enero 202417 febrero 2024

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

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