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?
I’ve used Lean 4 a decent amount. It’s quite usable for writing normal software in the way you would write Haskell. I find it nicer than Haskell, frankly; more predictable. It’s even pretty easy to model ocaml/sml modules, roughly. There’s an ever-present temptation to lean into using advanced type theory in ways you couldn’t in those simpler languages, and which will complicate your design and make the programming quite a bit more challenging as it goes on, but you don’t have to give in to temptation.