$ whois lean

Lean

first released in 2013 · by Leonardo de Moura

$ guessprog --inspect lean

year: 2013
paradigm: functional
family: ml
memory: reference counting
binding: static
safety: strong

LEAN(7)

AUTHORS: Leonardo de Moura
HISTORY: Leonardo de Moura started Lean at Microsoft Research in 2013 as a theorem prover based on dependent type theory, where a proof is a program and a theorem is its type. Lean 4, released in 2021, was rewritten in Lean itself and is also a general-purpose, purely functional programming language. It compiles to C and manages memory with reference counting, updating values in place when nobody else holds a reference.
USAGE: Lean is the leading tool for formalising mathematics: the community library Mathlib holds hundreds of thousands of verified theorems. It is increasingly used to verify software and by AI systems that generate checkable proofs, and since 2023 it is developed by the non-profit Lean FRO.
SEE ALSO: Lean on Wikipedia ↗

$ cat Sum.lean

def sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

#eval sum [1, 2, 3]  -- 6

-- a proof is checked by the compiler, like a type
theorem sum_append (xs ys : List Nat) :
    sum (xs ++ ys) = sum xs + sum ys := by
  induction xs with
  | nil => simp [sum]
  | cons x xs ih => simp [sum, ih, Nat.add_assoc]