Lean

Lean
Desarrollador(es)
Lean Focused Research Organization (FRO) http://leanprover.github.io/
Información general
Paradigma	Functional programming, Imperative programming
Apareció en	2013
Última versión estable	(2023 de octubre del 30)
Última versión en pruebas	(4.2.0)
Influido por	Coq
Ha influido a	ML Coq Haskell
Sistema operativo	Cross-platform
Licencia	Apache License 2.0
[editar datos en Wikidata]

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.

Lanzado inicialmente por Leonardo de Moura en Microsoft Research en 2013.^[1]​

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.^{[cita requerida]}

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.^[2]​ Otra mejora en comparación con la versión anterior fue la capacidad de evitar tocar el código C++ para obtener ciertas funciones.^{[cita requerida]}

Lean 4 no es compatible con versiones anteriores de Lean 3.^[3]​

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.^[4]​^[5]​ Para noviembre de 2023, Mathlib había formalizado más de 127 000 teoremas y 70 000 definiciones en Lean.^[6]​

Lean se integra con:^[7]​

• 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.

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.

inductive nat : Type
| cero : nat
| suc  : nat → nat

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

definition suma : nat → nat → nat
| n cero   := n
| n (suc m) := suc (suma n m)

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

theorem y_conmutativo : p ∧ q → q ∧ p :=
  assume h1 : p ∧ q,
  ⟨h1.right, h1.left⟩

Esta misma prueba se puede lograr mediante tácticas.

theorem y_conmutativo (p q : Prop) : p ∧ q → q ∧ p :=
begin
  assume h : (p ∧ q), -- sea la proposición p ∧ q verdadera
  cases h, -- extraer las proposiciones individuales de la conjunción
  split, -- bifurcar el objetivo en dos casos independientes: prueba p y prueba q
  repeat { assumption }
end

Lean ha llamado la atención de los matemáticos Thomas Hales^[8]​ y Kevin Buzzard. Hales lo está utilizando para su proyecto, Abstracciones Formales.^[9]​ Buzzard lo usa para el proyecto Xena.^[10]​ 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.^[11]​