Apuntes sobre demostraciones formales en Lean, matemáticas y programación. Aquí escribo sobre lo que estoy probando, demostrando o construyendo.
Esta es la primera de varias — más notas sobre Lean, matemáticas y programación van llegando.
Esta es una de las demostraciones más antiguas de las matemáticas — se le atribuye a los pitagóricos y aparece en los Elementos de Euclides. Es una prueba por contradicción, simple pero contundente.
Supongamos, por contradicción, que √2 es racional. Entonces existen enteros $p$ y $q$ coprimos (sin factores comunes) tales que:
Elevando al cuadrado y despejando:
Esto significa que $p^2$ es par, y por lo tanto $p$ también es par (el cuadrado de un impar siempre es impar). Escribimos $p = 2k$ para algún entero $k$:
Por el mismo argumento, $q^2$ es par, así que $q$ también es par. Pero si $p$ y $q$ son ambos pares, comparten el factor 2 — lo cual contradice que $\gcd(p, q) = 1$.
La suposición inicial es falsa: √2 no puede escribirse como una fracción $p/q$. Es irracional. $\blacksquare$
Y aquí está el mismo resultado, pero verificado formalmente — no con un argumento en prosa que un humano revisa, sino con una prueba que una computadora comprueba paso a paso, usando Mathlib:
import Mathlib.Data.Real.Irrational
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :=
(Nat.prime_two).irrational_sqrt
-- Mathlib ya lo tiene probado directamente como `irrational_sqrt_two`.
-- La prueba de fondo generaliza el mismo argumento de arriba:
-- para todo primo p, √p es irracional.(Código de referencia — verifica siempre el nombre exacto del lema contra la versión de Mathlib que estés usando, cambian con el tiempo.)
Estoy escribiendo un libro sobre este puente: demostraciones clásicas como esta, y cómo se ven cuando las llevas a un asistente de pruebas como Lean. Mientras tanto, en mi canal de YouTube (@SalvadorTech) voy subiendo contenido introductorio sobre Lean.