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?
Yeah you can use it for normal software. It is very complex though, and the documentation assumes you already have a PhD in formal verification.
I wouldn’t go that far. I don’t have a PhD in anything, and I find it pretty comprehensible for the most part. I did focus on formal logic for my undergrad computer science degree, but that’s my only formal training, and I’m not some genius or anything approaching that.