Lean es un asistente de pruebas y un lenguaje de programación funcional . [1] Se basa en el cálculo de construcciones con tipos inductivos . Es un proyecto de código abierto alojado en GitHub . Fue desarrollado principalmente por Leonardo de Moura mientras trabajaba para Microsoft Research y ahora Amazon Web Services , y ha tenido importantes contribuciones de otros coautores y colaboradores durante su historia. El desarrollo actualmente cuenta con el apoyo de la organización sin fines de lucro Lean Focused Research Organization (FRO) .
Lean fue lanzado por Leonardo de Moura en Microsoft Research en 2013. [2] Las versiones iniciales del lenguaje, posteriormente conocidas como Lean 1 y 2, eran experimentales y contenían características tales como soporte para fundamentos basados en la teoría de tipos de homotopía que luego fueron abandonados.
Lean 3 (publicada 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 Lean. Después de la versión 3.4.2, Lean 3 llegó al final de su vida útil oficialmente mientras comenzaba el desarrollo de Lean 4. En este período intermedio, los miembros de la comunidad Lean desarrollaron y publicaron versiones no oficiales hasta la 3.51.1.
En 2021, se lanzó Lean 4, que fue una reimplementación del demostrador de teoremas Lean capaz de producir código C que luego se compila, lo que permite el desarrollo de una automatización eficiente específica del dominio. [3] Lean 4 también contiene un sistema de macros y procedimientos mejorados de síntesis de clases de tipos y gestión de memoria con respecto a la versión anterior. Otro beneficio 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 están disponibles para que el usuario final las anule según sea necesario. [ cita requerida ]
Lean 4 no es compatible con versiones anteriores de Lean 3. [4]
En 2023, se formó Lean FRO, con los objetivos de mejorar la escalabilidad y usabilidad del lenguaje e implementar la automatización de pruebas . [5]
El paquete Lean oficial incluye una biblioteca estándar llamada baterías , que implementa estructuras de datos comunes que pueden usarse tanto para la investigación matemática como para el desarrollo de software más convencional. [6]
En 2017, comenzó un proyecto mantenido por la comunidad para desarrollar una biblioteca Lean, mathlib , con el objetivo de digitalizar la mayor cantidad posible de matemáticas puras en una gran biblioteca cohesiva, hasta llegar a las matemáticas de nivel de investigación. [7] [8] A septiembre de 2024, mathlib había formalizado más de 165 000 teoremas y 85 000 definiciones en Lean. [9]
Lean se integra con: [10]
La interfaz se realiza a través de una extensión de cliente y un servidor de protocolo de servidor de lenguaje .
Tiene soporte nativo para símbolos Unicode , que pueden escribirse usando secuencias similares a LaTeX , como "\times" para "×". Lean también puede compilarse en JavaScript y accederse a él en un navegador web y tiene un amplio soporte para metaprogramación .
Los números naturales pueden definirse 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.
inductivo Nat : Tipo | cero : Nat | succ : Nat → NatLa suma de números naturales se puede definir de forma recursiva , utilizando la coincidencia de patrones .
def Nat.add : Nat → Nat → Nat | n , Nat.cero => 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 para dos proposiciones y (donde es la conjunción y la implicación ) en Lean usando el modo táctico:
teorema and_swap ( p q : Prop ) : p ∧ q → q ∧ p := por intro h -- suponga 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 · exact h.right -- el primer subobjetivo es exactamente la parte derecha de h : p ∧ q · exact h.left -- el segundo subobjetivo es exactamente la parte izquierda de h : p ∧ qEsta misma prueba en modo término:
teorema and_swap ( p q : Prop ) : p ∧ q → q ∧ p := fun ⟨ hp , hq ⟩ => ⟨ hq , hp ⟩Lean ha recibido la atención de matemáticos como Thomas Hales , [11] Kevin Buzzard , [12] y Heather Macbeth. [13] Hales lo está utilizando para su proyecto, Formal Abstracts. [14] Buzzard lo utiliza para el proyecto Xena. [15] Uno de los objetivos del Proyecto Xena es reescribir todos los teoremas y pruebas en el plan de estudios de matemáticas de pregrado del Imperial College de Londres en Lean. Macbeth está utilizando Lean para enseñar a los estudiantes los fundamentos de la prueba matemática con retroalimentación instantánea. [16]
En 2021, un equipo de investigadores utilizó Lean para verificar la exactitud de una prueba de Peter Scholze en el área de las matemáticas condensadas . El proyecto ganó atención por formalizar un resultado en la vanguardia de la investigación matemática. [17] En 2023, Terence Tao utilizó Lean para formalizar una prueba de la conjetura polinomial de Freiman-Ruzsa (PFR), un resultado publicado por Tao y colaboradores en el mismo año. [18]
En 2022, OpenAI y Meta AI crearon de forma independiente modelos de IA para generar pruebas de varios problemas de olimpiadas de nivel secundario en Lean. [19] El modelo de Meta AI está disponible para uso público con el entorno Lean. [20]
En 2023, Vlad Tenev y Tudor Achim cofundaron la startup Harmonic, cuyo objetivo es reducir las alucinaciones de la IA generando y verificando código Lean. [21]
En 2024, Google DeepMind creó AlphaProof [22] , que demuestra afirmaciones matemáticas en Lean al nivel de un medallista de plata en la Olimpiada Internacional de Matemáticas. Este fue el primer sistema de IA que logró un desempeño digno de una medalla en los problemas de una olimpiada de matemáticas. [23]
.svg/1280px-Free_and_open-source_software_logo_(2009).svg.png){kind=logo}