Lean
# Lean

Lean es un asistente de pruebas y un lenguaje de programación. Se basa en el cálculo de construcciones con tipos inductivos. Es un proyecto de código abierto alojado en GitHub. Fue realizado por Microsoft Research.

## Historia

Lanzado inicialmente por Leonardo de Moura en Microsoft Research en 2013.

Lean 3 fue implementado como una máquina virtual, lo que lo hizo menos eficiente debido al coste inherente de la interpretación, lo que lo hizo menos competitivo en comparación con otros asistentes de pruebas como Coq.

En 2021, se liberó Lean 4 con una reimplementación del demostrador del teorema de Lean capaz de producir código C, que luego es compilado, lo que permite el desarrollo de una automatización eficiente de dominios específicos. Otra mejora en comparación con la versión anterior fue la capacidad de evitar tocar el código C++ para obtener ciertas funciones.

Lean 4 no es compatible con versiones anteriores de Lean 3.

## Descripción general

### Librerías

En 2017, el proyecto adoptó una librería mathlib mantenida por el usuario con el objetivo de digitalizar la investigación en matemáticas puras. Para noviembre de 2023, Mathlib había formalizado más de 127 000 teoremas y 70 000 definiciones en Lean.

### Integración con editores

Lean se integra con:

* Visual Studio Code
* Neovim
* Emacs

La interfaz se realiza a través de una extensión de cliente y un servidor Language Server Protocol.

Tiene soporte nativo para símbolos Unicode, que se pueden escribir usando secuencias similares a las de LaTeX, como "\times" para "×". Lean también puede transpilarse a JavaScript pudiéndose usar desde un navegador web y tiene un amplio soporte para la metaprogramación.

## Ejemplos (Lean 3)

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

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

Esta es una prueba simple con términos en lean.

Esta misma prueba se puede lograr mediante tácticas.

## Uso

Lean ha llamado la atención de los matemáticos Thomas Hales y Kevin Buzzard. Hales lo está utilizando para su proyecto, Abstracciones Formales. Buzzard lo usa para el proyecto Xena. Uno de los objetivos del Proyecto Xena es reescribir todos los teoremas y pruebas del plan de estudios de matemáticas del Imperial College London en Lean.

En 2021, Peter Scholze utilizó Lean para formalizar una nueva prueba en el área de matemáticas condensadas, demostrando que Lean puede ser útil en la vanguardia de la investigación matemática.

