Lean

Lean es a la vez un lenguaje de programación funcional y un asistente de demostración moderno. Su biblioteca Mathlib ha reunido a una gran comunidad de matemáticos que formalizan teoremas, y gana terreno frente a Coq por su ergonomía.

• Creado por Leonardo de Moura (Microsoft)
• Año 2013
• Paradigma: Funcional · asistente de pruebas
• Extensiones: .lean

Para qué se usa

• Formalizar matemáticas
• Verificación
• Investigación

A favor

• Moderno y ergonómico
• Gran comunidad (Mathlib)
• Funcional y de pruebas

En contra

• Curva muy dura
• Nicho académico
• En rápida evolución

Ecosistema

• Mathlib
• Lean 4
• Lake

Ejemplo

def main : IO Unit :=
  IO.println "¡Hola, mundo!"