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.
| 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 | |
Historia
editarLanzado 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]
Descripción general
editarLibrerías
editarEn 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]
Integración con editores
editarLean se integra con:[7]
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)
editarLos 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
Uso
editarLean 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]
Referencias
editar- ↑ «Lean Prover About Page». Archivado desde el original el 18 de octubre de 2021. Consultado el 16 de noviembre de 2023.
- ↑ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff, eds. Automated Deduction -- CADE 28. Springer International Publishing. pp. 625-635. ISBN 978-3-030-79876-5. Consultado el 24 de marzo de 2023.
- ↑ «Significant changes from Lean 3». Lean Manual. Consultado el 24 de marzo de 2023.
- ↑ «Building the Mathematical Library of the Future». Quanta Magazine. Archivado desde el original el 2 de octubre de 2020.
- ↑ «Lean community». leanprover-community.github.io. Consultado el 24 de octubre de 2023.
- ↑ «Mathlib statistics». leanprover-community.github.io. Consultado el 1 de noviembre de 2023.
- ↑ «Installing Lean 4 on Linux». leanprover-community.github.io. Consultado el 24 de octubre de 2023.
- ↑ Hales, Thomas (18 de septiembre de 2018). «A Review of the Lean Theorem Prover». Jigger Wit. Archivado desde el original el 21 de noviembre de 2020.
- ↑ «Formal Abstracts». Github.
- ↑ «What is the Xena project?». Xena (en inglés). 8 de mayo de 2019.
- ↑ Hartnett, Kevin (28 de julio de 2021). «Proof Assistant Makes Jump to Big-League Math». Quanta Magazine. Archivado desde el original el 2 Jan 2022.
Datos: Q6509476
