Mathlib en Lean 4. Componentes y tácticas

Mathlib es la biblioteca matemática comunitaria para Lean 4. Se trata de un proyecto colaborativo masivo, con millones de líneas de código, cuyo objetivo es formalizar de manera unificada las matemáticas, desde la lógica básica hasta el álgebra, el análisis y la teoría de números.

Tiene una estructura de grafo acíclico dirigido (DAG) de archivos Lean, donde los import determinan las dependencias. Hace un uso extensivo de type classes (clases de tipos) para sobrecargar operadores y representar estructuras matemáticas de forma genérica y se organiza en espacios de nombres.

Mathlib cubre prácticamente todas las áreas de las matemáticas puras. Algunos de sus componentes más utilizados son:

• Teoría de conjuntos y funciones.
• Relaciones y cocientes.
• Topología.
• Teoría de anillos.
• Álgebra lineal.
• Análisis.
• Probabilidad.
• Categorías.
• Derivación.
• Integración.

Aquí tenemos un ejemplo en teoría de conjuntos. Demuestra que la intersección se distribuye sobre la unión. Carga la librería de teoría de conjuntos, define las variables como conjuntos, usa la táctica de extensionalidad (el objetivo ahora es que la pertenencia del elemento x es equivalente a ambos lados) y usa la táctica simp para reescribir el objetivo traduciendo las reglas de intersección y unión a lógica proposicional y aplicando el and sobre el or.

import Mathlib
import Mathlib.Data.Set.Basic

example (A B C : Set ℕ) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  ext x
  simp only [Set.mem_inter_iff, Set.mem_union, and_or_left]

En el siguiente ejemplo se demuestra un teorema básico de topología: si una función real f es continua, entonces la función modificada g(x) = f(x) + 1 también es continua. Usa hf.add para añadir una función a la hipótesis de que f es continua y con continuous_const demuestra que cualquier función constante es continua.

import Mathlib
import Mathlib.Topology.Basic

example (f : ℝ → ℝ) (hf : Continuous f) : Continuous (fun x => f x + 1) := by
  exact hf.add continuous_const

En el siguiente ejemplo, usando la librería de cálculo diferencial, se demuestra una regla básica del cálculo: si una función f es diferenciable en un punto x, entonces la función f(y) + y también lo es, y su derivada en ese punto es f'(x) + 1. La demostración se resuelve en una sola línea usando la regla de la suma para derivadas. Si tienes una prueba de la derivada de f hf y una prueba de la derivada de g hg, hf.add hg combina ambas para demostrar que la derivada de (f + g) es la suma de sus derivadas individuales.

import Mathlib
import Mathlib.Analysis.Calculus.Deriv.Basic

example (f : ℝ → ℝ) (x : ℝ) (hf : HasDerivAt f (deriv f x) x) : 
    HasDerivAt (fun y => f y + y) (deriv f x + 1) x := by
  exact hf.add (hasDerivAt_id x)

A continuación vemos algunas de las principales tácticas que introduce Mathlib:

• ring: Identidades en anillos conmutativos.
• linarith: Desigualdades lineales sobre cuerpos ordenados.
• norm_num: Evaluación numérica concreta.
• ext: Extensionalidad para funciones, conjuntos, etc.
• gcongr: Congruencia monótona para desigualdades.
• positivity: Demuestra positividad de expresiones.
• field_simp: Simplificación de fracciones eliminando denominadores.
• aesop: Automatización general de pruebas (basada en Aesop).
• library_search: Búsqueda de lemas en la biblioteca.
• exact?: Buscar un lema exacto que cierre el objetivo.
• apply?: si solo necesitas avanzar un paso usando la biblioteca.
• tauto: Tautologías proposicionales.

Hemos visto la gran utilidad de Mathlib para formalizar las matemáticas y ayudar a hacer pruebas en Lean 4 basándose en resultados y axiomas ya existentes.