Lean (asistente de pruebas)

Lean es un asistente de demostración y un lenguaje de programación funcional . ^{[ 2 ]} Se basa en el cálculo de construcciones con tipos inductivos (específicamente, el Cálculo de Construcciones Inductivas), la teoría de tipos fundamental desarrollada originalmente con el demostrador de teoremas Coq , ^{[ 3 ]} que pasó a llamarse Rocq en 2024. ^{[ 4 ]} Es un proyecto de software libre y de código abierto alojado en GitHub . Su desarrollo cuenta actualmente con el apoyo de la organización sin fines de lucro Lean Focused Research Organization (FRO).

Lean fue desarrollado principalmente por el científico informático brasileño Leonardo de Moura mientras trabajaba para Microsoft Research y ahora para Amazon Web Services , y ha contado con importantes contribuciones de otros coautores y colaboradores a lo largo de su historia.

Lanzada en 2013, ^{[ 5 ]} las versiones iniciales del lenguaje, más tarde conocidas como Lean 1 y 2, eran experimentales y contenían características como soporte para fundamentos basados ​​en la teoría de tipos homotópicos que posteriormente fueron descartadas.

Lean 3 (lanzada por primera vez el 20 de enero de 2017) fue la primera versión moderadamente estable de Lean. Se implementó principalmente en C++ con algunas características escritas en el propio Lean. Después de la versión 3.4.2, Lean 3 llegó oficialmente al final de su ciclo de vida mientras comenzaba el desarrollo de Lean 4. Durante este período intermedio, miembros de la comunidad Lean desarrollaron y publicaron versiones no oficiales hasta la 3.51.1. ^{[ 6 ]}

En 2021, se lanzó Lean 4, una reimplementación del demostrador de teoremas Lean capaz de producir código C que luego se compila, lo que permite el desarrollo de automatización eficiente específica del dominio. ^{[ 7 ]} Lean 4 también contiene un sistema de macros higiénico y procedimientos mejorados de síntesis de clases de tipos y administración de memoria con respecto a la versión anterior. ^{[ 8 ]} Otra ventaja en comparación con Lean 3 es la capacidad de evitar tocar el código C++ para modificar el frontend y otras partes clave del sistema central, ya que ahora están todas implementadas en Lean y disponibles para que el usuario final las sobrescriba según sea necesario. ^{[ 2 ]}

Lean 4 no es compatible con versiones anteriores de Lean 3. ^{[ 9 ]} Utiliza la versión C++17 de C++. ^{[ 2 ]}

En 2023, se formó Lean FRO, con los objetivos de mejorar la escalabilidad y la usabilidad del lenguaje, e implementar la automatización de pruebas . ^{[ 10 ]}

En 2025, el premio ACM SIGPLAN Programming Languages ​​Software Award fue otorgado a Gabriel Ebner, Soonho Kong, Leo de Moura y Sebastian Ullrich por Lean, citado por su "impacto significativo en las matemáticas, la verificación de hardware y software y la IA". ^{[ 11 ]}

En 2026, la biblioteca mathlib fue galardonada con el premio Demailly a la ciencia abierta . ^{[ 12 ]}

Lean incluye muchas características útiles para la programación funcional y la demostración de teoremas, como tipos dependientes , clases de tipos , multihilo, un lenguaje de tácticas expresivo y un sistema de módulos. ^{[ 13 ]}

Los números naturales pueden definirse como un tipo inductivo . Esta definición se basa en los axiomas de Peano y establece que todo número natural es cero o el sucesor de algún otro número natural.

inductivo Nat : Tipo | cero : Nat | succ : Nat → Nat

La suma de números naturales se puede definir recursivamente , utilizando la coincidencia de patrones .

def Nat . add : Nat → Nat → Nat | n , Nat . zero => n -- n + 0 = n | n , Nat . succ m = > Nat . succ ( Nat . add n m ) -- n + succ(m) = succ(n + m)

Esta es una prueba simple de${\displaystyle (P\wedge Q)\implies (Q\wedge P)}$para dos proposiciones P y Q (donde${\displaystyle \wedge }$es la conjunción y${\displaystyle \implies }$la implicación ) en Lean usando el modo táctico:

teorema and_swap ( p q : Prop ) : p ∧ q → q ∧ p := por intro h -- suponemos p ∧ q con prueba h, el objetivo es q ∧ p aplicar And . intro -- el objetivo se divide en dos subobjetivos, uno es q y el otro es p · exacto h . derecha -- el primer subobjetivo es exactamente la parte derecha de h : p ∧ q · exacto h . izquierda -- el segundo subobjetivo es exactamente la parte izquierda de h : p ∧ q

Esta misma demostración en modo término:

teorema and_swap ( p q : Prop ) : p ∧ q → q ∧ p := fun ⟨ hp , hq ⟩ => ⟨ hq , hp ⟩

El teorema también se puede demostrar utilizando la táctica de molienda, que emplea técnicas de solucionadores SMT para construir demostraciones automáticamente:

teorema and_swap ( p q : Prop ) : p ∧ q → q ∧ p := por molienda

• Tipo dependiente
• Lista de asistentes de prueba
• mimalloc
• teoría de tipos

• Sitio web oficial
• Apóyate en GitHub
• Comunidad Lean
• Lean FRO
• El juego de los números naturales : un tutorial interactivo para aprender Lean
• Moogle.ai : un motor de búsqueda semántica para encontrar teoremas en mathlib.