Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code
/-- A prime is a number larger than 1 with no trivial divisors -/
def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n
-- 'Grind' efficiently manages complex pattern matching and
-- case analysis beyond standard tactics.
example (x : Nat) : 0 < match x with
| 0 => 1
| n+1 => x + n := by
grind
-- Automatically solves systems of linear inequalities.
example (x y : Int) :
27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45
→ -10 ≤ 7*x - 9*y → 7*x - 9*y > 4 := by
grind
Does anyone have experience with Lean? Can it be useful for implementing algorithms or logic beyond mathematical proofs, for software libs?
Lean is a functional programming language, and can be used as one i.e. you can make absolutely anything in it. But it’s mostly meant for theorem proving, so you won’t get any libraries/support for regular software dev. That said, I do know folks who have written complex software (I remember seeing the code for a raytracer) in it, so it’s definitely doable.