Introducción a Lean 4 como lenguaje de tipos para las matemáticas

Lean 4 es un lenguaje de programación funcional y un asistente de pruebas interactivo basado en la teoría de tipos dependientes. Su fundamento lógico es el cálculo de construcciones con una jerarquía de universos e tipos inductivos . La idea central es que en matemáticas, cada objeto (un número, una función, una demostración) tiene un tipo.  Las proposiciones matemáticas son tipos y las demostraciones son términos de esos tipos. Verificar una demostración es verificar que un término tiene el tipo correcto. 

TIPOS Y TÉRMINOS

En Lean, todo tiene un tipo. Un tipo es una colección de objetos, y un término es un elemento de un tipo. La relación se escribe x : T, que significa “el término x tiene tipo T“.

Por ejemplo, #check true tiene como salida Bool.true. Y #check Nat tiene como salida Nat : Type, ya que un tipo es también un término de tipo Type.

Esta estructura impide escribir expresiones sin sentido matemático, como “9 es un grupo”. Cada operación y cada función tienen un tipo que especifica exactamente qué entradas aceptan y qué salida producen.

Las funciones se construyen con tipos flecha. Si A y B son tipos, A → B es el tipo de las funciones que toman un elemento de A y devuelven uno de B. La aplicación de una función f a un argumento a se escribe simplemente f a.

-- Una función de Nat a Nat
def cuadrado (n : Nat) : Nat := n * n

-- Aplicación de la función
#eval cuadrado 5   -- 25

-- El tipo de la función
#check cuadrado    -- cuadrado : Nat → Nat

TIPOS INDUCTIVOS

Los tipos inductivos son la construcción fundamental en Lean 4 para definir nuevos tipos de datos. Un tipo inductivo se especifica enumerando sus constructores, que son las formas básicas de construir elementos del tipo . Intuitivamente, un elemento del tipo se construye aplicando finitamente los constructores.

El ejemplo más básico en matemáticas son los números naturales, definidos por los axiomas de Peano: existe un constructor para el cero, y una función sucesor.

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

Los tipos inductivos vienen equipados con reglas de eliminación que permiten definir funciones por recursión y demostrar propiedades por inducción. En Lean 4, las reglas de eliminación (o eliminators) describen cómo puedes usar o consumir un tipo de dato inductivo. Si la regla de introducción te dice cómo construir un valor (como zero o succ), la regla de eliminación te dice cómo desarmarlo para razonar sobre él o calcular un resultado.

TIPOS INDUCTIVOS DEPENDIENTES

Un tipo inductivo dependiente es una estructura de datos cuyos constructores cambian o dependen del valor de un índice y no solo de un parámetro como en los tipos inductivos.

Un ejemplo fundamental en matemáticas es el tipo de vectores de longitud fija. El tipo Vector α n representa listas de elementos de tipo α con exactamente n elementos.

inductive Vect (α : Type) : Nat → Type where
  | nil : Vect α 0
  | cons : {n : Nat} → α → Vect α n → Vect α (n + 1) 

open Vect
-- Vector que contiene 3 booleanos
def boolVec : Vect Bool 3 := cons true (cons false (cons true nil))

ESTRUCTURAS Y TYPE CLASSES

Las estructuras en Lean son tipos inductivos con un solo constructor, que agrupan varios campos. Se usan para representar objetos matemáticos compuestos, como pares ordenados, números complejos o espacios vectoriales.

A continuación vemos una estructura con dos parámetros para definir el producto cartesiano. Vemos que solo hay un constructor. Después creamos con esa estructura un par ordenado de dos números y accedemos a los valores.

structure MiProducto (α : Type) (β : Type) where
  fst : α
  snd : β

-- Un par ordenado de dos números: MiProducto Nat Nat
def coordenada : MiProducto Nat Nat := 
  { fst := 10, snd := 20 }

-- Acceder a los valores matemáticos:
#eval coordenada.snd -- Devuelve 20

Las type classes son un mecanismo de sobrecarga que permite definir jerarquías de estructuras algebraicas. Cada estructura algebraica (semigrupo, monoide, grupo, anillo, cuerpo, espacio vectorial) se define como una type class, y las instancias registran qué tipos concretos satisfacen esa estructura

La jerarquía comienza con la estructura más básica, el magma (un tipo con una operación binaria), y se extiende sucesivamente.

class Magma (α : Type) where
  op : α → α → α

class Semigroup (α : Type) extends Magma α where
  op_assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

class Monoid (α : Type) extends Semigroup α where
  e : α
  op_id_left  : ∀ (a : α), op e a = a
  op_id_right : ∀ (a : α), op a e = a

class Group (α : Type) extends Monoid α where
  inv : α → α
  op_inv_left  : ∀ (a : α), op (inv a) a = e
  op_inv_right : ∀ (a : α), op a (inv a) = e

Cuando escribimos una función que requiere que α sea un grupo, usamos el parámetro de instancia [Group α]. Lean buscará automáticamente una instancia de Group para el tipo concreto.

Mathlib, la biblioteca matemática de Lean, usa esta jerarquía de manera extensiva para definir las estructuras matemáticas.

PREDICADOS INDUCTIVOS

Un predicado inductivo es un tipo inductivo cuyo tipo de retorno es Prop (la proposición). En lugar de definir un tipo de datos, se define una relación o propiedad mediante reglas de inferencia. Cada constructor es una regla que permite derivar que ciertos elementos satisfacen el predicado.

Un ejemplo es la definición inductiva de los números pares. 0 es número par, entonces 2, 4….

inductive Even : N → Prop where
| zero : Even 0
| add_two : ∀k : N, Even k → Even (k + 2)

Estas definiciones inductivas generan automáticamente principios de inducción mutua, que permiten demostrar propiedades sobre números pares e impares simultáneamente.

Importante destacar que en Lean 4, la diferencia principal entre definir un objeto como un tipo inductivo o como un predicado inductivo radica en el universo de tipos en el que habitan (Type vs. Prop) y en su propósito fundamental: construir datos con contenido computacional (tipo inductivo) frente a establecer propiedades o condiciones lógicas (predicado inductivo).

Hemos visto las principales estructuras en Lean 4. La biblioteca Mathlib construye sobre estos cimientos una vasta formalización de las matemáticas modernas, desde el álgebra abstracta hasta el análisis real y la teoría de números.